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
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Documentation for pointwise lifting of relations over `List`s
------------------------------------------------------------------------
module README.Data.List.Relation.Binary.Pointwise where
open import Data.Nat using (ℕ; _<_; s≤s; z≤n)
open import Data.List.Base using (List; []; _∷_; length)
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; sym; cong; setoid)
open import Relation.Nullary.Negation using (¬_)
------------------------------------------------------------------------
-- Pointwise
-- One of the most basic ways to form a binary relation between two
-- lists of type `List A`, given a binary relation over `A`, is to say
-- that two lists are related if they are the same length and:
-- i) the first elements in the lists are related
-- ii) the second elements in the lists are related
-- iii) the third elements in the lists are related etc.
-- etc.
--
-- A formalisation of this "pointwise" lifting of a relation to lists
-- is found in:
open import Data.List.Relation.Binary.Pointwise
-- The same syntax to construct a list (`[]` & `_∷_`) is used to
-- construct proofs for the `Pointwise` relation. For example if you
-- want to prove that one list is strictly less than another list:
lem₁ : Pointwise _<_ (0 ∷ 2 ∷ 1 ∷ []) (1 ∷ 4 ∷ 2 ∷ [])
lem₁ = 0<1 ∷ 2<4 ∷ 1<2 ∷ []
where
0<1 = s≤s z≤n
2<4 = s≤s (s≤s (s≤s z≤n))
1<2 = s≤s 0<1
-- Lists that are related by `Pointwise` must be of the same length.
-- For example:
lem₂ : ¬ Pointwise _<_ (0 ∷ 2 ∷ []) (1 ∷ [])
lem₂ (0<1 ∷ ())
-- Proofs about pointwise, including that of the above fact are
-- also included in the module:
lem₃ : ∀ {xs ys} → Pointwise _<_ xs ys → length xs ≡ length ys
lem₃ = Pointwise-length
|
