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 = ?