Id.agda

module Id where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

sym : ∀ {A} {x y : A} -> x ≡ y -> y ≡ x
sym refl = refl

_qed : ∀ {A} -> (x : A) -> x ≡ x
_ qed = refl

infixr 2 _<_>_
_<_>_ : ∀ {A} {y z : A} -> (x : A) -> x ≡ y -> y ≡ z -> x ≡ z
_ < refl > refl = refl

cong : ∀ {A B} {a b : A} (f : A -> B) -> a ≡ b -> f a ≡ f b
cong _ refl = refl

plusRightZero : (n : Nat) -> n ≡ n + zero
plusRightZero zero = refl
plusRightZero (suc n) = cong suc (plusRightZero n)

plusRightSuc : (n m : Nat) -> suc n + m ≡ n + suc m
plusRightSuc zero m = refl
plusRightSuc (suc n) m = cong suc (plusRightSuc n m)

plusComm : (n m : Nat) -> n + m ≡ m + n
plusComm zero m = plusRightZero m
plusComm (suc n) m =
  suc (n + m) < cong suc (plusComm n m) >
  suc (m + n) < plusRightSuc m n >
  (m + suc n) qed

plusAssoc : (n m o : Nat) -> n + (m + o) ≡ (n + m) + o
plusAssoc zero m o = refl
plusAssoc (suc n) m o = cong suc (plusAssoc n m o)

mulComm : (n m : Nat) -> n * m ≡ m * n
mulComm zero m = {!!}
mulComm (suc n) m = {!!}

-- mulAssoc : (n m o : Nat) -> n * (m * o) ≡ (n * m) * o
-- mulAssoc zero m o = refl
-- mulAssoc (suc n) m o =
--   m * o + n * (m * o) < cong (λ x → m * o + x) (mulAssoc n m o) >
--   m * o + n * m * o < {!!} >
--   {!!} < {!!} >
--   ((m + n * m) * o) qed


mulDistOverPlus : (n m o : Nat) -> n * (m + o) ≡ n * m + n * o
mulDistOverPlus zero m o = refl
mulDistOverPlus (suc n) m o =
  m + o + n * (m + o) < cong (λ x → m + o + x) (mulDistOverPlus n m o) >
  m + o + (n * m + n * o) < sym (plusAssoc m o (n * m + n * o)) >
  m + (o + (n * m + n * o)) <  cong (λ x → m + x) (plusAssoc o (n * m) (n * o)) >
  m + (o + n * m + n * o) < cong (λ x → m + (x + n * o)) (plusComm o (n * m)) >
  m + ((n * m + o) + n * o) < cong (λ x → m + x) (sym (plusAssoc (n * m) o (n * o))) >
  m + (n * m + (o + n * o)) < plusAssoc m (n * m) (o + n * o) >
  (m + n * m + (o + n * o)) qed