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