Mercurial > hg > Members > kono > Proof > category

changeset 346:0fb47d8ff0ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 19 Apr 2014 14:39:54 +0900
parents 17acb62419ac
children 87ad542e4145
files system-t.agda
diffstat 1 files changed, 89 insertions(+), 89 deletions(-) [+]
line wrap: on
line diff
--- a/system-t.agda	Sat Apr 19 11:34:49 2014 +0900
+++ b/system-t.agda	Sat Apr 19 14:39:54 2014 +0900
@@ -6,7 +6,7 @@
        π1 : U
        π2 : V
 
-<_,_> : {U V : Set} -> U -> V -> U × V
+<_,_> : {U V : Set} → U → V → U × V
 < u , v >  = record {π1 = u ; π2 = v }
 
 open _×_
@@ -17,8 +17,8 @@
 postulate v : V
 postulate u : U
 
-f : U -> V
-f = \u -> v
+f : U → V
+f = λ u → v
 
 
 UV : Set
@@ -49,7 +49,7 @@
   T : Bool 
   F : Bool
 
-D : { U : Set } -> U -> U -> Bool -> U 
+D : { U : Set } → U → U → Bool → U 
 D u v T = u 
 D u v F = v
 
@@ -57,42 +57,42 @@
     zero : Int
     S : Int →  Int
 
-pred : Int -> Int
+pred : Int → Int
 pred zero = zero
 pred (S t) = t
 
-R : { U : Set } -> U -> ( U -> Int -> U ) -> Int -> U
+R : { U : Set } → U → ( U → Int → U ) → Int → U
 R u v zero = u 
 R u v ( S t ) = v (R u v t) t
 
-null : Int -> Bool
+null : Int → Bool
 null zero = T
 null (S _)  = F
 
-It : { T : Set } -> T -> (T -> T) -> Int -> T
+It : { T : Set } → T → (T → T) → Int → T
 It u v zero = u
 It u v ( S t ) = v (It u v t )
 
-R' : { T : Set } -> T -> ( T -> Int -> T ) -> Int -> T
+R' : { T : Set } → T → ( T → Int → T ) → Int → T
 R' u v t = π1 ( It ( < u , zero > ) (λ x →  < v (π1 x) (π2 x) , S (π2 x) > ) t )
 
-sum : Int -> Int -> Int
-sum x y = R y ( λ z -> λ w -> S z ) x
+sum : Int → Int → Int
+sum x y = R y ( λ z → λ w → S z ) x
 
-mul : Int -> Int -> Int
-mul x y = R zero ( λ z -> λ w -> sum y z ) x 
+mul : Int → Int → Int
+mul x y = R zero ( λ z → λ w → sum y z ) x 
 
-sum' : Int -> Int -> Int
-sum' x y = R' y ( λ z -> λ w -> S z ) x
+sum' : Int → Int → Int
+sum' x y = R' y ( λ z → λ w → S z ) x
 
-mul' : Int -> Int -> Int
-mul' x y = R' zero ( λ z -> λ w -> sum y z ) x
+mul' : Int → Int → Int
+mul' x y = R' zero ( λ z → λ w → sum y z ) x
 
-fact : Int -> Int
-fact  n = R  (S zero) (λ z -> λ w -> mul (S w) z ) n
+fact : Int → Int
+fact  n = R  (S zero) (λ z → λ w → mul (S w) z ) n
 
-fact' : Int -> Int
-fact' n = R' (S zero) (λ z -> λ w -> mul (S w) z ) n
+fact' : Int → Int
+fact' n = R' (S zero) (λ z → λ w → mul (S w) z ) n
 
 f3 = fact (S (S (S zero)))
 f3' = fact' (S (S (S zero)))
@@ -100,80 +100,80 @@
 lemma21 : f3 ≡ f3'
 lemma21 = refl
 
-lemma07 : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t :  Int ) -> 
+lemma07 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t :  Int ) → 
         (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t )) ≡  t
 lemma07 u v zero   =  refl
-lemma07 u v (S t)  =  cong ( \x -> S x ) ( lemma07 u v t )
+lemma07 u v (S t)  =  cong ( λ x → S x ) ( lemma07 u v t )
 
-lemma06 : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t :  Int ) -> ( (R u v t) ≡  (R' u v t ))
+lemma06 : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t :  Int ) → ( (R u v t) ≡  (R' u v t ))
 lemma06 u v zero = refl 
-lemma06 u v (S t) =  trans  ( cong ( \x ->  v x t )  ( lemma06 u v t ) ) 
-                            ( cong ( \y ->  v (R' u v t) y ) (sym ( lemma07 u v t ) ) )
+lemma06 u v (S t) =  trans  ( cong ( λ x →  v x t )  ( lemma06 u v t ) ) 
+                            ( cong ( λ y →  v (R' u v t) y ) (sym ( lemma07 u v t ) ) )
 
-lemma08 : ( n m : Int ) -> ( sum' n m ≡ sum n m )
+lemma08 : ( n m : Int ) → ( sum' n m ≡ sum n m )
 lemma08 zero _ = refl 
-lemma08 (S t) y =  cong ( \x -> S x ) ( lemma08 t y ) 
+lemma08 (S t) y =  cong ( λ x → S x ) ( lemma08 t y ) 
 
-lemma09 : ( n m : Int ) -> ( mul' n m ≡ mul n m )
+lemma09 : ( n m : Int ) → ( mul' n m ≡ mul n m )
 lemma09 zero _ = refl 
-lemma09 (S t) y =  cong ( \x -> sum y x) ( lemma09 t y ) 
+lemma09 (S t) y =  cong ( λ x → sum y x) ( lemma09 t y ) 
 
-lemma10 : ( n : Int ) -> ( fact n  ≡ fact n )
+lemma10 : ( n : Int ) → ( fact n  ≡ fact n )
 lemma10 zero = refl 
-lemma10 (S t) =  cong ( \x -> mul (S t) x ) ( lemma10 t ) 
+lemma10 (S t) =  cong ( λ x → mul (S t) x ) ( lemma10 t ) 
 
-lemma11 : ( n : Int ) -> ( fact n  ≡ fact' n )
-lemma11 n = lemma06 (S zero) (λ z -> λ w -> mul (S w) z ) n
+lemma11 : ( n : Int ) → ( fact n  ≡ fact' n )
+lemma11 n = lemma06 (S zero) (λ z → λ w → mul (S w) z ) n
 
-lemma06' : { U : Set } -> ( u : U ) -> ( v : U -> Int -> U ) ->( t :  Int ) -> ( (R u v t) ≡  (R' u v t ))
+lemma06' : { U : Set } → ( u : U ) → ( v : U → Int → U ) →( t :  Int ) → ( (R u v t) ≡  (R' u v t ))
 lemma06' u v zero = refl
 lemma06' u v (S t) = let open ≡-Reasoning in 
    begin 
        R u v (S t)
    ≡⟨⟩
        v (R u v t) t
-   ≡⟨ cong (\x -> v x t ) ( lemma06' u v t )  ⟩
+   ≡⟨ cong (λ x → v x t ) ( lemma06' u v t )  ⟩
        v (R' u v t) t
-   ≡⟨ cong (\x -> v (R' u v t) x ) ( sym ( lemma07 u v t )) ⟩
+   ≡⟨ cong (λ x → v (R' u v t) x ) ( sym ( lemma07 u v t )) ⟩
        v (R' u v t) (π2 (It < u , zero > (λ x → < v (π1 x) (π2 x) , S (π2 x) >) t))
    ≡⟨⟩
        R' u v (S t)
    ∎
 
 
-lemma13 : (x y : Int) -> sum x (S y)  ≡ S (sum x y )
-lemma13 zero y = refl
-lemma13 (S x) y = cong (\x -> S x ) (lemma13  x y )
+sum1 : (x y : Int) → sum x (S y)  ≡ S (sum x y )
+sum1 zero y = refl
+sum1 (S x) y = cong (λ x → S x ) (sum1  x y )
 
-lemma14sym : (x y : Int) -> sum x y  ≡ sum y x
-lemma14sym zero zero = refl
-lemma14sym zero (S t) = cong (\x -> S x )( lemma14sym zero t)
-lemma14sym (S t) zero = cong (\x -> S x ) ( lemma14sym t zero )
-lemma14sym (S t) (S t') =  let open ≡-Reasoning in 
+sum-sym : (x y : Int) → sum x y  ≡ sum y x
+sum-sym zero zero = refl
+sum-sym zero (S t) = cong (λ x → S x )( sum-sym zero t)
+sum-sym (S t) zero = cong (λ x → S x ) ( sum-sym t zero )
+sum-sym (S t) (S t') =  let open ≡-Reasoning in 
    begin 
        sum (S t) (S t')
    ≡⟨⟩
        S (sum t (S t')) 
-   ≡⟨ cong ( \x -> S x ) ( lemma13 t t') ⟩
+   ≡⟨ cong ( λ x → S x ) ( sum1 t t') ⟩
        S ( S (sum t t')) 
-   ≡⟨ cong ( \x -> S (S x ) ) ( lemma14sym t t') ⟩
+   ≡⟨ cong ( λ x → S (S x ) ) ( sum-sym t t') ⟩
        S ( S (sum t' t)) 
-   ≡⟨ sym ( cong ( \x -> S x ) ( lemma13 t' t)) ⟩
+   ≡⟨ sym ( cong ( λ x → S x ) ( sum1 t' t)) ⟩
        S (sum t' (S t)) 
    ≡⟨⟩
-       R (S t) ( λ z -> λ w -> S z ) (S t')
+       R (S t) ( λ z → λ w → S z ) (S t')
    ≡⟨⟩
        sum (S t') (S t)
    ∎
 
-lemma16assoc : (x y z : Int) -> sum x (sum y z ) ≡ sum (sum x y)  z 
-lemma16assoc zero y z  = refl
-lemma16assoc (S x) y z =  let open ≡-Reasoning in
+sum-assoc : (x y z : Int) → sum x (sum y z ) ≡ sum (sum x y)  z 
+sum-assoc zero y z  = refl
+sum-assoc (S x) y z =  let open ≡-Reasoning in
    begin
      sum (S x) ( sum y z )
    ≡⟨⟩
      S ( sum x ( sum y z ) )
-   ≡⟨ cong (\x -> S x ) ( lemma16assoc x y z) ⟩
+   ≡⟨ cong (λ x → S x ) ( sum-assoc x y z) ⟩
      S ( sum (sum x y) z )
    ≡⟨⟩
      sum (S ( sum x y)) z
@@ -181,25 +181,25 @@
      sum (sum (S x) y) z
    ∎
 
-lemma15'' : (x y : Int) -> mul x (S y) ≡ sum x ( mul x y )
-lemma15'' zero y = refl
-lemma15'' (S x) y =   let open ≡-Reasoning in
+mul-distr1 : (x y : Int) → mul x (S y) ≡ sum x ( mul x y )
+mul-distr1 zero y = refl
+mul-distr1 (S x) y =   let open ≡-Reasoning in
    begin
      mul (S x) (S y)
    ≡⟨⟩
      sum (S y) (mul x (S y))
    ≡⟨⟩
      S (sum y (mul x (S y)  ))
-   ≡⟨ cong (\t -> S ( sum y t )) (lemma15'' x y ) ⟩
+   ≡⟨ cong (λ t → S ( sum y t )) (mul-distr1 x y ) ⟩
      S (sum y (sum x (mul x y)))
-   ≡⟨ cong (\x -> S x ) (
+   ≡⟨ cong (λ x → S x ) (
    begin
      sum y (sum x (mul x y))
-   ≡⟨ lemma16assoc y x (mul x y) ⟩
+   ≡⟨ sum-assoc y x (mul x y) ⟩
      sum (sum y x) (mul x y)
-   ≡⟨ cong (\t -> sum t (mul x y)) (lemma14sym y x ) ⟩
+   ≡⟨ cong (λ t → sum t (mul x y)) (sum-sym y x ) ⟩
      sum (sum x y) (mul x y)
-   ≡⟨ sym ( lemma16assoc x y (mul x y)) ⟩
+   ≡⟨ sym ( sum-assoc x y (mul x y)) ⟩
      sum x (sum y (mul x y))
    ∎
    ) ⟩
@@ -210,71 +210,71 @@
      sum (S x) (mul (S x) y)
    ∎
 
-lemma15' : (x : Int) -> mul zero x  ≡ mul x zero 
-lemma15' zero = refl
-lemma15' (S x) =  lemma15' x
+mul-sym0 : (x : Int) → mul zero x  ≡ mul x zero 
+mul-sym0 zero = refl
+mul-sym0 (S x) =  mul-sym0 x
 
-lemma15 : (x y : Int) -> mul x y  ≡ mul y x
-lemma15 zero x =  lemma15' x
-lemma15 (S x) y =  let open ≡-Reasoning in
+mul-sym : (x y : Int) → mul x y  ≡ mul y x
+mul-sym zero x =  mul-sym0 x
+mul-sym (S x) y =  let open ≡-Reasoning in
    begin
       mul (S x) y
    ≡⟨⟩
      sum y (mul x y )
-   ≡⟨ cong ( \x -> sum y x ) (lemma15 x y ) ⟩
+   ≡⟨ cong ( λ x → sum y x ) (mul-sym x y ) ⟩
      sum y (mul y x)
-   ≡⟨ sym ( lemma15'' y x ) ⟩
+   ≡⟨ sym ( mul-distr1 y x ) ⟩
      mul y (S x) 
    ∎
 
 
-lemma15distr : (y z w : Int) -> sum (mul y z) ( mul w z ) ≡ mul (sum y w)  z
-lemma15distr y zero w =  let open ≡-Reasoning in
+mul-ditr : (y z w : Int) → sum (mul y z) ( mul w z ) ≡ mul (sum y w)  z
+mul-ditr y zero w =  let open ≡-Reasoning in
    begin
       sum (mul y zero) ( mul w zero ) 
-   ≡⟨ cong ( \t -> sum (mul y zero ) t ) (lemma15 w zero ) ⟩
+   ≡⟨ cong ( λ t → sum (mul y zero ) t ) (mul-sym w zero ) ⟩
       sum (mul y zero ) ( mul zero w ) 
-   ≡⟨ cong ( \t -> sum t zero ) (lemma15 y zero ) ⟩
+   ≡⟨ cong ( λ t → sum t zero ) (mul-sym y zero ) ⟩
       sum zero zero 
    ≡⟨⟩
       mul zero (sum y w) 
-   ≡⟨ lemma15 zero (sum y w) ⟩
+   ≡⟨  mul-sym0 (sum y w)  ⟩
       mul (sum y w)  zero
    ∎
-lemma15distr y (S z) w =  let open ≡-Reasoning in
+mul-ditr y (S z) w =  let open ≡-Reasoning in
    begin
       sum (mul y (S z)) ( mul w (S z) )
-   ≡⟨ cong ( \t -> sum t ( mul w (S z ))) (lemma15'' y z) ⟩
+   ≡⟨ cong ( λ t → sum t ( mul w (S z ))) (mul-distr1 y z) ⟩
       sum (  sum y ( mul y z)) ( mul w (S z) )
-   ≡⟨ cong ( \t -> sum (  sum y ( mul y z)) t ) (lemma15'' w z) ⟩
+   ≡⟨ cong ( λ t → sum (  sum y ( mul y z)) t ) (mul-distr1 w z) ⟩
       sum (  sum y ( mul y z)) ( sum w ( mul w z) )
-   ≡⟨ sym ( lemma16assoc y (mul y z ) ( sum w ( mul w z) ) ) ⟩
+   ≡⟨ sym ( sum-assoc y (mul y z ) ( sum w ( mul w z) ) ) ⟩
       sum  y ( sum ( mul y z) ( sum w ( mul w z) ))
-   ≡⟨ cong ( \t -> sum  y t) (lemma14sym ( mul y z)  ( sum w ( mul w z) )) ⟩
+   ≡⟨ cong ( λ t → sum  y t) (sum-sym ( mul y z)  ( sum w ( mul w z) )) ⟩
       sum  y ( sum  ( sum w ( mul w z) )( mul y z))
-   ≡⟨  sym ( cong ( \t -> sum  y t) (lemma16assoc w (mul w z) (mul y z )) ) ⟩
+   ≡⟨  sym ( cong ( λ t → sum  y t) (sum-assoc w (mul w z) (mul y z )) ) ⟩
       sum  y ( sum  w  (sum ( mul w z) ( mul y z)) )
-   ≡⟨  cong ( \t -> sum  y (sum w t) ) ( lemma14sym (mul w z) (mul y z ))  ⟩
+   ≡⟨  cong ( λ t → sum  y (sum w t) ) ( sum-sym (mul w z) (mul y z ))  ⟩
       sum  y ( sum  w  (sum ( mul y z) ( mul w z)) )
-   ≡⟨  cong ( \t -> sum  y (sum w t) ) ( lemma15distr y z w )  ⟩
+   ≡⟨  cong ( λ t → sum  y (sum w t) ) ( mul-ditr y z w )  ⟩
       sum  y ( sum  w  (mul (sum y w)  z) )
-   ≡⟨ lemma16assoc y w (mul (sum y w)  z) ⟩
+   ≡⟨ sum-assoc y w (mul (sum y w)  z) ⟩
       sum (sum y w) ( mul (sum y w)  z )
-   ≡⟨ sym ( lemma15'' (sum y w) z ) ⟩
+   ≡⟨ sym ( mul-distr1 (sum y w) z ) ⟩
       mul (sum y w) (S z) 
    ∎
 
 
-lemma15assoc : (x y z : Int) -> mul x (mul y z ) ≡ mul (mul x y)  z 
-lemma15assoc zero y z = refl
-lemma15assoc (S x) y z =  let open ≡-Reasoning in
+mul-assoc : (x y z : Int) → mul x (mul y z ) ≡ mul (mul x y)  z 
+mul-assoc zero y z = refl
+mul-assoc (S x) y z =  let open ≡-Reasoning in
    begin
       mul (S x) (mul y z )
    ≡⟨⟩
       sum (mul y z) ( mul x ( mul y z ) )
-   ≡⟨ cong (\t -> sum (mul y z) t ) (lemma15assoc x y z ) ⟩
+   ≡⟨ cong (λ t → sum (mul y z) t ) (mul-assoc x y z ) ⟩
       sum (mul y z) ( mul ( mul x y) z ) 
-   ≡⟨ lemma15distr y z (mul x y) ⟩
+   ≡⟨ mul-ditr y z (mul x y) ⟩
       mul (sum y (mul x y))  z
    ≡⟨⟩
       mul (mul (S x) y)  z