open import Paths
open import Algebra::Formula

open data Nat
| zero
| suc Nat

def pred Nat : Nat
| 0 ⇒ 0
| suc n ⇒ n

overlap def infixl + : BinOp Nat
| 0, a ⇒ a
| a, 0 ⇒ a
| suc a, b ⇒ suc (a + b)
| a, suc b ⇒ suc (a + b)
tighter =

private overlap def +-assoc-lemma : Associative (+)
| 0, b, c ⇒ idp
| a, 0, c ⇒ idp
| a, b, 0 ⇒ idp
| suc a, b, c ⇒ pmap suc +-assoc
| a, suc b, c ⇒ pmap suc +-assoc
| a, b, suc c ⇒ pmap suc +-assoc
inline def +-assoc {a b c : Nat} ⇒ +-assoc-lemma a b c

private overlap def +-comm-lemma : Commutative (+)
| 0, a ⇒ idp
| a, 0 ⇒ idp
| suc a, b ⇒ pmap suc +-comm
| a, suc b ⇒ pmap suc +-comm
inline def +-comm {a b : Nat} ⇒ +-comm-lemma a b

overlap def infixl * : BinOp Nat
| 0, n ⇒ 0
| m, 0 ⇒ 0
| suc m, n ⇒ n + m * n
tighter +

private def *-suc-lemma (m n : Nat) : m + m * n = m * suc n
| 0, n ⇒ idp
| suc m, n ⇒ pmap suc
  (<=3=> (sym +-assoc) (pmap (+ m * n) +-comm) +-assoc
   <==> pmap (n +) *-suc)
inline def *-suc {m n : Nat} ⇒ *-suc-lemma m n

def +-*-distl {n m : Nat} (k : Nat) : (m + k) * n = k * n + m * n
| 0 ⇒ idp
| suc k ⇒ pmap (_ +) (+-*-distl k) <==> sym +-assoc

private def *-comm-lemma : Commutative (*)
| 0, n ⇒ idp
| m, 0 ⇒ idp
| suc m, n ⇒ pmap (n +) *-comm <==> *-suc
// | m, suc n => sym *-suc <==> pmap (m +) *-comm
inline def *-comm {m n : Nat} ⇒ *-comm-lemma m n

private overlap def *-assoc-lemma : Associative (*)
| 0, _, _ ⇒ idp
| suc m, _, _ ⇒ <=3=> (+-*-distl _) (pmap (+ _) *-assoc) +-comm
inline def *-assoc {m n k : Nat} ⇒ *-assoc-lemma m n k