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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Documentation for List membership
------------------------------------------------------------------------
module README.Data.List.Membership where
open import Data.Char.Base using (Char; fromℕ)
open import Data.Char.Properties as Char hiding (setoid)
open import Data.List.Base using (List; []; _∷_; map)
open import Data.Nat as ℕ using (ℕ)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; cong; setoid)
------------------------------------------------------------------------
-- Membership
-- Membership of a list is simply a special case of `Any` where
-- `x ∈ xs` is defined as `Any (x ≈_) xs`.
-- Just like pointwise equality of lists, the exact membership module
-- that should be used depends on whether the equality on the
-- underlying elements of the list is i) propositional or setoid-based
-- and ii) decidable.
import Data.List.Membership.Setoid as SetoidMembership
import Data.List.Membership.DecSetoid as DecSetoidMembership
import Data.List.Membership.Propositional as PropMembership
import Data.List.Membership.DecPropositional as DecPropMembership
-- For example if we want to reason about membership for `List ℕ`
-- then you would use the `DecPropMembership` as we use
-- propositional equality over `ℕ` and it is also decidable. Therefore
-- the module `DecPropMembership` should be opened as follows:
open DecPropMembership ℕ._≟_
-- As membership is just an instance of `Any` we also need to import
-- the constructors `here` and `there`. (See issue #553 on Github for
-- why we're struggling to have `here` and `there` automatically
-- re-exported by the membership modules).
open import Data.List.Relation.Unary.Any using (here; there)
-- These modules provide the infix notation `_∈_` which can be used
-- as follows:
lem₁ : 1 ∈ 2 ∷ 1 ∷ 3 ∷ []
lem₁ = there (here refl)
-- Properties of the membership relation can be found in the following
-- two files:
import Data.List.Membership.Setoid.Properties as SetoidProperties
import Data.List.Membership.Propositional.Properties as PropProperties
-- As of yet there are no corresponding files for properties of
-- membership for decidable versions of setoid and propositional
-- equality as we have no properties that only hold when equality is
-- decidable.
-- These `Properties` modules are NOT parameterised in the same way as
-- the main membership modules as some of the properties relate
-- membership proofs for lists of different types. For example in the
-- following the first `∈` refers to lists of type `List ℕ` whereas
-- the second `∈` refers to lists of type `List Char`.
open DecPropMembership Char._≟_ renaming (_∈_ to _∈ᶜ_)
open SetoidProperties using (∈-map⁺)
lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs
lem₂ = ∈-map⁺ (setoid ℕ) (setoid Char) (cong fromℕ)
|
