Mercurial > hg > Members > kono > Proof > category

changeset 336:bda408a05c24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
λ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 23 Mar 2014 07:31:20 +0700
parents 45130bd669ca
children 203593ff1e60
files system-f.agda
diffstat 1 files changed, 107 insertions(+), 101 deletions(-) [+]
line wrap: on
line diff
--- a/system-f.agda	Sat Mar 22 18:46:51 2014 +0700
+++ b/system-f.agda	Sun Mar 23 07:31:20 2014 +0700
@@ -3,209 +3,215 @@
 
 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 X
-T 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 X
-F 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 U -> U
+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)
-_×_ {l} U V =  {X : Set l} -> (U -> V -> X)  -> X 
+_×_ : {l : Level} → Set l → Set l →  Set (suc l)
+_×_ {l} U V =  {X : Set l} → (U → V → X)  → X 
 
-<_,_> : {l : Level} {U V : Set l} -> U -> V -> (U ×  V) 
-<_,_> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
+<_,_> : {l : Level} {U V : Set l} → U → V → (U ×  V) 
+<_,_> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v
 
-π1 : {l : Level} {U V : Set l} -> (U ×  V) -> U
-π1 {l} {U} {V}  t = t {U} (\(x : U) -> \(y : V) -> x)
+π1 : {l : Level} {U V : Set l} → (U ×  V) → U
+π1 {l} {U} {V}  t = t {U} (λ(x : U) → λ(y : V) → x)
 
-π2 : {l : Level} {U V : Set l} -> (U ×  V) -> V
-π2 {l} {U} {V}  t = t {V} (\(x : U) -> \(y : V) -> y)
+π2 : {l : Level} {U V : Set l} → (U ×  V) → V
+π2 {l} {U} {V}  t = t {V} (λ(x : U) → λ(y : V) → y)
 
-lemma06 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
+lemma06 : {l : Level} {U V : Set l } → {u : U } → {v : V} → π1 ( < u , v > ) ≡  u
 lemma06 = refl
 
-lemma07 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡  v
+lemma07 : {l : Level} {U V : Set l } → {u : U } → {v : V} → π2 ( < u , v > ) ≡  v
 lemma07 = refl
 
-hoge : {l : Level} {U V : Set l} -> U -> V  -> (U ×  V)
+hoge : {l : Level} {U V : Set l} → U → V  → (U ×  V)
 hoge u v = < u , v >
 
--- lemma08 :  (t : U ×  V)  -> < π1 t  , π2 t > ≡ t
--- lemma08 t = {!!}
+-- lemma08 :  {l : Level} {U V : Set l } → {u : U } →  (t : U ×  V)  → < π1 t  , π2 t > ≡ t
+-- lemma08 t = refl
 
 -- Emp definision is still wrong...
 
-Emp  :  {l : Level} {X : Set l} ->  Set l
-Emp {l} = \{X : Set l} -> X
+Emp  :  {l : Level} {X : Set l} →  Set l
+Emp {l} = λ{X : Set l} → X
 
--- ε :  {l : Level} (U : Set l)  {l' : Level} {U' : Set l'}  -> Emp -> Emp 
+-- ε :  {l : Level} (U : Set l)  {l' : Level} {U' : Set l'}  → Emp → Emp 
 -- ε {l} U t =  t 
 
--- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} -> (t : Emp {l} {U} ) -> ε U (ε Emp t) ≡ ε U t
+-- lemma09 : {l : Level} {U : Set l} {l' : Level} {U' : Set l} → (t : Emp {l} {U} ) → ε U (ε Emp t) ≡ ε U t
 -- lemma09 t = refl
 
--- lemma10 :  {l : Level} {U V X : Set l} ->  (t : Emp {_} {U ×  V}) -> U × V
+-- lemma10 :  {l : Level} {U V X : Set l} →  (t : Emp {_} {U ×  V}) → U × V
 -- lemma10  {l} {U} {V} t = ε (U ×  V) t
 
--- lemma10' : {l : Level} {U V X : Set l} ->  (t : Emp {_} {U ×  V}) -> Emp
+-- lemma10' : {l : Level} {U V X : Set l} →  (t : Emp {_} {U ×  V}) → Emp
 -- lemma10' {l} {U} {V} {X} t = ε (U ×  V) t 
 
--- lemma100 : {l : Level} {U V X : Set l} ->  (t : Emp {_} {U}) -> Emp
+-- lemma100 : {l : Level} {U V X : Set l} →  (t : Emp {_} {U}) → Emp
 -- lemma100 {l} {U} {V} t = ε U t
 
--- lemma101 : {l k : Level} {U V : Set l} ->  (t : Emp {_} {U × V}) -> π1 (ε (U ×  V) t) ≡ ε U t
+-- lemma101 : {l k : Level} {U V : Set l} →  (t : Emp {_} {U × V}) → π1 (ε (U ×  V) t) ≡ ε U t
 -- lemma101 t = refl
 
--- lemma102 : {l k : Level} {U V : Set l} ->  (t : Emp {_} {U × V}) -> π2 (ε (U ×  V) t) ≡ ε V t
+-- lemma102 : {l k : Level} {U V : Set l} →  (t : Emp {_} {U × V}) → π2 (ε (U ×  V) t) ≡ ε V t
 -- lemma102 t = refl
 
--- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp {l} {_} ) -> (ε (U -> V) t) u ≡ ε V t
+-- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} {_} ) → (ε (U → V) t) u ≡ ε V t
 -- lemma103 u t = refl
 
-_+_  : {l : Level} -> Set l -> Set l -> Set (suc l)
-_+_ {l} U V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
+_+_  : {l : Level} → Set l → Set l → Set (suc l)
+_+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X
 
-ι1 : {l : Level } {U V : Set l} ->  U ->  U + V
-ι1 {l} {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u
+ι1 : {l : Level } {U V : Set l} →  U →  U + V
+ι1 {l} {U} {V} u = λ{X} → λ(x : U → X) → λ(y : V → X ) → x u
 
-ι2 : {l : Level } {U V : Set l} ->  V ->  U + V
-ι2 {l} {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
+ι2 : {l : Level } {U V : Set l} →  V →  U + V
+ι2 {l} {U} {V} v = λ{X} → λ(x : U → X) → λ(y : V → X ) → y v
 
-δ : {l : Level} { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U
-δ {l} {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y)
+δ : {l : Level} { U V R S : Set l } → (R → U) → (S → U) → ( R + S ) → U
+δ {l} {U} {V} {R} {S} u v t = t {U} (λ(x : R) → u x) ( λ(y : S) → v y)
 
-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
+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
 lemma11 u v r =  refl
 
-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
+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
 lemma12 u v s =  refl
 
 
-_××_ : {l : Level} -> Set (suc l) -> Set l ->  Set (suc l)
-_××_ {l} U V =  {X : Set l} -> (U -> V -> X)  -> X 
+_××_ : {l : Level} → Set (suc l) → Set l →  Set (suc l)
+_××_ {l} U V =  {X : Set l} → (U → V → X)  → X 
 
-<<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} -> U -> V -> (U  ××   V) 
-<<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
+<<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} → U → V → (U  ××   V) 
+<<_,_>> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v
 
 
-Int : {l : Level } ( X : Set l ) -> Set l
-Int {l} X = 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 X
-Zero {l} {X} = \(x : X ) -> \(y : X -> X ) -> x
+Zero : {l : Level } → { X : Set l } → Int X
+Zero {l} {X} = λ(x : X ) → λ(y : X → X ) → x
 
-S : {l : Level } -> { X : Set l } -> Int X -> Int X
-S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y )
+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 X
+n0 : {l : Level} {X : Set l} → Int X
 n0 = Zero 
 
-n1 : {l : Level } -> { X : Set l } -> Int X
-n1 {_} {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 X
-n2 {_} {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 X
-n3 {_} {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))
 
-n4 : {l : Level } -> { X : Set l } -> Int X
-n4 {_} {X} = \(x : X ) -> \(y : X -> X ) -> y (y (y (y x)))
+n4 : {l : Level } → { X : Set l } → Int X
+n4 {_} {X} = λ(x : X ) → λ(y : X → X ) → y (y (y (y x)))
 
-lemma13 : {l : Level } -> { X : Set l } -> S (S (Zero {_} {X}))  ≡ n2 
+lemma13 : {l : Level } → { X : Set l } → S (S (Zero {_} {X}))  ≡ n2 
 lemma13 = refl
 
-It : {l : Level} {U : Set l} -> U -> ( U -> U ) -> Int U -> U
+It : {l : Level} {U : Set l} → U → ( U → U ) → Int U → U
 It {l} {U} u f t = t u f
 
-R : {l : Level} { U X : Set l}   -> U -> ( U -> Int X ->  U ) -> Int _ -> U 
+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 ) 
 
-add : {l : Level} {X : Set l} -> Int X -> Int X -> Int X
-add x y = \z t -> x (y z t) t
+-- ItInt : {l : Level} {U : Set l} → Int U → ( Int U → Int U ) → Int U → Int U
+-- ItInt {l} {U} u f t = λt u f
 
-mul : {l : Level } {X : Set l} -> Int X -> Int (Int X) -> Int X
+-- RInt : {l : Level} { U X : Set l}   → Int U → ( Int U → Int X →  Int U ) → Int U → Int U 
+-- 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 ) 
+
+add : {l : Level} {X : Set l} → Int X → Int X → Int X
+add x y = λ z t → x (y z t) t
+
+mul : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
 mul {l} {X} x y = It Zero (add x) y
 
-fact : {l : Level} {X : Set l} -> Int _ -> Int X
-fact  {l} {X} n = R (S Zero) (λ z -> λ w -> mul z (S w) ) n
+fact : {l : Level} {X : Set l} → Int _ → Int X
+fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w) ) n
 
-lemma13' : {l : Level} {X : Set l} -> fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
+lemma13' : {l : Level} {X : Set l} → fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
 lemma13' = refl
 
--- lemma14 : {l : Level} {X : Set l} -> (x y : Int X) -> mul x y  ≡ mul y x
+-- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y  ≡ mul y x
 -- lemma14 x y = It {!!} {!!} {!!}
 
-lemma15 : {l : Level} {X : Set l} (x y : Int 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 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
+-- 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
 -- lemma17 u v t = refl
 
--- 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
+-- 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
 
-List : {l : Level} (U X : Set l) -> Set l
-List {l} = \( 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 U X
-Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> 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 U X -> List U X
-Cons {l} {U} {X} u t = \(x : X) -> \(y : U -> X -> X) -> y u (t x y )
+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 (Int X) (X')
+l0 : {l : Level} {X X' : Set l} → List (Int X) (X')
 l0 = Nil
 
-l1 : {l : Level} {X X' : Set l} -> List (Int 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 (Int 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 (Int 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 U W -> W
+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 U (Bool X) -> Bool _
-Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool _} {X} (T X) (\u w -> (F X)) 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 U X -> List U X -> List U X
-Append x y = \s t -> x (y s t) t
+Append : {l : Level} {U : Set l} {X : Set l} → List U X → List U X → List U X
+Append x y = λ s t → x (y s t) t
 
-lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {_} {Int 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 U (List U X) -> List U X
-Reverse {l} {U} {X} x = ListIt {_} {U} {List 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) → 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 {_} {Int 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} -> Set l -> Set l -> Set l
-Tree {l} = \( 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 U X
-NilTree 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 U X
-Collect 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 U W -> W
+TreeIt : {l : Level} {U W X : Set l} → W → ( (U → W) → W ) → Tree U W → W
 TreeIt w h t = t w h