1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Documentation for subset relations over `List`s
------------------------------------------------------------------------
open import Data.List.Base 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.Base using (String)
open import Data.String.Properties using (_≟_)
-- 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" ∷ [])
|
