Mercurial > hg > Members > kono > Proof > category
annotate system-f.agda @ 338:2f21eb997559
sym of sum and mul in system T
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 29 Mar 2014 17:12:33 +0900 |
parents | 203593ff1e60 |
children | 716f85bc7259 |
rev | line source |
---|---|
315 | 1 open import Level |
2 open import Relation.Binary.PropositionalEquality | |
3 | |
330 | 4 module system-f where |
315 | 5 |
336 | 6 Bool : {l : Level} (X : Set l) → Set l |
7 Bool = λ{l : Level} → λ(X : Set l) → X → X → X | |
315 | 8 |
336 | 9 T : {l : Level} (X : Set l) → Bool X |
10 T X = λ(x y : X) → x | |
315 | 11 |
336 | 12 F : {l : Level} (X : Set l) → Bool X |
13 F X = λ(x y : X) → y | |
315 | 14 |
336 | 15 D : {l : Level} → {U : Set l} → U → U → Bool U → U |
331 | 16 D u v t = t u v |
315 | 17 |
336 | 18 lemma04 : {l : Level} { U : Set l} {u v : U} → D {_} {U} u v (T U ) ≡ u |
315 | 19 lemma04 = refl |
20 | |
336 | 21 lemma05 : {l : Level} { U : Set l} {u v : U} → D {_} {U} u v (F U ) ≡ v |
315 | 22 lemma05 = refl |
23 | |
336 | 24 _×_ : {l : Level} → Set l → Set l → Set (suc l) |
25 _×_ {l} U V = {X : Set l} → (U → V → X) → X | |
315 | 26 |
336 | 27 <_,_> : {l : Level} {U V : Set l} → U → V → (U × V) |
28 <_,_> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v | |
315 | 29 |
336 | 30 π1 : {l : Level} {U V : Set l} → (U × V) → U |
31 π1 {l} {U} {V} t = t {U} (λ(x : U) → λ(y : V) → x) | |
315 | 32 |
336 | 33 π2 : {l : Level} {U V : Set l} → (U × V) → V |
34 π2 {l} {U} {V} t = t {V} (λ(x : U) → λ(y : V) → y) | |
315 | 35 |
336 | 36 lemma06 : {l : Level} {U V : Set l } → {u : U } → {v : V} → π1 ( < u , v > ) ≡ u |
315 | 37 lemma06 = refl |
38 | |
336 | 39 lemma07 : {l : Level} {U V : Set l } → {u : U } → {v : V} → π2 ( < u , v > ) ≡ v |
315 | 40 lemma07 = refl |
41 | |
336 | 42 hoge : {l : Level} {U V : Set l} → U → V → (U × V) |
315 | 43 hoge u v = < u , v > |
44 | |
336 | 45 -- lemma08 : {l : Level} {U V : Set l } → {u : U } → (t : U × V) → < π1 t , π2 t > ≡ t |
46 -- lemma08 t = refl | |
316 | 47 |
48 -- Emp definision is still wrong... | |
49 | |
336 | 50 Emp : {l : Level} {X : Set l} → Set l |
51 Emp {l} = λ{X : Set l} → X | |
316 | 52 |
336 | 53 -- ε : {l : Level} (U : Set l) {l' : Level} {U' : Set l'} → Emp → Emp |
327 | 54 -- ε {l} U t = t |
316 | 55 |
336 | 56 -- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} → (t : Emp {l} {U} ) → ε U (ε Emp t) ≡ ε U t |
322 | 57 -- lemma09 t = refl |
321 | 58 |
336 | 59 -- lemma10 : {l : Level} {U V X : Set l} → (t : Emp {_} {U × V}) → U × V |
327 | 60 -- lemma10 {l} {U} {V} t = ε (U × V) t |
316 | 61 |
336 | 62 -- lemma10' : {l : Level} {U V X : Set l} → (t : Emp {_} {U × V}) → Emp |
327 | 63 -- lemma10' {l} {U} {V} {X} t = ε (U × V) t |
64 | |
336 | 65 -- lemma100 : {l : Level} {U V X : Set l} → (t : Emp {_} {U}) → Emp |
322 | 66 -- lemma100 {l} {U} {V} t = ε U t |
321 | 67 |
336 | 68 -- lemma101 : {l k : Level} {U V : Set l} → (t : Emp {_} {U × V}) → π1 (ε (U × V) t) ≡ ε U t |
322 | 69 -- lemma101 t = refl |
319 | 70 |
336 | 71 -- lemma102 : {l k : Level} {U V : Set l} → (t : Emp {_} {U × V}) → π2 (ε (U × V) t) ≡ ε V t |
322 | 72 -- lemma102 t = refl |
321 | 73 |
336 | 74 -- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} {_} ) → (ε (U → V) t) u ≡ ε V t |
322 | 75 -- lemma103 u t = refl |
316 | 76 |
336 | 77 _+_ : {l : Level} → Set l → Set l → Set (suc l) |
78 _+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X | |
316 | 79 |
336 | 80 ι1 : {l : Level } {U V : Set l} → U → U + V |
81 ι1 {l} {U} {V} u = λ{X} → λ(x : U → X) → λ(y : V → X ) → x u | |
316 | 82 |
336 | 83 ι2 : {l : Level } {U V : Set l} → V → U + V |
84 ι2 {l} {U} {V} v = λ{X} → λ(x : U → X) → λ(y : V → X ) → y v | |
316 | 85 |
336 | 86 δ : {l : Level} { U V R S : Set l } → (R → U) → (S → U) → ( R + S ) → U |
87 δ {l} {U} {V} {R} {S} u v t = t {U} (λ(x : R) → u x) ( λ(y : S) → v y) | |
316 | 88 |
336 | 89 lemma11 : {l : Level} { U V R S : Set _ } → (u : R → U ) (v : S → U ) → (r : R) → δ {l} {U} {V} {R} {S} u v ( ι1 r ) ≡ u r |
316 | 90 lemma11 u v r = refl |
91 | |
336 | 92 lemma12 : {l : Level} { U V R S : Set _ } → (u : R → U ) (v : S → U ) → (s : S) → δ {l} {U} {V} {R} {S} u v ( ι2 s ) ≡ v s |
316 | 93 lemma12 u v s = refl |
94 | |
95 | |
336 | 96 _××_ : {l : Level} → Set (suc l) → Set l → Set (suc l) |
97 _××_ {l} U V = {X : Set l} → (U → V → X) → X | |
322 | 98 |
336 | 99 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} → U → V → (U ×× V) |
100 <<_,_>> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v | |
316 | 101 |
102 | |
336 | 103 Int : {l : Level } ( X : Set l ) → Set l |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
104 Int X = X → ( X → X ) → X |
322 | 105 |
336 | 106 Zero : {l : Level } → { X : Set l } → Int X |
107 Zero {l} {X} = λ(x : X ) → λ(y : X → X ) → x | |
322 | 108 |
336 | 109 S : {l : Level } → { X : Set l } → Int X → Int X |
110 S {l} {X} t = λ(x : X) → λ(y : X → X ) → y ( t x y ) | |
322 | 111 |
336 | 112 n0 : {l : Level} {X : Set l} → Int X |
331 | 113 n0 = Zero |
326 | 114 |
336 | 115 n1 : {l : Level } → { X : Set l } → Int X |
116 n1 {_} {X} = λ(x : X ) → λ(y : X → X ) → y x | |
322 | 117 |
336 | 118 n2 : {l : Level } → { X : Set l } → Int X |
119 n2 {_} {X} = λ(x : X ) → λ(y : X → X ) → y (y x) | |
322 | 120 |
336 | 121 n3 : {l : Level } → { X : Set l } → Int X |
122 n3 {_} {X} = λ(x : X ) → λ(y : X → X ) → y (y (y x)) | |
323 | 123 |
336 | 124 n4 : {l : Level } → { X : Set l } → Int X |
125 n4 {_} {X} = λ(x : X ) → λ(y : X → X ) → y (y (y (y x))) | |
333
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
126 |
336 | 127 lemma13 : {l : Level } → { X : Set l } → S (S (Zero {_} {X})) ≡ n2 |
331 | 128 lemma13 = refl |
322 | 129 |
336 | 130 It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
131 It u f t = t u f |
316 | 132 |
336 | 133 R : {l : Level} { U X : Set l} → U → ( U → Int X → U ) → Int _ → U |
331 | 134 R {l} {U} {X} u v t = π1 ( It {suc l} {U × Int X} (< u , Zero >) (λ (x : U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t ) |
316 | 135 |
336 | 136 -- ItInt : {l : Level} {U : Set l} → Int U → ( Int U → Int U ) → Int U → Int U |
137 -- ItInt {l} {U} u f t = λt u f | |
323 | 138 |
336 | 139 -- RInt : {l : Level} { U X : Set l} → Int U → ( Int U → Int X → Int U ) → Int U → Int U |
140 -- RInt {l} {U} {X} u v t = π1 ( It {suc l} {Int U × Int X} (< u , Zero >) (λ (x : Int U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t ) | |
141 | |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
142 -- bad adder which modifies input type |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
143 add' : {l : Level} {X : Set l} → Int (Int X) → Int X → Int X |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
144 add' x y = It y S x |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
145 |
336 | 146 add : {l : Level} {X : Set l} → Int X → Int X → Int X |
147 add x y = λ z t → x (y z t) t | |
148 | |
149 mul : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X | |
332 | 150 mul {l} {X} x y = It Zero (add x) y |
324 | 151 |
338
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
152 -- λ x y → y y y y x |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
153 -- λ x y → y y y x |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
154 -- λ z t → (λ x y → y y y y x) (λ x y → y y y y x) (λ x y → y y y y x) t |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
155 -- λ z t → t t t t t t t t t t t t z |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
156 -- mul : {l : Level } {X : Set l} → Int X → Int X → Int X |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
157 -- mul {l} {X} x y = λ z t → x z ( λ w → y ? ? ) |
2f21eb997559
sym of sum and mul in system T
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
337
diff
changeset
|
158 |
336 | 159 fact : {l : Level} {X : Set l} → Int _ → Int X |
160 fact {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w) ) n | |
326 | 161 |
336 | 162 lemma13' : {l : Level} {X : Set l} → fact {l} {X} n4 ≡ mul n4 ( mul n2 n3) |
334
357d3114c9b5
add : Int X -> Int X -> Int X
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
333
diff
changeset
|
163 lemma13' = refl |
324 | 164 |
336 | 165 -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y ≡ mul y x |
326 | 166 -- lemma14 x y = It {!!} {!!} {!!} |
323 | 167 |
336 | 168 lemma15 : {l : Level} {X : Set l} (x y : Int X) → mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2 |
324 | 169 lemma15 x y = refl |
323 | 170 |
336 | 171 lemma16 : {l : Level} {X U : Set l} → (u : U ) → (v : U → Int X → U ) → R u v Zero ≡ u |
324 | 172 lemma16 u v = refl |
173 | |
336 | 174 -- lemma17 : {l : Level} {X U : Set l} → (u : U ) → (v : U → Int → U ) → (t : Int ) → R u v (S t) ≡ v ( R u v t ) t |
324 | 175 -- lemma17 u v t = refl |
176 | |
336 | 177 -- postulate lemma17 : {l : Level} {X U : Set l} → (u : U ) → (v : U → Int X → U ) → (t : Int X ) → R u v (S t) ≡ v ( R u v t ) t |
316 | 178 |
336 | 179 List : {l : Level} (U X : Set l) → Set l |
180 List {l} = λ( U X : Set l) → X → ( U → X → X ) → X | |
323 | 181 |
336 | 182 Nil : {l : Level} {U : Set l} {X : Set l} → List U X |
183 Nil {l} {U} {X} = λ(x : X) → λ(y : U → X → X) → x | |
325 | 184 |
336 | 185 Cons : {l : Level} {U : Set l} {X : Set l} → U → List U X → List U X |
186 Cons {l} {U} {X} u t = λ(x : X) → λ(y : U → X → X) → y u (t x y ) | |
325 | 187 |
336 | 188 l0 : {l : Level} {X X' : Set l} → List (Int X) (X') |
325 | 189 l0 = Nil |
190 | |
336 | 191 l1 : {l : Level} {X X' : Set l} → List (Int X) (X') |
325 | 192 l1 = Cons n1 Nil |
193 | |
336 | 194 l2 : {l : Level} {X X' : Set l} → List (Int X) (X') |
325 | 195 l2 = Cons n2 l1 |
323 | 196 |
336 | 197 l3 : {l : Level} {X X' : Set l} → List (Int X) (X') |
330 | 198 l3 = Cons n3 l2 |
199 | |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
200 ListIt : {l : Level} {U W : Set l} → (X : Set l) → W → ( U → W → W ) → List U W → W |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
201 ListIt _ w f t = t w f |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
202 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
203 -- Car : {l : Level} {U : Set l} {X : Set l} → List U _ → U → U |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
204 -- Car x z = ListIt z ( λ u w → u ) x |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
205 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
206 -- Cdr : {l : Level} {U : Set l} {X : Set l} → List U _ → List U X |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
207 -- Cdr w = λ x → λ y → w x (λ x y → y) |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
208 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
209 -- lemma181 :{l : Level} {U : Set l} {X : Set l} → Car Zero l2 ≡ n2 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
210 -- lemma181 = refl |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
211 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
212 -- lemma182 :{l : Level} {U : Set l} {X : Set l} → Cdr l2 ≡ l1 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
213 -- lemma182 = refl |
323 | 214 |
336 | 215 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} → List U (Bool X) → Bool _ |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
216 Nullp {_} {_} {X} list = ListIt X (T X) (λ u w → (F X)) list |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
217 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
218 -- bad append |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
219 Append' : {l : Level} {U X : Set l} → List U (List U X) → List U X → List U X |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
220 Append' {_} {_} {X} x y = ListIt X y Cons x |
325 | 221 |
336 | 222 Append : {l : Level} {U : Set l} {X : Set l} → List U X → List U X → List U X |
223 Append x y = λ s t → x (y s t) t | |
325 | 224 |
336 | 225 lemma18 :{l : Level} {U : Set l} {X : Set l} → Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil)) |
328 | 226 lemma18 = refl |
326 | 227 |
336 | 228 Reverse : {l : Level} {U : Set l} {X : Set l} → List U (List U X) → List U X |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
229 Reverse {l} {U} {X} x = ListIt X Nil ( λ u w → Append w (Cons u Nil) ) x |
330 | 230 |
336 | 231 lemma19 :{l : Level} {U : Set l} {X : Set l} → Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil)) |
330 | 232 lemma19 = refl |
233 | |
336 | 234 Tree : {l : Level} → Set l → Set l → Set l |
235 Tree {l} = λ( U X : Set l) → X → ( (U → X) → X ) → X | |
325 | 236 |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
237 NilTree : {l : Level} {U : Set l} {X : Set l} → Tree U X |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
238 NilTree {l} {U} {X} = λ(x : X) → λ(y : (U → X) → X) → x |
325 | 239 |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
240 Collect : {l : Level} {U : Set l} {X : Set l} → (U → Tree U X ) → Tree U X |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
241 Collect {l} {U} {X} f = λ(x : X) → λ(y : (U → X) → X) → y (λ(z : U) → f z x y ) |
325 | 242 |
336 | 243 TreeIt : {l : Level} {U W X : Set l} → W → ( (U → W) → W ) → Tree U W → W |
331 | 244 TreeIt w h t = t w h |
337
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
245 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
246 t0 : {l : Level} {X X' : Set l} → Tree (Bool X) X' |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
247 t0 {l} {X} {X'} = NilTree |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
248 |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
249 t1 : {l : Level} {X X' : Set l} → Tree (Bool X) X' |
203593ff1e60
add Tree example ( not yet worked )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
336
diff
changeset
|
250 t1 {l} {X} {X'} = NilTree -- Collect (λ b → D b NilTree (λ c → Collect NilTree NilTree )) |