MonoidNat.agda

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Relation.Nullary

module MonoidNat3 where

data Expr : Set where
  add : Expr → Expr → Expr
  iota : ℕ → Expr

data _==_ : Expr → Expr → Set where
  ==-assoc : ∀ {a b c} →
    add a (add b c) == add (add a b) c

  ==-comm : ∀ {a b} →
    add a b == add b a

  ==-iota : ∀ {k l sum} →
    sum ≡ k + l →
    add (iota k) (iota l) == iota sum

  ==-iota0 : ∀ {a} →
    add (iota 0) a == a

  ==-refl : ∀ {a} → a == a
  ==-sym : ∀ {a b} → a == b → b == a
  ==-trans : ∀ {a b c} →
    a == b →
    b == c →
    a == c
  ==-add1 : ∀ {a a′ b} →
    a == a′ →
    add a b == add a′ b
  ==-add2 : ∀ {a b b′} →
    b == b′ →
    add a b == add a b′

eval : Expr → ℕ
eval (add a b) = eval a + eval b
eval (iota x) = x

==eval : ∀ {a b} →
  a == b →
  eval a ≡ eval b
==eval {.(add a (add b c))} {.(add (add a b) c)} (==-assoc {a} {b} {c}) = sym (+-assoc (eval a) (eval b) (eval c))
==eval {.(add a b)} {.(add b a)} (==-comm {a} {b}) = +-comm (eval a) (eval b)
==eval {.(add (iota _) (iota _))} (==-iota refl) = refl
==eval {.(add (iota 0) b)} {b} ==-iota0 = refl
==eval {a} {.a} ==-refl = refl
==eval {a} {b} (==-sym p) = sym (==eval p)
==eval {a} {b} (==-trans p p₁) = trans (==eval p) (==eval p₁)
==eval {.(add a b)} {.(add _ b)} (==-add1 {a} {b = b} p) = cong (_+ (eval b)) (==eval p)
==eval {.(add a b)} {.(add a _)} (==-add2 {a} {b} p) = cong (eval a +_) (==eval p)

eval==′ : ∀ {a} →
  a == iota (eval a)
eval==′ {add a a₁} = ==-trans (==-trans (==-add2 eval==′) (==-add1 eval==′)) (==-iota refl)
eval==′ {iota x} = ==-refl

eval== : ∀ {a b} →
  eval a ≡ eval b →
  a == b
eval== {b = b} p = ==-trans eval==′ (subst (λ z → iota z == b) (sym p) (==-sym eval==′))

thm : ∀ {a b} →
  add a (iota 1) == add b (iota 1) →
  a == b
thm {a} {b} p =
  let
    eq : eval a + 1 ≡ eval b + 1
    eq = ==eval p

    eq′ : 1 + eval a ≡ 1 + eval b
    eq′ = trans (+-comm 1 (eval a)) (trans eq (+-comm (eval b) 1))

    eq2 : eval a ≡ eval b
    eq2 = +-cancelˡ-≡ 1 eq′
  in
  eval== eq2