diff automaton-in-agda/src/mul.agda @ 412:b85402051cdb

add mul
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Apr 2024 13:38:20 +0900 (2024-04-05)
parents
children ad086c3161d7
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/mul.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -0,0 +1,122 @@
+module mul where
+
+open import  Relation.Binary.PropositionalEquality
+
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+
+lemmm00 : ℕ
+lemmm00 = suc (suc zero)
+
+_+_ : ℕ → ℕ → ℕ
+zero + y = y
+suc x + y = suc (x + y)
+
+_*_ : ℕ → ℕ → ℕ
+zero * y = zero
+suc x * y = y + (x * y)
+
+lemmm01 : ℕ
+lemmm01 = suc (suc zero) + suc (suc zero)
+
++-comm : ∀ x y → (x + y) ≡ (y + x)
++-comm zero zero = refl
++-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
+
++-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})) 
+
+*-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
+
+*-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)
+
+                                      
+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 = ?
+
+
+