Mercurial > hg > Members > kono > Proof > category
annotate system-f.agda @ 333:26f44a4fa494
factorial still have a problem
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Mar 2014 14:55:51 +0700 |
| parents | fa179abb6161 |
| children | 357d3114c9b5 |
| rev | line source |
|---|---|
| 315 | 1 open import Level |
| 2 open import Relation.Binary.PropositionalEquality | |
| 3 | |
| 330 | 4 module system-f where |
| 315 | 5 |
| 331 | 6 Bool : {l : Level} (X : Set l) -> Set l |
| 7 Bool = \{l : Level} -> \(X : Set l) -> X -> X -> X | |
| 315 | 8 |
| 331 | 9 T : {l : Level} (X : Set l) -> Bool X |
| 10 T X = \(x y : X) -> x | |
| 315 | 11 |
| 331 | 12 F : {l : Level} (X : Set l) -> Bool X |
| 13 F X = \(x y : X) -> y | |
| 315 | 14 |
| 331 | 15 D : {l : Level} -> {U : Set l} -> U -> U -> Bool U -> U |
| 16 D u v t = t u v | |
| 315 | 17 |
| 331 | 18 lemma04 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (T U ) ≡ u |
| 315 | 19 lemma04 = refl |
| 20 | |
| 331 | 21 lemma05 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (F U ) ≡ v |
| 315 | 22 lemma05 = refl |
| 23 | |
| 321 | 24 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l) |
| 25 _×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X | |
| 315 | 26 |
| 321 | 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 |
| 321 | 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 |
| 321 | 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 |
| 330 | 36 lemma06 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡ u |
| 315 | 37 lemma06 = refl |
| 38 | |
| 330 | 39 lemma07 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡ v |
| 315 | 40 lemma07 = refl |
| 41 | |
| 330 | 42 hoge : {l : Level} {U V : Set l} -> U -> V -> (U × V) |
| 315 | 43 hoge u v = < u , v > |
| 44 | |
| 45 -- lemma08 : (t : U × V) -> < π1 t , π2 t > ≡ t | |
| 46 -- lemma08 t = {!!} | |
| 316 | 47 |
| 48 -- Emp definision is still wrong... | |
| 49 | |
| 327 | 50 Emp : {l : Level} {X : Set l} -> Set l |
| 51 Emp {l} = \{X : Set l} -> X | |
| 316 | 52 |
| 327 | 53 -- ε : {l : Level} (U : Set l) {l' : Level} {U' : Set l'} -> Emp -> Emp |
| 54 -- ε {l} U t = t | |
| 316 | 55 |
| 327 | 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 |
| 327 | 59 -- lemma10 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> U × V |
| 60 -- lemma10 {l} {U} {V} t = ε (U × V) t | |
| 316 | 61 |
| 327 | 62 -- lemma10' : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> Emp |
| 63 -- lemma10' {l} {U} {V} {X} t = ε (U × V) t | |
| 64 | |
| 65 -- lemma100 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U}) -> Emp | |
| 322 | 66 -- lemma100 {l} {U} {V} t = ε U t |
| 321 | 67 |
| 327 | 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 |
| 327 | 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 |
| 327 | 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 |
| 330 | 77 _+_ : {l : Level} -> Set l -> Set l -> Set (suc l) |
| 78 _+_ {l} U V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X | |
| 316 | 79 |
| 330 | 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 |
| 330 | 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 |
| 330 | 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 |
| 330 | 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 | |
| 330 | 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 | |
| 322 | 96 _××_ : {l : Level} -> Set (suc l) -> Set l -> Set (suc l) |
| 97 _××_ {l} U V = {X : Set l} -> (U -> V -> X) -> X | |
| 98 | |
| 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 | |
| 331 | 103 Int : {l : Level } ( X : Set l ) -> Set l |
| 104 Int {l} X = X -> ( X -> X ) -> X | |
| 322 | 105 |
| 331 | 106 Zero : {l : Level } -> { X : Set l } -> Int X |
| 322 | 107 Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x |
| 108 | |
| 331 | 109 S : {l : Level } -> { X : Set l } -> Int X -> Int X |
| 322 | 110 S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y ) |
| 111 | |
| 331 | 112 n0 : {l : Level} {X : Set l} -> Int X |
| 113 n0 = Zero | |
| 326 | 114 |
| 331 | 115 n1 : {l : Level } -> { X : Set l } -> Int X |
| 116 n1 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y x | |
| 322 | 117 |
| 331 | 118 n2 : {l : Level } -> { X : Set l } -> Int X |
| 119 n2 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x) | |
| 322 | 120 |
| 331 | 121 n3 : {l : Level } -> { X : Set l } -> Int X |
| 122 n3 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x)) | |
| 323 | 123 |
|
333
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
124 n4 : {l : Level } -> { X : Set l } -> Int X |
|
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
125 n4 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y (y x))) |
|
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
126 |
| 331 | 127 lemma13 : {l : Level } -> { X : Set l } -> S (S (Zero {_} {X})) ≡ n2 |
| 128 lemma13 = refl | |
| 322 | 129 |
| 331 | 130 It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int U -> U |
|
333
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
131 It {l} {U} u f t = t u f |
| 316 | 132 |
| 331 | 133 R : {l : Level} { U X : Set l} -> U -> ( U -> Int X -> U ) -> Int _ -> U |
| 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 |
| 331 | 136 add : {l : Level} {X : Set l} -> Int (Int X) -> Int X -> Int X |
| 332 | 137 add x y = It y S x |
| 323 | 138 |
| 331 | 139 mul : {l : Level } {X : Set l} -> Int (Int X) -> Int (Int X) -> Int X |
| 332 | 140 mul {l} {X} x y = It Zero (add x) y |
| 324 | 141 |
|
333
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
142 -- fact : {l : Level} {X : Set l} -> Int _ -> Int X |
|
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
143 -- fact {l} {X} n = R (S Zero) (λ (z : Int _) -> λ w -> mul z (S w) ) n |
| 326 | 144 |
|
333
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
145 -- lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n4 ≡ mul n4 ( mul n2 n3) |
|
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
146 -- lemma13' = refl |
| 324 | 147 |
| 148 -- lemma14 : (x y : Int) -> mul x y ≡ mul y x | |
| 326 | 149 -- lemma14 x y = It {!!} {!!} {!!} |
| 323 | 150 |
|
333
26f44a4fa494
factorial still have a problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
332
diff
changeset
|
151 lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2 |
| 324 | 152 lemma15 x y = refl |
| 323 | 153 |
| 331 | 154 lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int X -> U ) -> R u v Zero ≡ u |
| 324 | 155 lemma16 u v = refl |
| 156 | |
| 157 -- 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 | |
| 158 -- lemma17 u v t = refl | |
| 159 | |
| 160 -- postulate 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 | |
| 316 | 161 |
| 331 | 162 List : {l : Level} (U X : Set l) -> Set l |
| 163 List {l} = \( U X : Set l) -> X -> ( U -> X -> X ) -> X | |
| 323 | 164 |
| 331 | 165 Nil : {l : Level} {U : Set l} {X : Set l} -> List U X |
| 325 | 166 Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x |
| 167 | |
| 331 | 168 Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List U X -> List U X |
| 325 | 169 Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y ) |
| 170 | |
| 331 | 171 l0 : {l : Level} {X X' : Set l} -> List (Int X) (X') |
| 325 | 172 l0 = Nil |
| 173 | |
| 331 | 174 l1 : {l : Level} {X X' : Set l} -> List (Int X) (X') |
| 325 | 175 l1 = Cons n1 Nil |
| 176 | |
| 331 | 177 l2 : {l : Level} {X X' : Set l} -> List (Int X) (X') |
| 325 | 178 l2 = Cons n2 l1 |
| 323 | 179 |
| 331 | 180 l3 : {l : Level} {X X' : Set l} -> List (Int X) (X') |
| 330 | 181 l3 = Cons n3 l2 |
| 182 | |
| 331 | 183 ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List U W -> W |
| 184 ListIt w f t = t w f | |
| 323 | 185 |
| 331 | 186 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List U (Bool X) -> Bool _ |
| 187 Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (\u w -> (F X)) list | |
| 325 | 188 |
| 331 | 189 Append : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X -> List U _ |
| 190 Append x y = \s t -> x (y s t) t | |
| 325 | 191 |
| 331 | 192 lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil)) |
| 328 | 193 lemma18 = refl |
| 326 | 194 |
| 331 | 195 Reverse : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X |
| 196 Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( \u w -> Append w (Cons u Nil) ) x | |
| 330 | 197 |
| 331 | 198 lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil)) |
| 330 | 199 lemma19 = refl |
| 200 | |
| 331 | 201 Tree : {l : Level} -> Set l -> Set l -> Set l |
| 202 Tree {l} = \( U X : Set l) -> X -> ( (U -> X) -> X ) -> X | |
| 325 | 203 |
| 331 | 204 NilTree : {l : Level} (U : Set l) (X : Set l) -> Tree U X |
| 205 NilTree U X = \(x : X) -> \(y : (U -> X) -> X) -> x | |
| 325 | 206 |
| 331 | 207 Collect : {l : Level} (U : Set l) (X : Set l) -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree U X |
| 208 Collect U X f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y ) | |
| 325 | 209 |
| 331 | 210 TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree U W -> W |
| 211 TreeIt w h t = t w h |