Superset relation on Data.Fin.Subsets (#2719)

* Subset supersets

* Use flip to define superset relations

Author: Taneb

CHANGELOG.md

@@ -235,6 +235,29 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Fin.Subset`:
+  ```agda
+  _⊇_ : Subset n → Subset n → Set
+  _⊉_ : Subset n → Subset n → Set
+  _⊃_ : Subset n → Subset n → Set
+  _⊅_ : Subset n → Subset n → Set
+
+  ```
+
+* In `Data.Fin.Subset.Induction`:
+  ```agda
+  ⊃-Rec : RecStruct (Subset n) ℓ ℓ
+  ⊃-wellFounded : WellFounded _⊃_
+  ```
+
+* In `Data.Fin.Subset.Properties`
+  ```agda
+  p⊆q⇒∁p⊇∁q : p ⊆ q → ∁ p ⊇ ∁ q
+  ∁p⊆∁q⇒p⊇q : ∁ p ⊆ ∁ q → p ⊇ q
+  p⊂q⇒∁p⊃∁q : p ⊂ q → ∁ p ⊃ ∁ q
+  ∁p⊂∁q⇒p⊃q : ∁ p ⊂ ∁ q → p ⊃ q
+  ```
+
 * In `Data.List.Properties`:
   ```agda
   map-applyUpTo : ∀ (f : ℕ → A) (g : A → B) n → map g (applyUpTo f n) ≡ applyUpTo (g ∘ f) n

src/Data/Fin/Subset.agda

@@ -15,6 +15,7 @@ open import Data.List.Base using (List; foldr; foldl)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (∃; _×_)
 open import Data.Vec.Base hiding (foldr; foldl)
+open import Function.Base using (flip)
 open import Relation.Nullary
 
 private
@@ -77,6 +78,18 @@ p ⊂ q = p ⊆ q × ∃ (λ x → x ∈ q × x ∉ p)
 _⊄_ : Subset n → Subset n → Set
 p ⊄ q = ¬ (p ⊂ q)
 
+_⊇_ : Subset n → Subset n → Set
+_⊇_ = flip _⊆_
+
+_⊉_ : Subset n → Subset n → Set
+_⊉_ = flip _⊈_
+
+_⊃_ : Subset n → Subset n → Set
+_⊃_ = flip _⊂_
+
+_⊅_ : Subset n → Subset n → Set
+_⊅_ = flip _⊄_
+
 ------------------------------------------------------------------------
 -- Set operations
 

src/Data/Fin/Subset/Induction.agda

@@ -10,8 +10,8 @@ module Data.Fin.Subset.Induction where
 
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Induction using (<-wellFounded)
-open import Data.Fin.Subset using (Subset; _⊂_; ∣_∣)
-open import Data.Fin.Subset.Properties using (p⊂q⇒∣p∣<∣q∣)
+open import Data.Fin.Subset using (Subset; ∁; _⊂_; _⊃_; ∣_∣)
+open import Data.Fin.Subset.Properties using (p⊂q⇒∣p∣<∣q∣; p⊂q⇒∁p⊃∁q)
 open import Induction using (RecStruct)
 open import Induction.WellFounded as WF
 open import Level using (Level)
@@ -36,3 +36,13 @@ open WF public using (Acc; acc)
 ⊂-wellFounded : WellFounded {A = Subset n} _⊂_
 ⊂-wellFounded = Subrelation.wellFounded p⊂q⇒∣p∣<∣q∣
   (On.wellFounded ∣_∣ <-wellFounded)
+
+------------------------------------------------------------------------
+-- Complete induction based on _⊃_
+
+⊃-Rec : RecStruct (Subset n) ℓ ℓ
+⊃-Rec = WfRec _⊃_
+
+⊃-wellFounded : WellFounded {A = Subset n} _⊃_
+⊃-wellFounded = Subrelation.wellFounded p⊂q⇒∁p⊃∁q
+  (On.wellFounded ∁ ⊂-wellFounded)

src/Data/Fin/Subset/Properties.agda

@@ -371,6 +371,18 @@ p∪∁p≡⊤ (inside  ∷ p) = cong (inside ∷_) (p∪∁p≡⊤ p)
   suc  _ ∸ ∣ p ∣  ∎
   where open ≡-Reasoning
 
+p⊆q⇒∁p⊇∁q : p ⊆ q → ∁ p ⊇ ∁ q
+p⊆q⇒∁p⊇∁q p⊆q x∈∁q = x∉p⇒x∈∁p (x∈∁p⇒x∉p x∈∁q ∘ p⊆q)
+
+∁p⊆∁q⇒p⊇q : ∁ p ⊆ ∁ q → p ⊇ q
+∁p⊆∁q⇒p⊇q ∁p⊆∁q x∈q = x∉∁p⇒x∈p (x∈p⇒x∉∁p x∈q ∘ ∁p⊆∁q)
+
+p⊂q⇒∁p⊃∁q : p ⊂ q → ∁ p ⊃ ∁ q
+p⊂q⇒∁p⊃∁q (p⊆q , x , x∈q , x∉p) = p⊆q⇒∁p⊇∁q p⊆q , x , x∉p⇒x∈∁p x∉p , x∈p⇒x∉∁p x∈q
+
+∁p⊂∁q⇒p⊃q : ∁ p ⊂ ∁ q → p ⊃ q
+∁p⊂∁q⇒p⊃q (∁p⊆∁q , x , x∈∁q , x∉∁p) = ∁p⊆∁q⇒p⊇q ∁p⊆∁q , x , x∉∁p⇒x∈p x∉∁p , x∈∁p⇒x∉p x∈∁q
+
 ------------------------------------------------------------------------
 -- _∩_