mult-commutative.agda

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
succ m + n = succ (m + n)

_×_ : ℕ → ℕ → ℕ
zero × n = zero
succ m × n = n + (m × n)

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl    #-}

≡-sym : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → y ≡ x
≡-sym refl = refl

+-ass : ∀ m n p → (m + (n + p)) ≡ ((m + n) + p)
+-ass zero n p = refl
+-ass (succ m) n p rewrite +-ass m n p = refl

+-com-zero : ∀ n → (n + zero) ≡ n
+-com-zero zero = refl
+-com-zero (succ n) rewrite +-com-zero n = refl

+-com-succ : ∀ n m → (n + succ m) ≡ succ (n + m)
+-com-succ zero m = refl
+-com-succ (succ n) m rewrite +-com-succ n m = refl

+-com : ∀ m n → (m + n) ≡ (n + m)
+-com zero n rewrite +-com-zero n = refl
+-com (succ m) n rewrite +-com-succ n m | +-com m n = refl

×-com-zero : ∀ n → (n × zero) ≡ zero
×-com-zero zero = refl
×-com-zero (succ n) rewrite ×-com-zero n = refl

×-com-succ : ∀ n m → (n × succ m) ≡ (n + (n × m))
×-com-succ zero m = refl
×-com-succ (succ n) m
  rewrite ×-com-succ n m
        | +-ass m n (n × m)
        | +-ass n m (n × m)
        | +-com m n = refl

×-com : ∀ m n → (m × n) ≡ (n × m)
×-com zero n = ≡-sym (×-com-zero n)
×-com (succ m) n rewrite ×-com-succ n m | ×-com m n = refl