Mercurial > hg > Members > kono > Proof > category

changeset 331:f385a5821563

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fact
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Mar 2014 11:51:34 +0700
parents fa018eb1723e
children fa179abb6161
files system-f.agda
diffstat 1 files changed, 64 insertions(+), 64 deletions(-) [+]
line wrap: on
line diff
--- a/system-f.agda	Sat Mar 22 10:22:25 2014 +0700
+++ b/system-f.agda	Sat Mar 22 11:51:34 2014 +0700
@@ -3,22 +3,22 @@
 
 module system-f  where
 
-Bool : {l : Level} {X : Set l} -> Set l
-Bool = \{l : Level} -> \{X : Set l} -> X -> X -> X
+Bool : {l : Level} (X : Set l) -> Set l
+Bool = \{l : Level} -> \(X : Set l) -> X -> X -> X
 
-T : {l : Level} {X : Set l} -> Bool {l} {X}
-T {l} {X} = \(x y : X) -> x
+T : {l : Level} (X : Set l) -> Bool X
+T X = \(x y : X) -> x
 
-F : {l : Level} {X : Set l} -> Bool {l} {X}
-F {l} {X} = \(x y : X) -> y
+F : {l : Level} (X : Set l) -> Bool X
+F X = \(x y : X) -> y
 
-D : {l : Level} -> {U : Set l} -> U -> U -> Bool {l} {U} -> U
-D {l} {U} u v t = t u v
+D : {l : Level} -> {U : Set l} -> U -> U -> Bool U -> U
+D u v t = t u v
 
-lemma04 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (T {_} {U} ) ≡  u
+lemma04 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (T U ) ≡  u
 lemma04 = refl
 
-lemma05 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (F {_} {U} ) ≡  v
+lemma05 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (F U ) ≡  v
 lemma05 = refl
 
 _×_ : {l : Level} -> Set l -> Set l ->  Set (suc l)
@@ -100,48 +100,47 @@
 <<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
 
 
-Int : {l : Level } { X : Set l } -> Set l
-Int = \{l : Level } -> \{ X : Set l } -> X -> ( X -> X ) -> X
+Int : {l : Level } ( X : Set l ) -> Set l
+Int {l} X = X -> ( X -> X ) -> X
 
-Zero : {l : Level } -> { X : Set l } -> Int 
+Zero : {l : Level } -> { X : Set l } -> Int X
 Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x
 
-S : {l : Level } -> { X : Set l } -> Int -> Int 
+S : {l : Level } -> { X : Set l } -> Int X -> Int X
 S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y )
 
-n0 : {l : Level} {X : Set l} -> Int {l} {X}
-n0 = Zero
+n0 : {l : Level} {X : Set l} -> Int X
+n0 = Zero 
 
-n1 : {l : Level } -> { X : Set l } -> Int {l} {X}
-n1 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y x
+n1 : {l : Level } -> { X : Set l } -> Int X
+n1 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y x
 
-n2 : {l : Level } -> { X : Set l } -> Int {l} {X}
-n2 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x)
+n2 : {l : Level } -> { X : Set l } -> Int X
+n2 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y x)
 
-n3 : {l : Level } -> { X : Set l } -> Int {l} {X}
-n3 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x))
+n3 : {l : Level } -> { X : Set l } -> Int X
+n3 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y x))
 
-lemma13 : {l : Level } -> { X : Set l } -> S ( S ( Zero {l} {X}) )  ≡ n2 
-lemma13 {l} {X} = refl
+lemma13 : {l : Level } -> { X : Set l } -> S (S (Zero {_} {X}))  ≡ n2 
+lemma13 = refl
 
-It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int -> U
-It {l} {U} u f t = t u f
+It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int U -> U
+It u f t = t u f
 
+R : {l : Level} { U X : Set l}   -> U -> ( U -> Int X ->  U ) -> Int _ -> U 
+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 ) 
 
-R : {l : Level} { U X : Set l}   -> U -> ( U -> Int {l} {X} ->  U ) -> Int -> U 
-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 ) 
+add : {l : Level} {X : Set l} -> Int (Int X) -> Int X -> Int X
+add x y = It y ( λ z -> S z ) x
 
-sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int
-sum x y = It y ( λ z -> S z ) x
-
-mul : {l : Level } {X : Set l} -> Int {l} {_} -> Int  -> Int {l} {X}
-mul  x y = It Zero ( λ (z : Int) -> sum y z ) x
+mul : {l : Level } {X : Set l} -> Int (Int X) -> Int (Int X) -> Int X
+mul  x y = It Zero ( λ z -> add y z ) x
 
-copyInt : {l : Level } {X : Set l} -> Int {l} {_} -> Int {l} {X}
-copyInt  x = It Zero ( λ (z : Int) -> S z ) x
+copyInt : {l : Level } {X : Set l} -> Int (Int X) -> Int X
+copyInt  x = It Zero ( λ (z : Int _) -> S z ) x
 
--- fact : {l : Level} {X X' : Set l} -> Int -> Int {l} {_}
--- fact  {l} {X} {X'} n = R  (S Zero) (λ ( z w : Int) -> mul {l} {_} z (S w) ) n
+fact : {l : Level} {X : Set l} -> Int _ -> Int X
+fact  {l} {X} n = R (S Zero) (λ z -> λ w -> mul (S w) w ) n
 
 -- lemma13' : fact n3 ≡ mul n1 ( mul n2 n3)
 -- lemma13' = refl
@@ -149,10 +148,10 @@
 -- lemma14 : (x y : Int) -> mul x y  ≡ mul y x
 -- lemma14 x y = It {!!} {!!} {!!}
 
-lemma15 : {l : Level} {X : Set l} (x y : Int {l} {X}) -> mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2
+lemma15 : {l : Level} {X : Set l} (x y : Int X) -> mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2
 lemma15 x y = refl
 
-lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int {l} {X} ->  U ) -> R u v Zero ≡ u
+lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int X ->  U ) -> R u v Zero ≡ u
 lemma16 u v = refl
 
 -- 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
@@ -160,52 +159,53 @@
 
 -- 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
 
-List : {l : Level} {U X : Set l} -> Set l
-List = \{l : Level} -> \{ U X : Set l}  -> X -> ( U -> X ->  X ) -> X 
+List : {l : Level} (U X : Set l) -> Set l
+List {l} = \( U X : Set l)  -> X -> ( U -> X ->  X ) -> X 
 
-Nil : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {X}
+Nil : {l : Level} {U : Set l} {X : Set l} -> List U X
 Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x
 
-Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List {l} {U} {X} -> List {l} {U} {X}
+Cons : {l : Level} {U : Set l} {X : Set l} -> U -> List U X -> List U X
 Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y )
 
-l0 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
+l0 : {l : Level} {X X' : Set l} -> List (Int X) (X')
 l0 = Nil
 
-l1 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
+l1 : {l : Level} {X X' : Set l} -> List (Int X) (X')
 l1 = Cons n1 Nil
 
-l2 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
+l2 : {l : Level} {X X' : Set l} -> List (Int X) (X')
 l2 = Cons n2 l1
 
-l3 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
+l3 : {l : Level} {X X' : Set l} -> List (Int X) (X')
 l3 = Cons n3 l2
 
-ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List {l} {U} {W} -> W
-ListIt {l} {U} {W} {X} w f t = t w f
+ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List U W -> W
+ListIt w f t = t w f
 
-Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List {suc l} {U} {Bool {_} {X}} -> Bool {_} {_}
-Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool} {X} T (\u w -> F) list
+Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List U (Bool X) -> Bool _
+Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (\u w -> (F X)) list
 
-Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_}
-Append {l} {U} {X} x y = \s t -> x (y s t) t
+Append : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X -> List U _
+Append x y = \s t -> x (y s t) t
 
-lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {l} {Int {l} {U}} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
+lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {_} {Int U} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
 
-Reverse : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X}
-Reverse {l} {U} {X} x = ListIt {l} {U} {List {l} {U} {_}} {X} Nil ( \u w -> Append w (Cons u Nil) ) x
+Reverse : {l : Level} {U : Set l} {X : Set l} -> List U _ -> List U X
+Reverse {l} {U} {X} x = ListIt {_} {U} {List U _} {X} Nil ( \u w -> Append w (Cons u Nil) ) x
 
-lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {l} {Int {l} {U}} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
+lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {_} {Int U} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
 lemma19 = refl
 
-Tree = \{l : Level} -> \{ U X : Set l}  -> X -> ( (U -> X) ->  X ) -> X
+Tree : {l : Level} -> Set l -> Set l -> Set l
+Tree {l} = \( U X : Set l)  -> X -> ( (U -> X) ->  X ) -> X
 
-NilTree : {l : Level} {U : Set l} {X : Set l} -> Tree {l} {U} {X}
-NilTree {l} {U} {X} = \(x : X) -> \(y : (U -> X) -> X) -> x
+NilTree : {l : Level} (U : Set l) (X : Set l) -> Tree U X
+NilTree U X = \(x : X) -> \(y : (U -> X) -> X) -> x
 
-Collect : {l : Level} {U : Set l} {X : Set l} -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree {l} {U} {X}
-Collect {l} {U} {X} f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y )
+Collect : {l : Level} (U : Set l) (X : Set l) -> (U -> X -> ((U -> X) -> X) -> X ) -> Tree U X
+Collect U X f = \(x : X) -> \(y : (U -> X) -> X) -> y (\(z : U) -> f z x y )
 
-TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree {l} {U} {W} -> W
-TreeIt {l} {U} {W} {X} w h t = t w h
+TreeIt : {l : Level} {U W X : Set l} -> W -> ( (U -> W) -> W ) -> Tree U W -> W
+TreeIt w h t = t w h