Mercurial > hg > Members > kono > Proof > category

changeset 339:716f85bc7259

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
assoc in sysem-T
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 29 Mar 2014 23:00:22 +0900
parents 2f21eb997559
children 1ff7b85e5bb2
files system-f.agda system-t.agda
diffstat 2 files changed, 90 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/system-f.agda	Sat Mar 29 17:12:33 2014 +0900
+++ b/system-f.agda	Sat Mar 29 23:00:22 2014 +0900
@@ -134,7 +134,7 @@
 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 ) 
 
 -- 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
+-- ItInt {l} {U} u f t = λ t u f
 
 -- 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 ) 
@@ -146,18 +146,15 @@
 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
+-- bad adder which modifies input type
+mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
+mul' {l} {X} x y = It Zero (add x) y
 
---   λ x y → y y y y x
---   λ x y → y y y x
---   λ z t →   (λ x y → y y y y x) (λ x y → y y y y x) (λ x y → y y y y x) t
---   λ z t →            t t t t             t t t t             t t t t    z
--- mul : {l : Level } {X : Set l} → Int X → Int X → Int X
--- mul {l} {X} x y = λ z t → x z ( λ w → y ? ? )
+mul : {l : Level } {X : Set l} → Int X → Int X → Int X
+mul {l} {X} x y = λ z t → x z ( λ w → y w t )
 
 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} {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' = refl
--- a/system-t.agda	Sat Mar 29 17:12:33 2014 +0900
+++ b/system-t.agda	Sat Mar 29 23:00:22 2014 +0900
@@ -145,49 +145,42 @@
 lemma13 zero y = refl
 lemma13 (S x) y = cong (\x -> S x ) (lemma13  x y )
 
-lemma14 : (x y : Int) -> sum x y  ≡ sum y x
-lemma14 zero zero = refl
-lemma14 zero (S t) = cong (\x -> S x )( lemma14 zero t)
-lemma14 (S t) zero = cong (\x -> S x ) ( lemma14 t zero )
-lemma14 (S t) (S t') =  let open ≡-Reasoning in 
+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 
    begin 
        sum (S t) (S t')
    ≡⟨⟩
-       R (S t') ( λ z -> λ w -> S z ) (S t)
-   ≡⟨⟩
-       S ( R (S t') ( λ z -> λ w -> S z ) t) 
+       S (sum t (S t')) 
    ≡⟨ cong ( \x -> S x ) ( lemma13 t t') ⟩
-       S ( S ( R t' ( λ z -> λ w -> S z ) t)) 
-   ≡⟨ cong ( \x -> S (S x ) ) ( lemma14 t t') ⟩
-       S ( S ( R t ( λ z -> λ w -> S z )  t'))
+       S ( S (sum t t')) 
+   ≡⟨ cong ( \x -> S (S x ) ) ( lemma14sym t t') ⟩
+       S ( S (sum t' t)) 
    ≡⟨ sym ( cong ( \x -> S x ) ( lemma13 t' t)) ⟩
-       S ( R (S t) ( λ z -> λ w -> S z )  t')
+       S (sum t' (S t)) 
    ≡⟨⟩
        R (S t) ( λ z -> λ w -> S z ) (S t')
    ≡⟨⟩
        sum (S t') (S t)
    ∎
 
-lemma15assoc' : (x y : Int) -> S ( sum x y ) ≡ sum x (S y )
-lemma15assoc' zero _ = refl
-lemma15assoc' (S x) y = cong (\x -> S x ) ( lemma15assoc' x y  )
-
-lemma15assoc : (x y z : Int) -> sum x (sum y z ) ≡ sum y (sum x z )
-lemma15assoc zero y z  = refl
-lemma15assoc (S x) y z =  let open ≡-Reasoning in
+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
    begin
-     sum (S x) (sum y z)
+     sum (S x) ( sum y z )
    ≡⟨⟩
-     S ( sum x (sum y z) )
-   ≡⟨ cong (\x -> S x ) ( lemma15assoc x y z ) ⟩
-     S ( sum y ( sum x z)  )
-   ≡⟨ lemma15assoc' y (sum x z )⟩
-     sum y (S ( sum x z) )
+     S ( sum x ( sum y z ) )
+   ≡⟨ cong (\x -> S x ) ( lemma16assoc x y z) ⟩
+     S ( sum (sum x y) z )
    ≡⟨⟩
-     sum y (sum (S x) z)
+     sum (S ( sum x y)) z
+   ≡⟨⟩
+     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
@@ -199,7 +192,17 @@
      S (sum y (mul x (S y)  ))
    ≡⟨ cong (\t -> S ( sum y t )) (lemma15'' x y ) ⟩
      S (sum y (sum x (mul x y)))
-   ≡⟨ cong (\x -> S x ) (lemma15assoc y x (mul x y)) ⟩
+   ≡⟨ cong (\x -> S x ) (
+   begin
+     sum y (sum x (mul x y))
+   ≡⟨ lemma16assoc y x (mul x y) ⟩
+     sum (sum y x) (mul x y)
+   ≡⟨ cong (\t -> sum t (mul x y)) (lemma14sym y x ) ⟩
+     sum (sum x y) (mul x y)
+   ≡⟨ sym ( lemma16assoc x y (mul x y)) ⟩
+     sum x (sum y (mul x y))
+   ∎
+   ) ⟩
      S (sum x (sum y (mul x y) ))
    ≡⟨⟩
      S (sum x (mul (S x) y ) )
@@ -225,6 +228,58 @@
    ∎
 
 
+lemma15assoc' : (y z w : Int) -> sum (mul y z) ( mul w z ) ≡ mul (sum y w)  z
+lemma15assoc' 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 ) ⟩
+      sum (mul y zero ) ( mul zero w ) 
+   ≡⟨ cong ( \t -> sum t zero ) (lemma15 y zero ) ⟩
+      sum zero zero 
+   ≡⟨⟩
+      mul zero (sum y w) 
+   ≡⟨ lemma15 zero (sum y w) ⟩
+      mul (sum y w)  zero
+   ∎
+lemma15assoc' 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) ⟩
+      sum (  sum y ( mul y z)) ( mul w (S z) )
+   ≡⟨ cong ( \t -> sum (  sum y ( mul y z)) t ) (lemma15'' w z) ⟩
+      sum (  sum y ( mul y z)) ( sum w ( mul w z) )
+   ≡⟨ sym ( lemma16assoc 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) )) ⟩
+      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 )) ) ⟩
+      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 ))  ⟩
+      sum  y ( sum  w  (sum ( mul y z) ( mul w z)) )
+   ≡⟨  cong ( \t -> sum  y (sum w t) ) ( lemma15assoc' y z w )  ⟩
+      sum  y ( sum  w  (mul (sum y w)  z) )
+   ≡⟨ lemma16assoc y w (mul (sum y w)  z) ⟩
+      sum (sum y w) ( mul (sum y w)  z )
+   ≡⟨ sym ( lemma15'' (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
+   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 ) ⟩
+      sum (mul y z) ( mul ( mul x y) z ) 
+   ≡⟨ lemma15assoc' y z (mul x y) ⟩
+      mul (sum y (mul x y))  z
+   ≡⟨⟩
+      mul (mul (S x) y)  z
+   ∎
 
 
 
+