|
17
|
1 module list-nat where
|
|
|
2
|
|
|
3 open import Level
|
|
15
|
4
|
|
|
5
|
|
130
|
6 postulate A : Set
|
|
|
7 postulate B : Set
|
|
|
8 postulate C : Set
|
|
15
|
9
|
|
130
|
10 postulate a : A
|
|
|
11 postulate b : A
|
|
|
12 postulate c : A
|
|
|
13 postulate d : B
|
|
15
|
14
|
|
|
15 infixr 40 _::_
|
|
130
|
16 data List (A : Set ) : Set where
|
|
15
|
17 [] : List A
|
|
|
18 _::_ : A -> List A -> List A
|
|
|
19
|
|
|
20
|
|
|
21 infixl 30 _++_
|
|
130
|
22 _++_ : {A : Set } -> List A -> List A -> List A
|
|
15
|
23 [] ++ ys = ys
|
|
|
24 (x :: xs) ++ ys = x :: (xs ++ ys)
|
|
|
25
|
|
|
26 l1 = a :: []
|
|
130
|
27 -- l1' = A :: []
|
|
15
|
28 l2 = a :: b :: a :: c :: []
|
|
|
29
|
|
|
30 l3 = l1 ++ l2
|
|
|
31
|
|
130
|
32 data Node ( A : Set ) : Set where
|
|
30
|
33 leaf : A -> Node A
|
|
|
34 node : Node A -> Node A -> Node A
|
|
|
35
|
|
130
|
36 flatten : { A : Set } -> Node A -> List A
|
|
30
|
37 flatten ( leaf a ) = a :: []
|
|
|
38 flatten ( node a b ) = flatten a ++ flatten b
|
|
|
39
|
|
|
40 n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c ))
|
|
|
41
|
|
18
|
42 open import Relation.Binary.PropositionalEquality
|
|
|
43
|
|
15
|
44 infixr 20 _==_
|
|
|
45
|
|
130
|
46 data _==_ {A : Set } : List A -> List A -> Set where
|
|
15
|
47 reflection : {x : List A} -> x == x
|
|
19
|
48
|
|
130
|
49 cong1 : {A : Set } { B : Set } ->
|
|
19
|
50 ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
|
|
|
51 cong1 f reflection = reflection
|
|
|
52
|
|
130
|
53 eq-cons : {A : Set } {x y : List A} ( a : A ) -> x == y -> ( a :: x ) == ( a :: y )
|
|
19
|
54 eq-cons a z = cong1 ( \x -> ( a :: x) ) z
|
|
|
55
|
|
130
|
56 trans-list : {A : Set } {x y z : List A} -> x == y -> y == z -> x == z
|
|
19
|
57 trans-list reflection reflection = reflection
|
|
18
|
58
|
|
|
59
|
|
130
|
60 ==-to-≡ : {A : Set } {x y : List A} -> x == y -> x ≡ y
|
|
19
|
61 ==-to-≡ reflection = refl
|
|
15
|
62
|
|
|
63 list-id-l : { A : Set } -> { x : List A} -> [] ++ x == x
|
|
|
64 list-id-l = reflection
|
|
|
65
|
|
|
66 list-id-r : { A : Set } -> ( x : List A ) -> x ++ [] == x
|
|
|
67 list-id-r [] = reflection
|
|
19
|
68 list-id-r (x :: xs) = eq-cons x ( list-id-r xs )
|
|
15
|
69
|
|
|
70 list-assoc : {A : Set } -> ( xs ys zs : List A ) ->
|
|
|
71 ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
|
|
|
72 list-assoc [] ys zs = reflection
|
|
19
|
73 list-assoc (x :: xs) ys zs = eq-cons x ( list-assoc xs ys zs )
|
|
15
|
74
|
|
18
|
75
|
|
130
|
76 module ==-Reasoning (A : Set ) where
|
|
17
|
77
|
|
|
78 infixr 2 _∎
|
|
30
|
79 infixr 2 _==⟨_⟩_ _==⟨⟩_
|
|
17
|
80 infix 1 begin_
|
|
15
|
81
|
|
|
82
|
|
19
|
83 data _IsRelatedTo_ (x y : List A) :
|
|
130
|
84 Set where
|
|
18
|
85 relTo : (x≈y : x == y ) → x IsRelatedTo y
|
|
17
|
86
|
|
19
|
87 begin_ : {x : List A } {y : List A} →
|
|
18
|
88 x IsRelatedTo y → x == y
|
|
17
|
89 begin relTo x≈y = x≈y
|
|
|
90
|
|
19
|
91 _==⟨_⟩_ : (x : List A ) {y z : List A} →
|
|
17
|
92 x == y → y IsRelatedTo z → x IsRelatedTo z
|
|
19
|
93 _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)
|
|
18
|
94
|
|
30
|
95 _==⟨⟩_ : (x : List A ) {y : List A}
|
|
|
96 → x IsRelatedTo y → x IsRelatedTo y
|
|
|
97 _ ==⟨⟩ x≈y = x≈y
|
|
|
98
|
|
20
|
99 _∎ : (x : List A ) → x IsRelatedTo x
|
|
18
|
100 _∎ _ = relTo reflection
|
|
17
|
101
|
|
130
|
102 lemma11 : (A : Set ) ( x : List A ) -> x == x
|
|
19
|
103 lemma11 A x = let open ==-Reasoning A in
|
|
18
|
104 begin x ∎
|
|
|
105
|
|
130
|
106 ++-assoc : (L : Set ) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs == xs ++ (ys ++ zs)
|
|
19
|
107 ++-assoc A [] ys zs = let open ==-Reasoning A in
|
|
17
|
108 begin -- to prove ([] ++ ys) ++ zs == [] ++ (ys ++ zs)
|
|
15
|
109 ( [] ++ ys ) ++ zs
|
|
17
|
110 ==⟨ reflection ⟩
|
|
15
|
111 ys ++ zs
|
|
17
|
112 ==⟨ reflection ⟩
|
|
15
|
113 [] ++ ( ys ++ zs )
|
|
|
114 ∎
|
|
17
|
115
|
|
19
|
116 ++-assoc A (x :: xs) ys zs = let open ==-Reasoning A in
|
|
17
|
117 begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)
|
|
15
|
118 ((x :: xs) ++ ys) ++ zs
|
|
17
|
119 ==⟨ reflection ⟩
|
|
15
|
120 (x :: (xs ++ ys)) ++ zs
|
|
17
|
121 ==⟨ reflection ⟩
|
|
15
|
122 x :: ((xs ++ ys) ++ zs)
|
|
19
|
123 ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
|
|
15
|
124 x :: (xs ++ (ys ++ zs))
|
|
17
|
125 ==⟨ reflection ⟩
|
|
15
|
126 (x :: xs) ++ (ys ++ zs)
|
|
|
127 ∎
|
|
|
128
|
|
|
129
|
