Mercurial > hg > Members > kono > Proof > category

comparison system-f.agda @ 324:6e9bca4e67a3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
R lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 20 Mar 2014 10:23:54 +0700
parents d22a39e155c4
children c7388bb66f1c
comparison
equal deleted inserted replaced
323:d22a39e155c4 324:6e9bca4e67a3
143 143
144 R : {l : Level} { U X : Set l} -> U -> ( U -> Int {l} {X} -> U ) -> Int -> U 144 R : {l : Level} { U X : Set l} -> U -> ( U -> Int {l} {X} -> U ) -> Int -> U
145 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 ) 145 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 )
146 146
147 sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int 147 sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int
148 sum {l} {X} x y = R {l} {Int {l} {X}} y ( λ z -> λ w -> S z ) x 148 sum x y = R y ( λ z -> λ w -> S z ) x
149 149
150 mul : {l : Level} {X : Set l} -> Int -> Int -> Int 150 mul : Int -> Int -> Int
151 mul x y = R Zero ( λ (z : Int) -> λ (w : Int) -> sum y z ) x 151 mul x y = R Zero ( λ (z : Int) -> λ (w : Int) -> sum y z ) x
152 152
153 fact : {l : Level} {X : Set l} -> Int -> Int 153 -- fact : {l : Level} {X : Set l} -> Int -> Int
154 fact {l} {X} n = R (S Zero) (λ ( z : Int) -> λ (w : Int) -> mul (S w) z ) n 154 -- fact {l} {X} n = R (S Zero) (λ ( z : Int) -> λ (w : Int) -> mul (S w) z ) n
155
156 -- lemma14 : (x y : Int) -> mul x y ≡ mul y x
157 -- lemma14 x y = {!!}
158
159 lemma15 : {l : Level} {X : Set l} (x y : Int {l} {X}) -> mul n2 n3 ≡ mul n3 n2
160 lemma15 x y = refl
161
162 lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int {l} {X} -> U ) -> R u v Zero ≡ u
163 lemma16 u v = refl
164
165 -- 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
166 -- lemma17 u v t = refl
167
168 -- 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
155 169
156 170
157 171
158 172
159 173