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