Mercurial > hg > Members > kono > Proof > automaton

changeset 413:ad086c3161d7 default tip

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 Tue, 18 Jun 2024 14:05:44 +0900
parents b85402051cdb
children
files automaton-in-agda/src/mul.agda
diffstat 1 files changed, 54 insertions(+), 89 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/mul.agda	Fri Apr 05 13:38:20 2024 +0900
+++ b/automaton-in-agda/src/mul.agda	Tue Jun 18 14:05:44 2024 +0900
@@ -10,12 +10,12 @@
 lemmm00 = suc (suc zero)
 
 _+_ : ℕ → ℕ → ℕ
-zero + y = y
-suc x + y = suc (x + y)
+x + zero = x
+x + (suc y) = suc (x + y)
 
 _*_ : ℕ → ℕ → ℕ
-zero * y = zero
-suc x * y = y + (x * y)
+x * zero  = zero
+x * (suc y) = x + (x * y) 
 
 lemmm01 : ℕ
 lemmm01 = suc (suc zero) + suc (suc zero)
@@ -25,98 +25,63 @@
 +-comm zero (suc y) = cong suc (+-comm zero y)
 +-comm (suc x) zero = cong suc (+-comm x zero)
 +-comm (suc x) (suc y) = begin
-   suc (x + suc y)   ≡⟨ (cong suc (+-comm x (suc y))) ⟩
-   suc (suc (y + x)) ≡⟨  cong suc (cong suc (+-comm y x)) ⟩
-   suc (suc (x + y)) ≡⟨  cong suc ( +-comm (suc x) y) ⟩
-   suc (y + suc x) ∎ where open ≡-Reasoning
+   suc (suc x + y)   ≡⟨ cong suc (+-comm (suc x) y) ⟩
+   suc (y + suc x)   ≡⟨ refl  ⟩
+   suc (suc (y + x))  ≡⟨ cong suc (cong suc (+-comm y x )) ⟩
+   suc (suc (x + y))  ≡⟨ refl ⟩
+   suc (x + suc y)   ≡⟨ cong suc (+-comm x (suc y) ) ⟩
+   suc (suc y + x)  ∎ where open ≡-Reasoning
 
 +-assoc : ∀ x y z → (x + (y + z)) ≡ ((x + y) + z)
-+-assoc zero y z = refl
-+-assoc (suc x) y z = cong suc (+-assoc x y z)
-   
-*-distr-r : {y x z : ℕ } → (y * z) + (x * z) ≡ ((y + x) * z)
-*-distr-r {zero} {x} {z} = refl
-*-distr-r {suc y} {x} {z} = trans (sym (+-assoc z _ _)) (cong (λ k → z + k)(*-distr-r {y} {x} {z})) 
++-assoc x y zero = refl
++-assoc x y (suc z) = cong suc (+-assoc x y z)
 
-*-distr-l : {y x z : ℕ } → (y * z) + (y * x) ≡ y * (z + x )
-*-distr-l {zero} {x}  = refl
-*-distr-l {suc y} {x} {z} = begin
-  (z + (y * z)) + (x + (y * x))  ≡⟨ +-assoc (z + (y * z)) x _ ⟩
-  ((z + (y * z)) + x) + (y * x)  ≡⟨ cong (λ k → k + (y * x)) (sym (+-assoc z _ _)) ⟩
-  (z + ((y * z) + x)) + (y * x)  ≡⟨ cong (λ k → (z + k) + (y * x)  ) (+-comm _ x) ⟩
-  (z + (x + (y * z))) + (y * x)  ≡⟨ cong (λ k → k + (y * x)) (+-assoc z _ _) ⟩
-  ((z + x) + (y * z)) + (y * x)  ≡⟨ sym (+-assoc (z + x) _ _) ⟩
-  (z + x) + ((y * z) + (y * x)) ≡⟨ cong (λ k → (z + x) + k) (*-distr-l {y} {x} {z}) ⟩
-  (z + x) + (y * (z + x)) ∎  where open ≡-Reasoning
+*-distr-r : {x y z : ℕ } → (x * y) + (x * z) ≡ x * (y + z)
+*-distr-r {x} {y} {zero} = refl
+*-distr-r {x} {y} {suc z} = begin
+    (x * y) + (x + (x * z)) ≡⟨ +-assoc (x * y) x _  ⟩
+    ((x * y) + x) + (x * z) ≡⟨ cong (λ k → k + (x * z)) (+-comm (x * y) _ ) ⟩
+    (x + (x * y) ) + (x * z) ≡⟨ sym (+-assoc x (x * y) _) ⟩
+    (x + ((x * y) + (x * z))) ≡⟨ cong (λ k → x + k)(*-distr-r {x} {y} {z}) ⟩
+     x + (x * (y + z)) ∎ where open ≡-Reasoning
+
+*-distr-l : {x y z : ℕ } → (x * z) + (y * z) ≡ (x + y) * z 
+*-distr-l {x} {y} {zero} = refl
+*-distr-l {x} {y} {suc z} = begin
+    (x + (x * z)) + (y + (y * z)) ≡⟨ +-assoc (x + (x * z)) y (y * z) ⟩
+    ((x + (x * z)) + y) + (y * z) ≡⟨ cong (λ k → k + (y * z)) (sym (+-assoc x  (x * z) y)) ⟩
+    (x + ((x * z) + y)) + (y * z) ≡⟨ cong (λ k → (x + k) + (y * z) ) (+-comm _ y) ⟩
+    (x + (y + (x * z) )) + (y * z) ≡⟨ cong (λ k → k + (y * z)) (+-assoc x y (x * z)) ⟩
+    ((x + y) + (x * z) ) + (y * z) ≡⟨ sym (+-assoc (x + y) (x * z) (y * z)) ⟩
+    (x + y) + ((x * z)  + (y * z)) ≡⟨ cong (λ k → (x + y) + k) (*-distr-l {x} {y} {z}) ⟩
+    (x + y) + ((x + y) * z) ∎ where open ≡-Reasoning
 
 *-comm : ∀ x y → (x * y) ≡ (y * x)
 *-comm zero zero = refl
-*-comm zero (suc y) = *-comm zero y
-*-comm (suc x) y = lemma2 where 
-   lemma3 : {y : ℕ}　→  y ≡ (y * suc zero)
-   lemma3 {zero} = refl
-   lemma3 {suc y} = cong suc (lemma3 {y})
-   lemma2 : (y + (x * y)) ≡ (y * suc x)
-   lemma2 = begin
-      (y + (x * y)) ≡⟨ cong₂ (λ j k → j + k ) lemma3 (*-comm x y) ⟩
-      (y * suc zero) + (y * x) ≡⟨ *-distr-l {y} ⟩
-      y * suc x ∎ where open ≡-Reasoning
-
-*-assoc : ∀ x y z → (x * y) * z ≡ x * (y * z) 
-*-assoc zero y z = refl
-*-assoc (suc x) y z = begin
-    ((y + (x * y)) * z) ≡⟨ sym (*-distr-r {y} ) ⟩
-    (y * z) + ((x * y) * z) ≡⟨ cong (λ k → (y * z) + k) (*-assoc x y z) ⟩
-    (y * z) + (x * (y * z)) ∎ where open ≡-Reasoning
-
-_+ˡ_ : ℕ → ℕ → ℕ
-x +ˡ zero = x
-x +ˡ suc y = suc (x +ˡ y)
-
-theorem00 : ∀ x y → (x +ˡ y) ≡ (y + x)
-theorem00 x zero = refl
-theorem00 x (suc y) = cong suc (theorem00 x y)
-
-_*ˡ_ : ℕ → ℕ → ℕ
-x *ˡ zero = zero
-x *ˡ (suc y) = x +ˡ (x *ˡ y)
+*-comm zero (suc y) = trans (+-comm zero (zero * y)) (*-comm zero y)
+*-comm (suc x) zero = trans (*-comm x zero) (+-comm (zero * x ) zero ) 
+*-comm (suc x) (suc y) = lemma2  where
+      lemma3 : (y : ℕ) → y ≡ (suc zero * y)
+      lemma3 zero = refl
+      lemma3 (suc y) = trans (cong suc (lemma3 y)) (+-comm _ (suc zero)) 
+      lemma2 : (suc x * suc y) ≡ (suc y * suc x)
+      lemma2 = begin
+         (suc x * suc y) ≡⟨ sym ( *-distr-l {x} {suc zero} {suc y}) ⟩
+         (x + (x * y)) + (suc zero + (suc zero * y)) ≡⟨ cong (λ k → (x + (x * y)) + k) (+-comm (suc zero) (suc zero * y)) ⟩
+         (x + (x * y)) + suc (suc zero * y) ≡⟨ cong (λ k → (x + (x * y)) + k ) (cong suc (sym (lemma3 y))) ⟩
+         (x + (x * y)) + suc y ≡⟨ refl ⟩
+         (x * suc y) + suc y ≡⟨ +-comm _ (suc y) ⟩
+         suc y + (x * suc y ) ≡⟨ cong (λ k → suc y + k) (*-comm x (suc y)) ⟩
+         suc y + (suc y * x) ≡⟨ refl ⟩
+         suc y * suc x ∎ where open ≡-Reasoning
 
-                                      
-open import Data.Empty                                                
-open import Data.Unit                                                                         
-open import Relation.Nullary
-
--- theorem000 : ¬ ( _*_ ≡ _*ˡ_ )
--- theorem000 ()
-
-theorem01 : ∀ x y → (x *ˡ y) ≡ (y * x)
-theorem01 x zero = refl
-theorem01 x (suc y) = begin
-   (x *ˡ suc y) ≡⟨ refl ⟩
-   x +ˡ (x *ˡ y) ≡⟨ cong (λ k → x +ˡ k) (theorem01 x y) ⟩
-   x +ˡ (y * x) ≡⟨ theorem00 x _ ⟩
-   (y * x) + x ≡⟨ +-comm _ x ⟩
-   x + (y * x)  ∎ where open ≡-Reasoning
-
-+ˡ-assoc : ∀ x y z → (x +ˡ (y +ˡ z)) ≡ ((x +ˡ y) +ˡ z)
-+ˡ-assoc x y zero = refl
-+ˡ-assoc x y (suc z) = cong suc (+ˡ-assoc x y z)
-   
--- *ˡ-distr-l : {y x z : ℕ } → (y *ˡ z) +ˡ (y *ˡ x) ≡ y *ˡ (z +ˡ x )
--- *ˡ-distr-l {y} {zero} {z} = refl
--- *ˡ-distr-l {y} {suc x} {z} = trans ? (cong (λ k → y +ˡ k)(*ˡ-distr-l {y} {x} {z})) 
-
-
-theorem02 : ∀ x y → (x *ˡ y) ≡ (x * y)
-theorem02 x y = trans (theorem01 x y) (*-comm y x)
-
--- record Monad (M : Set → Set) : Set₁ where
---  field
---    return : {A : Set} → A → M A
---    _>>=_ : {A B : Set} → M A → (A → M B) → M B
-
---*-Monad : { M : Set → Set } → Monad M → ℕ → ℕ → ℕ
---*-Monad {M} m n n = ?
+*-assoc : ∀ x y z → (x * (y * z)) ≡ ((x * y) * z)
+*-assoc x y zero = refl
+*-assoc x y (suc z) = begin
+    x * (y * suc z) ≡⟨ refl ⟩
+    x * (y + (y * z)) ≡⟨ sym ( *-distr-r {x} {y} {y * z})  ⟩
+    (x * y) + (x * (y * z)) ≡⟨ cong (λ k → (x * y) + k) (*-assoc x y z) ⟩
+    (x * y) + ((x * y) * z) ∎ where open ≡-Reasoning