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