Mercurial > hg > Members > kono > Proof > category
annotate src/system-t.agda @ 1110:45de2b31bf02
add original library and fix for safe mode
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 07 Oct 2023 19:43:31 +0900 |
parents | ac53803b3b2a |
children |
rev | line source |
---|---|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
949
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
949
diff
changeset
|
2 |
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
949
diff
changeset
|
3 module system-t (U : Set) (V : Set) (v : V) (u : U) where |
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
949
diff
changeset
|
4 |
315 | 5 open import Relation.Binary.PropositionalEquality |
6 | |
7 record _×_ ( U : Set ) ( V : Set ) : Set where | |
8 field | |
9 π1 : U | |
10 π2 : V | |
11 | |
346 | 12 <_,_> : {U V : Set} → U → V → U × V |
315 | 13 < u , v > = record {π1 = u ; π2 = v } |
14 | |
15 open _×_ | |
16 | |
17 | |
346 | 18 f : U → V |
19 f = λ u → v | |
315 | 20 |
21 | |
22 UV : Set | |
23 UV = U × V | |
24 | |
25 uv : U × V | |
26 uv = < u , v > | |
27 | |
28 lemma01 : π1 < u , v > ≡ u | |
29 lemma01 = refl | |
30 | |
31 lemma02 : π2 < u , v > ≡ v | |
32 lemma02 = refl | |
33 | |
34 lemma03 : (uv : U × V ) → < π1 uv , π2 uv > ≡ uv | |
35 lemma03 uv = refl | |
36 | |
37 lemma04 : (λ x → f x ) u ≡ f u | |
38 lemma04 = refl | |
39 | |
40 lemma05 : (λ x → f x ) ≡ f | |
41 lemma05 = refl | |
42 | |
43 nn = λ (x : U ) → u | |
44 n1 = λ ( x : U ) → f x | |
45 | |
46 data Bool : Set where | |
47 T : Bool | |
48 F : Bool | |
49 | |
346 | 50 D : { U : Set } → U → U → Bool → U |
315 | 51 D u v T = u |
52 D u v F = v | |
53 | |
54 data Int : Set where | |
55 zero : Int | |
56 S : Int → Int | |
57 | |
346 | 58 pred : Int → Int |
315 | 59 pred zero = zero |
60 pred (S t) = t | |
61 | |
346 | 62 R : { U : Set } → U → ( U → Int → U ) → Int → U |
315 | 63 R u v zero = u |
64 R u v ( S t ) = v (R u v t) t | |
65 | |
346 | 66 null : Int → Bool |
315 | 67 null zero = T |
68 null (S _) = F | |
69 | |
346 | 70 It : { T : Set } → T → (T → T) → Int → T |
315 | 71 It u v zero = u |
72 It u v ( S t ) = v (It u v t ) | |
73 | |
346 | 74 R' : { T : Set } → T → ( T → Int → T ) → Int → T |
315 | 75 R' u v t = π1 ( It ( < u , zero > ) (λ x → < v (π1 x) (π2 x) , S (π2 x) > ) t ) |
76 | |
346 | 77 sum : Int → Int → Int |
78 sum x y = R y ( λ z → λ w → S z ) x | |
315 | 79 |
605
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
80 sum2 : Int → Int → Int |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
81 sum2 zero x = x |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
82 sum2 (S x) y = S ( sum2 x y ) |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
83 |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
84 cong1 : { x y : Int } -> ( f : Int -> Int ) -> x ≡ y -> f x ≡ f y |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
85 cong1 {x} {.x} f refl = refl |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
86 |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
87 lemma1 : ( x y : Int ) → sum x y ≡ sum2 x y |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
88 lemma1 zero y = refl |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
89 lemma1 (S x) y = cong1 ( λ z -> S z ) ( lemma1 x y ) |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
346
diff
changeset
|
90 |
346 | 91 mul : Int → Int → Int |
92 mul x y = R zero ( λ z → λ w → sum y z ) x | |
315 | 93 |
346 | 94 sum' : Int → Int → Int |
95 sum' x y = R' y ( λ z → λ w → S z ) x | |
315 | 96 |
346 | 97 mul' : Int → Int → Int |
98 mul' x y = R' zero ( λ z → λ w → sum y z ) x | |
315 | 99 |
346 | 100 fact : Int → Int |
101 fact n = R (S zero) (λ z → λ w → mul (S w) z ) n | |
315 | 102 |
346 | 103 fact' : Int → Int |
104 fact' n = R' (S zero) (λ z → λ w → mul (S w) z ) n | |
315 | 105 |
106 f3 = fact (S (S (S zero))) | |
107 f3' = fact' (S (S (S zero))) | |
108 | |
109 lemma21 : f3 ≡ f3' | |
110 lemma21 = refl | |
111 | |
346 | 112 lemma07 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → |
315 | 113 (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t )) ≡ t |
114 lemma07 u v zero = refl | |
346 | 115 lemma07 u v (S t) = cong ( λ x → S x ) ( lemma07 u v t ) |
315 | 116 |
346 | 117 lemma06 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → ( (R u v t) ≡ (R' u v t )) |
315 | 118 lemma06 u v zero = refl |
346 | 119 lemma06 u v (S t) = trans ( cong ( λ x → v x t ) ( lemma06 u v t ) ) |
120 ( cong ( λ y → v (R' u v t) y ) (sym ( lemma07 u v t ) ) ) | |
315 | 121 |
346 | 122 lemma08 : ( n m : Int ) → ( sum' n m ≡ sum n m ) |
315 | 123 lemma08 zero _ = refl |
346 | 124 lemma08 (S t) y = cong ( λ x → S x ) ( lemma08 t y ) |
315 | 125 |
346 | 126 lemma09 : ( n m : Int ) → ( mul' n m ≡ mul n m ) |
315 | 127 lemma09 zero _ = refl |
346 | 128 lemma09 (S t) y = cong ( λ x → sum y x) ( lemma09 t y ) |
315 | 129 |
346 | 130 lemma10 : ( n : Int ) → ( fact n ≡ fact n ) |
315 | 131 lemma10 zero = refl |
346 | 132 lemma10 (S t) = cong ( λ x → mul (S t) x ) ( lemma10 t ) |
315 | 133 |
346 | 134 lemma11 : ( n : Int ) → ( fact n ≡ fact' n ) |
135 lemma11 n = lemma06 (S zero) (λ z → λ w → mul (S w) z ) n | |
315 | 136 |
346 | 137 lemma06' : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t : Int ) → ( (R u v t) ≡ (R' u v t )) |
315 | 138 lemma06' u v zero = refl |
139 lemma06' u v (S t) = let open ≡-Reasoning in | |
140 begin | |
141 R u v (S t) | |
142 ≡⟨⟩ | |
143 v (R u v t) t | |
346 | 144 ≡⟨ cong (λ x → v x t ) ( lemma06' u v t ) ⟩ |
315 | 145 v (R' u v t) t |
346 | 146 ≡⟨ cong (λ x → v (R' u v t) x ) ( sym ( lemma07 u v t )) ⟩ |
315 | 147 v (R' u v t) (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t)) |
148 ≡⟨⟩ | |
149 R' u v (S t) | |
150 ∎ | |
151 | |
152 | |
346 | 153 sum1 : (x y : Int) → sum x (S y) ≡ S (sum x y ) |
154 sum1 zero y = refl | |
155 sum1 (S x) y = cong (λ x → S x ) (sum1 x y ) | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
156 |
346 | 157 sum-sym : (x y : Int) → sum x y ≡ sum y x |
158 sum-sym zero zero = refl | |
159 sum-sym zero (S t) = cong (λ x → S x )( sum-sym zero t) | |
160 sum-sym (S t) zero = cong (λ x → S x ) ( sum-sym t zero ) | |
161 sum-sym (S t) (S t') = let open ≡-Reasoning in | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
162 begin |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
163 sum (S t) (S t') |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
164 ≡⟨⟩ |
339 | 165 S (sum t (S t')) |
346 | 166 ≡⟨ cong ( λ x → S x ) ( sum1 t t') ⟩ |
339 | 167 S ( S (sum t t')) |
346 | 168 ≡⟨ cong ( λ x → S (S x ) ) ( sum-sym t t') ⟩ |
339 | 169 S ( S (sum t' t)) |
346 | 170 ≡⟨ sym ( cong ( λ x → S x ) ( sum1 t' t)) ⟩ |
339 | 171 S (sum t' (S t)) |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
172 ≡⟨⟩ |
346 | 173 R (S t) ( λ z → λ w → S z ) (S t') |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
174 ≡⟨⟩ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
175 sum (S t') (S t) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
176 ∎ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
177 |
346 | 178 sum-assoc : (x y z : Int) → sum x (sum y z ) ≡ sum (sum x y) z |
179 sum-assoc zero y z = refl | |
180 sum-assoc (S x) y z = let open ≡-Reasoning in | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
181 begin |
339 | 182 sum (S x) ( sum y z ) |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
183 ≡⟨⟩ |
339 | 184 S ( sum x ( sum y z ) ) |
346 | 185 ≡⟨ cong (λ x → S x ) ( sum-assoc x y z) ⟩ |
339 | 186 S ( sum (sum x y) z ) |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
187 ≡⟨⟩ |
339 | 188 sum (S ( sum x y)) z |
189 ≡⟨⟩ | |
190 sum (sum (S x) y) z | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
191 ∎ |
315 | 192 |
346 | 193 mul-distr1 : (x y : Int) → mul x (S y) ≡ sum x ( mul x y ) |
194 mul-distr1 zero y = refl | |
195 mul-distr1 (S x) y = let open ≡-Reasoning in | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
196 begin |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
197 mul (S x) (S y) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
198 ≡⟨⟩ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
199 sum (S y) (mul x (S y)) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
200 ≡⟨⟩ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
201 S (sum y (mul x (S y) )) |
346 | 202 ≡⟨ cong (λ t → S ( sum y t )) (mul-distr1 x y ) ⟩ |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
203 S (sum y (sum x (mul x y))) |
346 | 204 ≡⟨ cong (λ x → S x ) ( |
339 | 205 begin |
206 sum y (sum x (mul x y)) | |
346 | 207 ≡⟨ sum-assoc y x (mul x y) ⟩ |
339 | 208 sum (sum y x) (mul x y) |
346 | 209 ≡⟨ cong (λ t → sum t (mul x y)) (sum-sym y x ) ⟩ |
339 | 210 sum (sum x y) (mul x y) |
346 | 211 ≡⟨ sym ( sum-assoc x y (mul x y)) ⟩ |
339 | 212 sum x (sum y (mul x y)) |
213 ∎ | |
214 ) ⟩ | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
215 S (sum x (sum y (mul x y) )) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
216 ≡⟨⟩ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
217 S (sum x (mul (S x) y ) ) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
218 ≡⟨⟩ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
219 sum (S x) (mul (S x) y) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
220 ∎ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
221 |
346 | 222 mul-sym0 : (x : Int) → mul zero x ≡ mul x zero |
223 mul-sym0 zero = refl | |
224 mul-sym0 (S x) = mul-sym0 x | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
225 |
346 | 226 mul-sym : (x y : Int) → mul x y ≡ mul y x |
227 mul-sym zero x = mul-sym0 x | |
228 mul-sym (S x) y = let open ≡-Reasoning in | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
229 begin |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
230 mul (S x) y |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
231 ≡⟨⟩ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
232 sum y (mul x y ) |
346 | 233 ≡⟨ cong ( λ x → sum y x ) (mul-sym x y ) ⟩ |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
234 sum y (mul y x) |
346 | 235 ≡⟨ sym ( mul-distr1 y x ) ⟩ |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
236 mul y (S x) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
237 ∎ |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
238 |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
239 |
346 | 240 mul-ditr : (y z w : Int) → sum (mul y z) ( mul w z ) ≡ mul (sum y w) z |
241 mul-ditr y zero w = let open ≡-Reasoning in | |
339 | 242 begin |
243 sum (mul y zero) ( mul w zero ) | |
346 | 244 ≡⟨ cong ( λ t → sum (mul y zero ) t ) (mul-sym w zero ) ⟩ |
339 | 245 sum (mul y zero ) ( mul zero w ) |
346 | 246 ≡⟨ cong ( λ t → sum t zero ) (mul-sym y zero ) ⟩ |
339 | 247 sum zero zero |
248 ≡⟨⟩ | |
249 mul zero (sum y w) | |
346 | 250 ≡⟨ mul-sym0 (sum y w) ⟩ |
339 | 251 mul (sum y w) zero |
252 ∎ | |
346 | 253 mul-ditr y (S z) w = let open ≡-Reasoning in |
339 | 254 begin |
255 sum (mul y (S z)) ( mul w (S z) ) | |
346 | 256 ≡⟨ cong ( λ t → sum t ( mul w (S z ))) (mul-distr1 y z) ⟩ |
339 | 257 sum ( sum y ( mul y z)) ( mul w (S z) ) |
346 | 258 ≡⟨ cong ( λ t → sum ( sum y ( mul y z)) t ) (mul-distr1 w z) ⟩ |
339 | 259 sum ( sum y ( mul y z)) ( sum w ( mul w z) ) |
346 | 260 ≡⟨ sym ( sum-assoc y (mul y z ) ( sum w ( mul w z) ) ) ⟩ |
339 | 261 sum y ( sum ( mul y z) ( sum w ( mul w z) )) |
346 | 262 ≡⟨ cong ( λ t → sum y t) (sum-sym ( mul y z) ( sum w ( mul w z) )) ⟩ |
339 | 263 sum y ( sum ( sum w ( mul w z) )( mul y z)) |
346 | 264 ≡⟨ sym ( cong ( λ t → sum y t) (sum-assoc w (mul w z) (mul y z )) ) ⟩ |
339 | 265 sum y ( sum w (sum ( mul w z) ( mul y z)) ) |
346 | 266 ≡⟨ cong ( λ t → sum y (sum w t) ) ( sum-sym (mul w z) (mul y z )) ⟩ |
339 | 267 sum y ( sum w (sum ( mul y z) ( mul w z)) ) |
346 | 268 ≡⟨ cong ( λ t → sum y (sum w t) ) ( mul-ditr y z w ) ⟩ |
339 | 269 sum y ( sum w (mul (sum y w) z) ) |
346 | 270 ≡⟨ sum-assoc y w (mul (sum y w) z) ⟩ |
339 | 271 sum (sum y w) ( mul (sum y w) z ) |
346 | 272 ≡⟨ sym ( mul-distr1 (sum y w) z ) ⟩ |
339 | 273 mul (sum y w) (S z) |
274 ∎ | |
275 | |
276 | |
346 | 277 mul-assoc : (x y z : Int) → mul x (mul y z ) ≡ mul (mul x y) z |
278 mul-assoc zero y z = refl | |
279 mul-assoc (S x) y z = let open ≡-Reasoning in | |
339 | 280 begin |
281 mul (S x) (mul y z ) | |
282 ≡⟨⟩ | |
283 sum (mul y z) ( mul x ( mul y z ) ) | |
346 | 284 ≡⟨ cong (λ t → sum (mul y z) t ) (mul-assoc x y z ) ⟩ |
339 | 285 sum (mul y z) ( mul ( mul x y) z ) |
346 | 286 ≡⟨ mul-ditr y z (mul x y) ⟩ |
339 | 287 mul (sum y (mul x y)) z |
288 ≡⟨⟩ | |
289 mul (mul (S x) y) z | |
290 ∎ | |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
291 |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
292 |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
324
diff
changeset
|
293 |
339 | 294 |