Mercurial > hg > Members > kono > Proof > automaton
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 = ? + + +