Add documentation for subset relation on lists (#1267)

Author: doyougnu

CHANGELOG.md

@@ -565,14 +565,16 @@ Other minor additions
 * Added new proof to `Data.List.Relation.Binary.Subset.Setoid.Properties`:
   ```agda
   xs⊆x∷xs    : xs ⊆ x ∷ xs
-  ∷⁺ʳ        : xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
+  ∷⁺ʳ        : xs ⊆ ys → x ∷ xs ⊆ x ∷ ys  
+  ∈-∷⁺ʳ      : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
   applyUpTo⁺ : m ≤ n → applyUpTo f m ⊆ applyUpTo f n
   ```
 
 * Added new proof to `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```agda
   xs⊆x∷xs    : xs ⊆ x ∷ xs
   ∷⁺ʳ        : xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
+  ∈-∷⁺ʳ      : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
   applyUpTo⁺ : m ≤ n → applyUpTo f m ⊆ applyUpTo f n
   ```
 

README/Data/List.agda

@@ -141,6 +141,15 @@ import README.Data.List.Relation.Binary.Equality
 
 import README.Data.List.Relation.Binary.Permutation
 
+------------------------------------------------------------------------
+-- Subsets
+
+-- Instead one might want to order lists by the subset relation which
+-- forms a partial order over lists. One list is a subset of another if
+-- every element in the first list occurs at least once in the second.
+
+import README.Data.List.Relation.Binary.Subset
+
 ------------------------------------------------------------------------
 -- Other binary relations
 
@@ -155,11 +164,7 @@ import Data.List.Relation.Binary.Lex.Strict
 
 import Data.List.Relation.Binary.BagAndSetEquality
 
---    3. the subset relations.
-
-import Data.List.Relation.Binary.Subset.Propositional
-
---    4. the sublist relations
+--    3. the sublist relations
 
 import Data.List.Relation.Binary.Sublist.Propositional
 

README/Data/List/Relation/Binary/Subset.agda

@@ -0,0 +1,56 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Documentation for subset relations over `List`s
+------------------------------------------------------------------------
+
+open import Data.List using (List; _∷_; [])
+open import Data.List.Membership.Propositional.Properties
+  using (∈-++⁺ˡ; ∈-insert)
+open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Relation.Binary.PropositionalEquality using (refl)
+
+module README.Data.List.Relation.Binary.Subset where
+
+------------------------------------------------------------------------
+-- Subset Relation
+
+-- The Subset relation is a wrapper over `Any` and so is parameterized
+-- over an equality relation. Thus to use the subset relation we must
+-- tell Agda which equality relation to use.
+
+-- Decidable equality over Strings
+open import Data.String using (String; _≟_)
+
+-- Open the decidable membership module using Decidable ≡ over Strings
+open import Data.List.Membership.DecPropositional _≟_
+
+
+-- Simple cases are inductive proofs
+
+lem₁ : ∀ {xs : List String} → xs ⊆ xs
+lem₁ p = p
+
+lem₂ : "A" ∷ [] ⊆ "B" ∷ "A" ∷ []
+lem₂ p = there p
+
+-- Or directly use the definition of subsets
+
+lem₃₀ : "E" ∷ "S" ∷ "B" ∷ [] ⊆ "S" ∷ "U" ∷ "B" ∷ "S" ∷ "E" ∷ "T" ∷ []
+lem₃₀ (here refl) = there (there (there (there (here refl))))  -- "E"
+lem₃₀ (there (here refl)) = here refl                          -- "S"
+lem₃₀ (there (there (here refl))) = there (there (here refl))  -- "B"
+
+-- Or use proofs from `Data.List.Membership.Propositional.Properties`
+
+lem₄ : "A" ∷  [] ⊆ "B" ∷ "A" ∷ "C" ∷ []
+lem₄ p = ∈-++⁺ˡ (there p)
+
+lem₅ : "B" ∷ "S" ∷ "E" ∷ [] ⊆ "S" ∷ "U" ∷ "B" ∷ "S" ∷ "E" ∷ "T" ∷ []
+lem₅ p = ∈-++⁺ˡ (there (there p))
+
+lem₃₁ : "E" ∷ "S" ∷ "B" ∷ [] ⊆ "S" ∷ "U" ∷ "B" ∷ "S" ∷ "E" ∷ "T" ∷ []
+lem₃₁ (here refl) = ∈-insert ("S" ∷ "U" ∷ "B" ∷ "S" ∷ [])
+lem₃₁ (there (here refl)) = here refl
+lem₃₁ (there (there (here refl))) = ∈-insert ("S" ∷ "U" ∷ [])

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

@@ -142,6 +142,9 @@ xs⊆x∷xs = Setoidₚ.xs⊆x∷xs (setoid _)
 ∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
 ∷⁺ʳ = Setoidₚ.∷⁺ʳ (setoid _)
 
+∈-∷⁺ʳ : ∀ {x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
+∈-∷⁺ʳ = Setoidₚ.∈-∷⁺ʳ (setoid _)
+
 ------------------------------------------------------------------------
 -- _++_
 

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

@@ -175,7 +175,9 @@ module _ (S : Setoid a ℓ) where
 
 module _ (S : Setoid a ℓ) where
 
+  open Setoid S
   open Subset S
+  open Membership S
 
   xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs
   xs⊆x∷xs xs x = there
@@ -184,6 +186,11 @@ module _ (S : Setoid a ℓ) where
   ∷⁺ʳ x xs⊆ys (here  p) = here p
   ∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p)
 
+  ∈-∷⁺ʳ : ∀ {xs ys x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
+  ∈-∷⁺ʳ x∈ys _  (here  v≈x)  = ∈-resp-≈ S (sym v≈x) x∈ys
+  ∈-∷⁺ʳ _ xs⊆ys (there x∈xs) = xs⊆ys x∈xs
+
+------------------------------------------------------------------------
 -- ++
 
 module _ (S : Setoid a ℓ) where