Mercurial > hg > Members > kono > Proof > category
annotate system-f.agda @ 329:c4514e0cf0e2
no yellow on append example
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Mar 2014 09:31:46 +0700 |
| parents | d6eb3520ccf8 |
| children | fa018eb1723e |
| rev | line source |
|---|---|
| 315 | 1 open import Level |
| 2 open import Relation.Binary.PropositionalEquality | |
| 3 | |
| 4 module system-f {l : Level} where | |
| 5 | |
| 6 postulate A : Set | |
| 7 postulate B : Set | |
| 8 | |
| 9 data _∨_ (A B : Set) : Set where | |
| 10 or1 : A -> A ∨ B | |
| 11 or2 : B -> A ∨ B | |
| 12 | |
| 13 lemma01 : A -> A ∨ B | |
| 14 lemma01 a = or1 a | |
| 15 | |
| 16 lemma02 : B -> A ∨ B | |
| 17 lemma02 b = or2 b | |
| 18 | |
| 19 lemma03 : {C : Set} -> (A ∨ B) -> (A -> C) -> (B -> C) -> C | |
| 20 lemma03 (or1 a) ac bc = ac a | |
| 21 lemma03 (or2 b) ac bc = bc b | |
| 22 | |
| 23 postulate U : Set l | |
| 24 postulate V : Set l | |
| 25 | |
| 26 | |
| 325 | 27 Bool = \{l : Level} -> {X : Set l} -> X -> X -> X |
| 315 | 28 |
| 325 | 29 T : {l : Level} -> Bool |
| 30 T {l} = \{X : Set l} -> \(x y : X) -> x | |
| 315 | 31 |
| 325 | 32 F : {l : Level} -> Bool |
| 33 F {l} = \{X : Set l} -> \(x y : X) -> y | |
| 315 | 34 |
| 325 | 35 D : {l : Level} -> {U : Set l} -> U -> U -> Bool -> U |
| 36 D {l} {U} u v t = t {U} u v | |
| 315 | 37 |
| 38 lemma04 : {u v : U} -> D u v T ≡ u | |
| 39 lemma04 = refl | |
| 40 | |
| 41 lemma05 : {u v : U} -> D u v F ≡ v | |
| 42 lemma05 = refl | |
| 43 | |
| 321 | 44 _×_ : {l : Level} -> Set l -> Set l -> Set (suc l) |
| 45 _×_ {l} U V = {X : Set l} -> (U -> V -> X) -> X | |
| 315 | 46 |
| 321 | 47 <_,_> : {l : Level} {U V : Set l} -> U -> V -> (U × V) |
| 48 <_,_> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v | |
| 315 | 49 |
| 321 | 50 π1 : {l : Level} {U V : Set l} -> (U × V) -> U |
| 51 π1 {l} {U} {V} t = t {U} (\(x : U) -> \(y : V) -> x) | |
| 315 | 52 |
| 321 | 53 π2 : {l : Level} {U V : Set l} -> (U × V) -> V |
| 54 π2 {l} {U} {V} t = t {V} (\(x : U) -> \(y : V) -> y) | |
| 315 | 55 |
| 56 lemma06 : {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡ u | |
| 57 lemma06 = refl | |
| 58 | |
| 59 lemma07 : {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡ v | |
| 60 lemma07 = refl | |
| 61 | |
| 62 hoge : {U V : Set l} -> U -> V -> (U × V) | |
| 63 hoge u v = < u , v > | |
| 64 | |
| 65 -- lemma08 : (t : U × V) -> < π1 t , π2 t > ≡ t | |
| 66 -- lemma08 t = {!!} | |
| 316 | 67 |
| 68 -- Emp definision is still wrong... | |
| 69 | |
| 327 | 70 Emp : {l : Level} {X : Set l} -> Set l |
| 71 Emp {l} = \{X : Set l} -> X | |
| 316 | 72 |
| 327 | 73 -- ε : {l : Level} (U : Set l) {l' : Level} {U' : Set l'} -> Emp -> Emp |
| 74 -- ε {l} U t = t | |
| 316 | 75 |
| 327 | 76 -- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} -> (t : Emp {l} {U} ) -> ε U (ε Emp t) ≡ ε U t |
| 322 | 77 -- lemma09 t = refl |
| 321 | 78 |
| 327 | 79 -- lemma10 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> U × V |
| 80 -- lemma10 {l} {U} {V} t = ε (U × V) t | |
| 316 | 81 |
| 327 | 82 -- lemma10' : {l : Level} {U V X : Set l} -> (t : Emp {_} {U × V}) -> Emp |
| 83 -- lemma10' {l} {U} {V} {X} t = ε (U × V) t | |
| 84 | |
| 85 -- lemma100 : {l : Level} {U V X : Set l} -> (t : Emp {_} {U}) -> Emp | |
| 322 | 86 -- lemma100 {l} {U} {V} t = ε U t |
| 321 | 87 |
| 327 | 88 -- lemma101 : {l k : Level} {U V : Set l} -> (t : Emp {_} {U × V}) -> π1 (ε (U × V) t) ≡ ε U t |
| 322 | 89 -- lemma101 t = refl |
| 319 | 90 |
| 327 | 91 -- lemma102 : {l k : Level} {U V : Set l} -> (t : Emp {_} {U × V}) -> π2 (ε (U × V) t) ≡ ε V t |
| 322 | 92 -- lemma102 t = refl |
| 321 | 93 |
| 327 | 94 -- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp {l} {_} ) -> (ε (U -> V) t) u ≡ ε V t |
| 322 | 95 -- lemma103 u t = refl |
| 316 | 96 |
| 97 _+_ : Set l -> Set l -> Set (suc l) | |
| 98 U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X | |
| 99 | |
| 100 ι1 : {U V : Set l} -> U -> U + V | |
| 101 ι1 {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u | |
| 102 | |
| 103 ι2 : {U V : Set l} -> V -> U + V | |
| 104 ι2 {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v | |
| 105 | |
| 317 | 106 δ : { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U |
| 107 δ {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y) | |
| 316 | 108 |
| 317 | 109 lemma11 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (r : R) -> δ {U} {V} {R} {S} u v ( ι1 r ) ≡ u r |
| 316 | 110 lemma11 u v r = refl |
| 111 | |
| 317 | 112 lemma12 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ {U} {V} {R} {S} u v ( ι2 s ) ≡ v s |
| 316 | 113 lemma12 u v s = refl |
| 114 | |
| 115 | |
| 322 | 116 _××_ : {l : Level} -> Set (suc l) -> Set l -> Set (suc l) |
| 117 _××_ {l} U V = {X : Set l} -> (U -> V -> X) -> X | |
| 118 | |
| 119 <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} -> U -> V -> (U ×× V) | |
| 120 <<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v | |
| 316 | 121 |
| 122 | |
| 322 | 123 Int = \{l : Level } -> \{ X : Set l } -> X -> ( X -> X ) -> X |
| 124 | |
| 125 Zero : {l : Level } -> { X : Set l } -> Int | |
| 126 Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x | |
| 127 | |
| 128 S : {l : Level } -> { X : Set l } -> Int -> Int | |
| 129 S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y ) | |
| 130 | |
| 326 | 131 n0 : {l : Level} {X : Set l} -> Int {l} {X} |
| 132 n0 = Zero | |
| 133 | |
| 322 | 134 n1 : {l : Level } -> { X : Set l } -> Int {l} {X} |
| 135 n1 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y x | |
| 136 | |
| 137 n2 : {l : Level } -> { X : Set l } -> Int {l} {X} | |
| 138 n2 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x) | |
| 139 | |
| 323 | 140 n3 : {l : Level } -> { X : Set l } -> Int {l} {X} |
| 141 n3 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x)) | |
| 142 | |
| 322 | 143 lemma13 : {l : Level } -> { X : Set l } -> S ( S ( Zero {l} {X}) ) ≡ n2 |
| 144 lemma13 {l} {X} = refl | |
| 145 | |
| 146 It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int -> U | |
| 147 It {l} {U} u f t = t u f | |
| 316 | 148 |
| 149 | |
| 323 | 150 R : {l : Level} { U X : Set l} -> U -> ( U -> Int {l} {X} -> U ) -> Int -> U |
| 151 R {l} {U} u v t = π1 ( It {suc l} {U × Int} (< u , Zero >) (λ (x : U × Int) → < v (π1 x) (π2 x) , S (π2 x) > ) t ) | |
| 152 | |
| 153 sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int | |
| 326 | 154 sum x y = It y ( λ z -> S z ) x |
| 155 | |
| 156 mul : {l : Level } {X : Set l} -> Int {l} {_} -> Int -> Int {l} {X} | |
| 157 mul x y = It Zero ( λ (z : Int) -> sum y z ) x | |
| 324 | 158 |
| 326 | 159 copyInt : {l : Level } {X : Set l} -> Int {l} {_} -> Int {l} {X} |
| 160 copyInt x = It Zero ( λ (z : Int) -> S z ) x | |
| 324 | 161 |
| 326 | 162 -- fact : {l : Level} {X X' : Set l} -> Int -> Int {l} {_} |
| 163 -- fact {l} {X} {X'} n = R (S Zero) (λ ( z w : Int) -> mul {l} {_} z (S w) ) n | |
| 164 | |
| 165 -- lemma13' : fact n3 ≡ mul n1 ( mul n2 n3) | |
| 166 -- lemma13' = refl | |
| 324 | 167 |
| 168 -- lemma14 : (x y : Int) -> mul x y ≡ mul y x | |
| 326 | 169 -- lemma14 x y = It {!!} {!!} {!!} |
| 323 | 170 |
| 326 | 171 lemma15 : {l : Level} {X : Set l} (x y : Int {l} {X}) -> mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2 |
| 324 | 172 lemma15 x y = refl |
| 323 | 173 |
| 324 | 174 lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int {l} {X} -> U ) -> R u v Zero ≡ u |
| 175 lemma16 u v = refl | |
| 176 | |
| 177 -- 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 | |
| 178 -- lemma17 u v t = refl | |
| 179 | |
| 180 -- 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 | 181 |
| 182 | |
| 325 | 183 List = \{l : Level} -> \{ U X : Set l} -> X -> ( U -> X -> X ) -> X |
| 323 | 184 |
| 325 | 185 Nil : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {X} |
| 186 Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x | |
| 187 | |
| 188 Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List {l} {U} {X} -> List {l} {U} {X} | |
| 189 Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y ) | |
| 190 | |
| 328 | 191 l0 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'} |
| 325 | 192 l0 = Nil |
| 193 | |
| 328 | 194 l1 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'} |
| 325 | 195 l1 = Cons n1 Nil |
| 196 | |
| 328 | 197 l2 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'} |
| 325 | 198 l2 = Cons n2 l1 |
| 323 | 199 |
| 325 | 200 ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List {l} {U} {W} -> W |
| 201 ListIt {l} {U} {W} {X} w f t = t w f | |
| 323 | 202 |
| 325 | 203 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List {suc l} {U} {Bool {l}} -> Bool |
| 204 Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool} {X} T (\u w -> F) list | |
| 205 | |
| 326 | 206 Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_} |
| 328 | 207 Append {l} {U} {X} x y = \s t -> x (y s t) t |
| 325 | 208 |
|
329
c4514e0cf0e2
no yellow on append example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
328
diff
changeset
|
209 lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {l} {Int {l} {U}} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil)) |
| 328 | 210 lemma18 = refl |
| 326 | 211 |
| 325 | 212 Tree = \{l : Level} -> \{ U X : Set l} -> X -> ( (U -> X) -> X ) -> X |
| 213 | |
| 214 NilTree : {l : Level} {U : Set l} {X : Set l} -> Tree {l} {U} {X} | |
| 215 NilTree {l} {U} {X} = \(x : X) -> \(y : (U -> X) -> X) -> x | |
| 216 | |
| 217 Collect : {l : Level} {U : Set l} {X : Set l} -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree {l} {U} {X} | |
| 218 Collect {l} {U} {X} f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y ) | |
| 219 | |
| 220 TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree {l} {U} {W} -> W | |
| 221 TreeIt {l} {U} {W} {X} w h t = t w h |