Mercurial > hg > Members > kono > Proof > automaton
view automaton-in-agda/src/mul.agda @ 413:ad086c3161d7 default tip
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 18 Jun 2024 14:05:44 +0900 |
parents | b85402051cdb |
children |
line wrap: on
line source
module mul where open import Relation.Binary.PropositionalEquality data ℕ : Set where zero : ℕ suc : ℕ → ℕ lemmm00 : ℕ lemmm00 = suc (suc zero) _+_ : ℕ → ℕ → ℕ x + zero = x x + (suc y) = suc (x + y) _*_ : ℕ → ℕ → ℕ x * zero = zero x * (suc y) = x + (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 (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 x y zero = refl +-assoc x y (suc z) = cong suc (+-assoc x y z) *-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) = 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 *-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