MonoidNatVar.agda

-- Idea:
-- (1) Define a language of normal forms:                                                       Nf
-- (2) Define translations to and from the normal form language:                                from-Nf, to-Nf
-- (3) Show that normal forms are equal if and only if they are equal in the original language: ==→~, ~→==
-- (4) Prove the theorem about normal form language:                                            thm′
-- (5) Reflect that proof back into a statement about the original language:                    thm

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality renaming (subst to Eq-subst)
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Data.Empty
open import Data.Unit
open import Function hiding (const; Injective)

module MonoidNatVar where

data Ctx : Set where
  ∅ : Ctx
  extend : Ctx → Ctx

data Var : Ctx → Set where
  here : ∀ {Γ} → Var (extend Γ)
  there : ∀ {Γ} → Var Γ → Var (extend Γ)

data Expr : Ctx → Set where
  add : ∀ {Γ} → Expr Γ → Expr Γ → Expr Γ
  iota : ∀ {Γ} → ℕ → Expr Γ
  var : ∀ {Γ} → Var Γ → 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′

infix  1 begin_
infixr 2 step-≡-∣ step-≡-⟩
infix  3 _∎

begin_ : ∀ {Γ} {x y : Expr Γ} → x == y → x == y
begin x≡y  =  x≡y

step-≡-∣ : ∀ {Γ} (x : Expr Γ) {y : Expr Γ} → x == y → x == y
step-≡-∣ x x≡y  =  x≡y

step-≡-⟩ : ∀ {Γ} (x : Expr Γ) {y z : Expr Γ} → y == z → x == y → x == z
step-≡-⟩ x y≡z x≡y  =  ==-trans x≡y y≡z

syntax step-≡-∣ x x≡y      =  x ==⟨⟩ x≡y
syntax step-≡-⟩ x y≡z x≡y  =  x ==⟨  x≡y ⟩ y≡z

_∎ : ∀ {Γ} (x : Expr Γ) → x == x
x ∎  =  ==-refl

private
  Var-dec : ∀ {Γ} (x y : Var Γ) →
    (x ≡ y) ⊎ (x ≢ y)
  Var-dec here here = inj₁ refl
  Var-dec here (there y) = inj₂ (λ ())
  Var-dec (there x) here = inj₂ (λ ())
  Var-dec (there x) (there y) with Var-dec x y
  ... | inj₁ refl = inj₁ refl
  ... | inj₂ p = inj₂ λ { refl → p refl }
  
  record Nf (Γ : Ctx) : Set where
    field
      const : ℕ
      vars : Var Γ → ℕ
  
  ext : ∀ {Γ Δ} →
    (Var Γ → Var Δ) →
    (Var (extend Γ) → Var (extend Δ))
  ext ρ here = here
  ext ρ (there x) = there (ρ x)
  
  rename : ∀ {Γ Δ} →
    (Var Γ → Var Δ) →
    (Expr Γ → Expr Δ)
  rename ρ (add a b) = add (rename ρ a) (rename ρ b)
  rename ρ (iota x) = iota x
  rename ρ (var x) = var (ρ x)
  
  mul : ∀ {Γ} → ℕ → Expr Γ → Expr Γ
  mul {Γ} zero a = iota 0
  mul {Γ} (suc n) a = add a (mul n a)
  
  mkVars : ∀ {Γ} → (Var Γ → ℕ) → Expr Γ
  mkVars {∅} v = iota zero
  mkVars {extend Γ} v =
    add (mul (v here) (var here))
        (rename there (mkVars {Γ} (λ x → v (there x))))
  
  from-Nf : ∀ {Γ} → Nf Γ → Expr Γ
  from-Nf record { const = const ; vars = vars } =
    add (iota const) (mkVars vars)
  
  add-Nf : ∀ {Γ} → Nf Γ → Nf Γ → Nf Γ
  add-Nf nf1 nf2 =
    record
      { const = Nf.const nf1 + Nf.const nf2
      ; vars = λ x → Nf.vars nf1 x + Nf.vars nf2 x
      }
  
  mk-one-var : ∀ {Γ} (x : Var Γ) →
    Var Γ → ℕ
  mk-one-var x y with Var-dec x y
  ... | inj₁ x₁ = 1
  ... | inj₂ y₁ = 0
  
  to-Nf : ∀ {Γ} → Expr Γ → Nf Γ
  to-Nf (add a b) = add-Nf (to-Nf a) (to-Nf b)
  to-Nf (iota x) =
    record
      { const = x
      ; vars = λ _ → 0
      }
  to-Nf (var x) =
    record
      { const = 0
      ; vars = mk-one-var x
      }
  
  _~_ : ∀ {Γ} → Nf Γ → Nf Γ → Set
  _~_ {Γ} a b =
    Nf.const a ≡ Nf.const b × (∀ (x : Var Γ) → Nf.vars a x ≡ Nf.vars b x)
  
  ~refl : ∀ {Γ} {a : Nf Γ} →
    a ~ a
  ~refl = refl , λ x → refl
  
  ~sym : ∀ {Γ} {a b : Nf Γ} →
    a ~ b →
    b ~ a
  ~sym {a} {b} (refl , snd) =
    refl , λ x → sym (snd x)
  
  ~trans : ∀ {Γ} {a b c : Nf Γ} →
    a ~ b →
    b ~ c →
    a ~ c
  ~trans {a} {b} {c} (refl , p) (refl , q) =
    refl , λ x → trans (p x) (q x)
  
  ~add1 : ∀ {Γ} {a a′ b : Nf Γ} →
    a ~ a′ →
    add-Nf a b ~ add-Nf a′ b
  ~add1 {_} {a} {a′} {b} (refl , q) =
    refl , λ x → cong (_+ Nf.vars b x) (q x)
  
  ~add2 : ∀ {Γ} {a b b′ : Nf Γ} →
    b ~ b′ →
    add-Nf a b ~ add-Nf a b′
  ~add2 {_} {a} {b} {b′} (refl , q) =
    refl , λ x → cong (Nf.vars a x +_) (q x)
  
  assoc-const : ∀ {Γ} (a b c : Expr Γ) →
    Nf.const (to-Nf a) + (Nf.const (to-Nf b) + Nf.const (to-Nf c))
      ≡
    Nf.const (to-Nf a) + Nf.const (to-Nf b) + Nf.const (to-Nf c)
  assoc-const a b c = sym (+-assoc (Nf.const (to-Nf a)) (Nf.const (to-Nf b)) (Nf.const (to-Nf c)))
  
  assoc-vars : ∀ {Γ} (a b c : Expr Γ) →
    (x : Var Γ) →
    Nf.vars (to-Nf a) x + (Nf.vars (to-Nf b) x + Nf.vars (to-Nf c) x)
      ≡
    Nf.vars (to-Nf a) x + Nf.vars (to-Nf b) x + Nf.vars (to-Nf c) x
  assoc-vars a b c = λ x → sym (+-assoc (Nf.vars (to-Nf a) x) (Nf.vars (to-Nf b) x) (Nf.vars (to-Nf c) x))
  
  comm-const : ∀ {Γ} (a b : Expr Γ) →
    Nf.const (to-Nf a) + Nf.const (to-Nf b)
      ≡
    Nf.const (to-Nf b) + Nf.const (to-Nf a)
  comm-const a b = +-comm (Nf.const (to-Nf a)) (Nf.const (to-Nf b))
   
  comm-vars : ∀ {Γ} (a b : Expr Γ) →
    (x : Var Γ) →
    Nf.vars (to-Nf a) x + Nf.vars (to-Nf b) x
      ≡
    Nf.vars (to-Nf b) x + Nf.vars (to-Nf a) x
  comm-vars a b x = +-comm (Nf.vars (to-Nf a) x) (Nf.vars (to-Nf b) x)
  
  ==→~ : ∀ {Γ} {a b : Expr Γ} →
    a == b →
    to-Nf a ~ to-Nf b
  ==→~ (==-assoc {a} {b} {c}) = assoc-const a b c , assoc-vars a b c
  ==→~ (==-comm {a} {b}) = comm-const a b , comm-vars a b
  ==→~ (==-iota refl) = refl , λ x → refl
  ==→~ ==-iota0 = refl , λ x → refl
  ==→~ ==-refl = refl , λ x → refl
  ==→~ (==-sym p) = ~sym (==→~ p)
  ==→~ (==-trans p q) = ~trans (==→~ p) (==→~ q)
  ==→~ (==-add1 p) = ~add1 (==→~ p)
  ==→~ (==-add2 p) = ~add2 (==→~ p)
  
  Nfη : ∀ {Γ} {i j} {vars vars′ : Var Γ → ℕ} →
    i ≡ j →
    vars ≡ vars′ →
    record { const = i; vars = vars } ≡ record { const = j; vars = vars′ }
  Nfη refl refl = refl
  
  ~→≡₁ : ∀ {Γ} {a b : Nf Γ} →
    a ~ b →
    Nf.const a ≡ Nf.const b
  ~→≡₁ {a = record { const = _ ; vars = vars }} (refl , snd) = refl
  
  ~→≡₂ : ∀ {Γ} {a b : Nf Γ} →
    a ~ b →
    (∀ z → Nf.vars a z ≡ Nf.vars b z)
  ~→≡₂ (fst , snd) z = snd z
  
  rename-compose : ∀ {Γ Δ Σ} (ρ : Var Γ → Var Δ) (ρ′ : Var Δ → Var Σ) →
    (a : Expr Γ) →
    rename ρ′ (rename ρ a) ≡ rename (λ x → ρ′ (ρ x)) a
  rename-compose ρ ρ′ (add a b)
    rewrite rename-compose ρ ρ′ a
          | rename-compose ρ ρ′ b = refl
  rename-compose ρ ρ′ (iota x) = refl
  rename-compose ρ ρ′ (var x) = refl
  
  rename-id : ∀ {Γ} (a : Expr Γ) →
    rename (λ x → x) a ≡ a
  rename-id (add a b) rewrite rename-id a | rename-id b = refl
  rename-id (iota x) = refl
  rename-id (var x) = refl
  
  rename-0 : ∀ {Γ Δ} (ρ : Var Γ → Var Δ) →
    rename ρ (mkVars (λ x → 0)) == iota 0
  rename-0 {∅} {Δ} ρ = ==-refl
  rename-0 {extend Γ} {Δ} ρ with rename-0 {Γ} {Δ} (λ x → ρ (there x))
  ... | z rewrite sym (rename-compose there ρ (mkVars (λ x → 0))) =
    ==-trans ==-iota0 z
  
  iota-ctx : ∀ {Γ Δ} {i} →
    iota {Γ} i == from-Nf (to-Nf (iota i)) →
    iota {Δ} i == from-Nf (to-Nf (iota i))
  iota-ctx {∅} {∅} p = p
  iota-ctx {∅} {extend Δ} {i} p =
    ==-sym (==-trans ==-comm (==-trans (==-add1 ==-iota0) go))
    where
      go : add (rename there (mkVars (λ x → 0))) (iota i) == iota i
      go = ==-trans (==-add1 (rename-0 there)) (==-iota refl)
  iota-ctx {extend Γ} {∅} p =
    ==-sym (==-trans ==-comm ==-iota0)
    --==-sym (==-trans ==-comm ==-iota0)
  iota-ctx {extend Γ} {extend Δ} {i} p =
    ==-sym (==-trans ==-comm (==-trans (==-add1 ==-iota0) go))
    where
      go : add (rename there (mkVars (λ x → 0))) (iota i) == iota i
      go = ==-trans (==-add1 (rename-0 there)) (==-iota refl)
  
  mkVars-here-there : ∀ {Γ Δ} (x : Var Γ) →
    mkVars (λ x → mk-one-var here (there x)) == iota {Δ} 0
  mkVars-here-there {_} {∅} x = ==-refl
  mkVars-here-there {_} {extend Δ} x = ==-trans ==-iota0 (rename-0 there)
  
  Injective : ∀ {A B} → (A → B) → Set
  Injective f = ∀ {x y} → f x ≡ f y → x ≡ y
  
  Injective-comp : ∀ {A B C} {f : B → C} {g : A → B} →
    Injective f →
    Injective g →
    Injective (λ x → f (g x))
  Injective-comp f-inj g-inj z = g-inj (f-inj z)
  
  there-Injective : ∀ {Γ} → Injective (there {Γ})
  there-Injective refl = refl
  
  mk-one-var-rename : ∀ {Γ Δ} (ρ : Var Γ → Var Δ) (x y : Var Γ) →
    Injective ρ →
    mk-one-var (ρ x) (ρ y)
      ≡
    mk-one-var x y
  mk-one-var-rename {Γ} {Δ} ρ x y ρ-inj with Var-dec x y
  mk-one-var-rename {Γ} {Δ} ρ x y ρ-inj | inj₁ refl with Var-dec (ρ x) (ρ y)
  mk-one-var-rename {Γ} {Δ} ρ x x ρ-inj | inj₁ refl | inj₁ x₁ = refl
  mk-one-var-rename {Γ} {Δ} ρ x x ρ-inj | inj₁ refl | inj₂ y = ⊥-elim (y refl)
  mk-one-var-rename {Γ} {Δ} ρ x y ρ-inj | inj₂ y₁ with Var-dec (ρ x) (ρ y)
  mk-one-var-rename {Γ} {Δ} ρ x y ρ-inj | inj₂ y₁ | inj₁ x₁ = ⊥-elim (y₁ (ρ-inj x₁))
  mk-one-var-rename {Γ} {Δ} ρ x y ρ-inj | inj₂ y₁ | inj₂ y₂ = refl
  
  mkVars≡ : ∀ {Γ} (vars vars′ : Var Γ → ℕ) →
    (∀ y → vars y ≡ vars′ y) →
    mkVars vars ≡ mkVars vars′
  mkVars≡ {∅} vars vars′ p = refl
  mkVars≡ {extend Γ} vars vars′ p =
    let
      z = mkVars≡ {Γ} (λ z → vars (there z)) (λ z → vars′ (there z)) λ y → p (there y)
    in
    cong₂ add (cong₂ mul (p here) refl) (cong (rename there) z)
  
  mkVars-rename : ∀ {Γ Δ} (ρ : Var Γ → Var Δ) (x : Var Γ) →
    Injective ρ →
    mkVars (λ y → mk-one-var (ρ x) (ρ y))
      ≡
    mkVars (λ y → mk-one-var x y)
  mkVars-rename {extend Γ} {Δ} ρ v ρ-inj =
    trans (cong (λ z → add z e) q) (cong₂ add refl e-eq)
    where
      q : mul (mk-one-var (ρ v) (ρ here)) (var here) ≡ mul (mk-one-var v here) (var here)
      q with Var-dec (ρ v) (ρ here)
      q | inj₁ x with Var-dec v here
      q | inj₁ x | inj₁ x₁ = refl
      q | inj₁ x | inj₂ y = ⊥-elim (y (ρ-inj x))
      q | inj₂ y with Var-dec v here
      q | inj₂ y | inj₁ refl = ⊥-elim (y refl)
      q | inj₂ y | inj₂ y₁ = refl
  
      e = rename there (mkVars (λ x → mk-one-var (ρ v) (ρ (there x))))
  
      e-eq : e ≡ rename there (mkVars (λ x → mk-one-var v (there x)))
      e-eq =
        let eq = λ z → mk-one-var-rename ρ v (there z) ρ-inj
        in
        cong (rename there) (mkVars≡ (λ z → mk-one-var (ρ v) (ρ (there z))) (λ z → mk-one-var v (there z)) eq)
  
  rename== : ∀ {Γ Δ} (ρ : Var Γ → Var Δ) (a b : Expr Γ) →
    a == b →
    rename ρ a == rename ρ b
  rename== ρ .(add _ (add _ _)) .(add (add _ _) _) ==-assoc = ==-assoc
  rename== ρ .(add _ _) .(add _ _) ==-comm = ==-comm
  rename== ρ .(add (iota _) (iota _)) .(iota _) (==-iota x) = ==-iota x
  rename== ρ .(add (iota 0) b) b ==-iota0 = ==-iota0
  rename== ρ a .a ==-refl = ==-refl
  rename== ρ a b (==-sym eq) = ==-sym (rename== ρ b a eq)
  rename== ρ a b (==-trans {b = c} eq eq₁) =
    ==-trans (rename== ρ a c eq) (rename== ρ c b eq₁)
  rename== ρ .(add a _) .(add a′ _) (==-add1 {a} {a′} eq) = ==-add1 (rename== ρ a a′ eq)
  rename== ρ .(add _ b) .(add _ b′) (==-add2 {b = b} {b′} eq) = ==-add2 (rename== ρ b b′ eq)
  
  mkVars-lemma : ∀ {Γ} (x : Var Γ) →
    mkVars (λ y → mk-one-var x y) == var x
  mkVars-lemma {extend Γ} here =
    ==-trans (==-add1 (==-trans ==-comm ==-iota0)) (==-trans (==-add2 (rename-0 there)) (==-trans ==-comm ==-iota0))
  mkVars-lemma {extend Γ} (there x) =
    ==-trans ==-iota0 (==-trans (rename== there e e′ p) (rename== there (mkVars (mk-one-var x)) (var x) (mkVars-lemma x)))
    where
      e = mkVars (λ y → mk-one-var (there x) (there y))
      e′ = mkVars (λ y → mk-one-var x y)
  
      p : e == e′
      p rewrite mkVars-rename there x there-Injective = ==-refl
  
  from-to-var : ∀ {Γ} (x : Var Γ) →
    var x == from-Nf (to-Nf (var x))
  from-to-var {.(extend _)} here =
    ==-sym (==-trans ==-iota0 (==-trans (==-add1 (==-trans ==-comm ==-iota0))
      (==-trans (==-add2 (rename-0 there)) (==-trans ==-comm ==-iota0))))
  
  from-to-var {extend Γ} (there x) =
    let
        w : mkVars (λ x₁ → mk-one-var (there x) x₁) == var (there x)
        w = mkVars-lemma {extend Γ} (there x)
  
        e : Expr (extend Γ)
        e = rename there (mkVars (λ y → Nf.vars (to-Nf (var (there x))) (there y)))
    in
    ==-sym (==-trans ==-iota0 (==-trans ==-iota0 (==-trans go′ ==-refl)))
    where
      go : ∀ {Δ} (z : Var Δ) → mkVars (λ y → mk-one-var (there z) (there y)) == var z
      go z rewrite mkVars-rename there z there-Injective = mkVars-lemma z
  
      go′ : rename there (mkVars (λ y → mk-one-var (there x) (there y))) == var (there x)
      go′ =
        let z = go (there x)
  
            z-lam = λ e → add (iota 0) (rename there e) == var (there x)
  
            z′ : add (iota 0) (rename there (mkVars (λ y → mk-one-var x y)))
                   ==
                 var (there x)
            z′ = Eq-subst z-lam (mkVars-rename (λ z → there (there z)) x (Injective-comp there-Injective there-Injective)) z
        in
        ==-trans (==-trans (rename== there s t eq) (==-sym ==-iota0)) z′
        where
            s : Expr Γ
            s = mkVars (λ y → mk-one-var (there x) (there y))
  
            t : Expr Γ
            t = mkVars (λ y → mk-one-var x y)
  
            eq : s == t
            eq rewrite mkVars-rename there x there-Injective = ==-refl
  
  from-to-iota : ∀ {Γ} i →
    iota {Γ} i == from-Nf (to-Nf (iota i))
  from-to-iota {∅} i = ==-sym (==-trans ==-comm ==-iota0)
  from-to-iota {extend Γ} i =
    let z = from-to-iota {Γ} i
    in
    iota-ctx z
  
  data SplitExpr {Γ} : Expr Γ → Expr Γ → Expr Γ → Set where
    Split-iota : ∀ {i} {a} →
      a == iota 0 →
      SplitExpr (iota i) (iota i) a
    Split-var : ∀ {x} {a} {b} →
      a == iota 0 →
      b == var x →
      SplitExpr (var x) a b
    Split-add : ∀ {a b vars vars′ consts consts′} {var-sum const-sum} →
      SplitExpr a consts vars →
      SplitExpr b consts′ vars′ →
      var-sum == add vars vars′ →
      const-sum == add consts consts′ →
      SplitExpr (add a b) const-sum var-sum
  
  SplitExpr-exists : ∀ {Γ} a →
    ∃[ consts ]
    ∃[ vars ]
    SplitExpr {Γ} a consts vars
  SplitExpr-exists (add a b) with SplitExpr-exists a | SplitExpr-exists b
  ... | fst , fst₂ , snd | fst₁ , fst₃ , snd₁ = add fst fst₁ , add fst₂ fst₃ , Split-add snd snd₁ ==-refl ==-refl
  SplitExpr-exists (iota x) = iota x , iota zero , Split-iota ==-refl
  SplitExpr-exists (var x) = iota zero , var x , Split-var ==-refl ==-refl
  
  SplitExpr-sound : ∀ {Γ} {a consts vars : Expr Γ} →
    SplitExpr a consts vars →
    a == add consts vars
  SplitExpr-sound (Split-iota eq) = ==-sym (==-trans ==-comm (==-trans (==-add1 eq) ==-iota0))
  SplitExpr-sound (Split-var eq eq2) = ==-sym (==-trans (==-add1 eq) (==-trans ==-iota0 eq2))
  SplitExpr-sound (Split-add {a = a} {b = b} {vars = vars} {vars′ = vars′} {consts = consts} {consts′ = consts′} p q eq eq2) =
    let z = SplitExpr-sound p
        w = SplitExpr-sound q
    in
    ==-trans (==-add1 z) (==-trans (==-add2 w) (==-trans ==-assoc (==-trans (==-add1 (==-sym ==-assoc)) (==-trans (==-add1 (==-add2 ==-comm))
          (==-trans (==-add1 ==-assoc) (==-sym (==-trans (==-add2 eq) (==-trans (==-add1 eq2) ==-assoc))))))))
  
  mkVars-0 : ∀ {Γ Δ} (ρ : Var Γ → Var Δ) →
    rename ρ (mkVars {Γ} (λ _ → 0)) == iota 0
  mkVars-0 {∅} ρ = ==-refl
  mkVars-0 {extend Γ} ρ rewrite rename-compose there ρ (mkVars (λ x → 0)) =
    ==-trans (==-add2 (mkVars-0 λ z → ρ (there z))) (==-iota refl)
  
  mul-+ : ∀ {Γ} {i j} {a : Expr Γ} →
    mul (i + j) a == add (mul i a) (mul j a)
  mul-+ {_} {zero} {j} = ==-sym ==-iota0
  mul-+ {_} {suc i} {j} = ==-trans (==-add2 mul-+) ==-assoc

  mkVars-add : ∀ {Γ} (f g : Var Γ → ℕ) →
    mkVars (λ x → f x + g x)
      ==
    add (mkVars f) (mkVars g)
  mkVars-add {∅} f g = ==-sym (==-iota refl)
  mkVars-add {extend Γ} f g =
    let s = mkVars-add {Γ} (λ x → f (there x)) (λ x → g (there x))
    in
    begin
      add (mul (f here + g here) (var here)) (rename there (mkVars (λ z → f (there z) + g (there z))))
        ==⟨ ==-add2 (rename== there _ _ s) ⟩
      add (mul (f here + g here) (var here)) (rename there (add (mkVars (λ z → f (there z))) (mkVars (λ z → g (there z)))))
        ==⟨ ==-add1 mul-+ ⟩
      add (add (mul (f here) (var here)) (mul (g here) (var here))) (rename there (add (mkVars (λ z → f (there z))) (mkVars (λ z → g (there z)))))
        ==⟨ ==-sym ==-assoc ⟩
      add (mul (f here) (var here)) (add (mul (g here) (var here)) (rename there (add (mkVars (λ z → f (there z))) (mkVars (λ z → g (there z))))))
        ==⟨ ==-refl ⟩
      add (mul (f here) (var here)) (add (mul (g here) (var here)) (add (rename there (mkVars (λ z → f (there z)))) (rename there (mkVars (λ z → g (there z))))))
        ==⟨ ==-add2 ==-assoc ⟩
      add (mul (f here) (var here)) (add (add (mul (g here) (var here)) (rename there (mkVars (λ z → f (there z))))) (rename there (mkVars (λ z → g (there z)))))
        ==⟨ ==-sym (==-add2 ==-assoc) ⟩
      add (mul (f here) (var here)) (add (mul (g here) (var here)) (add (rename there (mkVars (λ z → f (there z)))) (rename there (mkVars (λ z → g (there z))))))
        ==⟨ ==-add2 (==-trans ==-assoc (==-add1 ==-comm)) ⟩
      add (mul (f here) (var here)) (add (add (rename there (mkVars (λ z → f (there z)))) (mul (g here) (var here))) (rename there (mkVars (λ z → g (there z)))))
        ==⟨ ==-sym (==-add2 ==-assoc) ⟩
      add (mul (f here) (var here)) (add (rename there (mkVars (λ z → f (there z)))) (add (mul (g here) (var here)) (rename there (mkVars (λ z → g (there z))))))
        ==⟨ ==-assoc ⟩
      add
       (add (mul (f here) (var here))
        (rename there (mkVars (λ z → f (there z)))))
       (add (mul (g here) (var here))
        (rename there (mkVars (λ z → g (there z)))))
    ∎
  
  to-Nf-SplitExpr : ∀ {Γ} (a : Expr Γ) →
    SplitExpr a (iota (Nf.const (to-Nf a))) (mkVars (Nf.vars (to-Nf a)))
  to-Nf-SplitExpr (add a b) =
    let s = to-Nf-SplitExpr a
        t = to-Nf-SplitExpr b
    in
    Split-add s t (mkVars-add (Nf.vars (to-Nf a)) (Nf.vars (to-Nf b))) (==-sym (==-iota refl))
  to-Nf-SplitExpr {Γ} (iota x) with mkVars-0 {Γ} (λ x → x)
  ... | z rewrite rename-id {Γ} (mkVars (λ _ → 0)) = Split-iota z
  to-Nf-SplitExpr (var x) = Split-var ==-refl (mkVars-lemma x)
  
  split-recombine : ∀ {Γ} (a : Expr Γ) →
      add (iota (Nf.const (to-Nf a))) (mkVars (Nf.vars (to-Nf a)))
        ==
      a
  split-recombine {Γ} a =
    ==-sym (SplitExpr-sound (to-Nf-SplitExpr a))
  
  from-to-add : ∀ {Γ} {a b : Expr Γ} →
    add a b == from-Nf (add-Nf (to-Nf a) (to-Nf b))
  from-to-add {Γ} {a} {b} =
    ==-sym (begin
      from-Nf (add-Nf (to-Nf a) (to-Nf b)) ==⟨ ==-add2 (mkVars-add (Nf.vars (to-Nf a)) (Nf.vars (to-Nf b))) ⟩
  
      add (iota (Nf.const (to-Nf a) + Nf.const (to-Nf b))) (add (mkVars (Nf.vars (to-Nf a))) (mkVars (Nf.vars (to-Nf b)))) ==⟨ ==-add1 (==-sym (==-iota refl)) ⟩
  
      add (add (iota (Nf.const (to-Nf a)))
               (iota (Nf.const (to-Nf b))))
          (add (mkVars (Nf.vars (to-Nf a)))
               (mkVars (Nf.vars (to-Nf b)))) ==⟨ ==-sym ==-assoc ⟩
  
      add (iota (Nf.const (to-Nf a)))
          (add (iota (Nf.const (to-Nf b)))
               (add (mkVars (Nf.vars (to-Nf a)))
                    (mkVars (Nf.vars (to-Nf b))))) ==⟨ ==-add2 ==-assoc ⟩
  
      add (iota (Nf.const (to-Nf a)))
          (add (add (iota (Nf.const (to-Nf b)))
                    (mkVars (Nf.vars (to-Nf a))))
               (mkVars (Nf.vars (to-Nf b)))) ==⟨ ==-add2 (==-add1 ==-comm) ⟩
  
      add (iota (Nf.const (to-Nf a)))
          (add (add (mkVars (Nf.vars (to-Nf a)))
                    (iota (Nf.const (to-Nf b))))
               (mkVars (Nf.vars (to-Nf b)))) ==⟨ ==-assoc ⟩
  
      add (add (iota (Nf.const (to-Nf a)))
               (add (mkVars (Nf.vars (to-Nf a)))
                    (iota (Nf.const (to-Nf b)))))
          (mkVars (Nf.vars (to-Nf b))) ==⟨ ==-add1 ==-assoc ⟩
  
      add (add (add (iota (Nf.const (to-Nf a)))
                    (mkVars (Nf.vars (to-Nf a))))
               (iota (Nf.const (to-Nf b))))
          (mkVars (Nf.vars (to-Nf b))) ==⟨ ==-sym ==-assoc ⟩
  
  
      add (add (iota (Nf.const (to-Nf a)))
               (mkVars (Nf.vars (to-Nf a))))
          (add (iota (Nf.const (to-Nf b)))
               (mkVars (Nf.vars (to-Nf b)))) ==⟨ ==-add1 (split-recombine a) ⟩
  
      add a
          (add (iota (Nf.const (to-Nf b)))
               (mkVars (Nf.vars (to-Nf b)))) ==⟨ ==-add2 (split-recombine b) ⟩
  
      add a b
    ∎)
  
  from-to-Nf : ∀ {Γ} (a : Expr Γ) →
    a == from-Nf (to-Nf a)
  from-to-Nf {Γ} (add a b) = from-to-add
  from-to-Nf {Γ} (var x) = from-to-var x
  from-to-Nf {Γ} (iota x) = from-to-iota x
  
  Var-dec-eq : ∀ {Γ} (x : Var Γ) →
    Var-dec x x ≡ inj₁ refl
  Var-dec-eq here = refl
  Var-dec-eq (there x) rewrite Var-dec-eq x = refl
  
  split-add : ∀ {Γ} {a b : Expr Γ} {i j} →
    a == iota i →
    b == iota j →
    add a b == iota (i + j)
  split-add p q =
    ==-trans (==-add1 p) (==-trans (==-add2 q) (==-iota refl))
  
  +0 : ∀ n → n + 0 ≡ n
  +0 zero = refl
  +0 (suc n) rewrite +0 n = refl
  
  from-to-elim : ∀ {Γ} (a b : Expr Γ) →
    from-Nf (to-Nf a) == from-Nf (to-Nf b) →
    a == b
  from-to-elim a b p = ==-trans (from-to-Nf a) (==-trans p (==-sym (from-to-Nf b)))
  
  mkVars~ : ∀ {Γ} (a b : Nf Γ) →
    a ~ b →
    mkVars (Nf.vars a) ≡ mkVars (Nf.vars b)
  mkVars~ {Γ} a b (fst , snd) =
    mkVars≡ (Nf.vars a) (Nf.vars b) snd
  
  ~→== : ∀ {Γ} {a : Expr Γ} {b} →
    to-Nf a ~ to-Nf b →
    a == b
  ~→== {_} {a} {b} p with from-to-elim a b go
    where
      go : from-Nf (to-Nf a) == from-Nf (to-Nf b)
      go rewrite ~→≡₁ p | mkVars~ (to-Nf a) (to-Nf b) p = ==-refl
  ... | z = z

iota-Nf : ∀ {Γ} →
  ℕ →
  Nf Γ
iota-Nf n = record { const = n ; vars = λ _ → 0 }

thm′ : ∀ {Γ} {a b : Nf Γ} →
  add-Nf a (iota-Nf 1) ~ add-Nf b (iota-Nf 1) →
  a ~ b
thm′ {_} {a} {b} (fst , snd) =
  +-cancelʳ-≡ {1} (Nf.const a) (Nf.const b) fst
  , λ x → +-cancelʳ-≡ {0} (Nf.vars a x) (Nf.vars b x) (snd x)

thm : ∀ {Γ} {a b : Expr Γ} →
  add a (iota 1) == add b (iota 1) →
  a == b
thm {_} {a} {b} p =
  ~→== (thm′ (==→~ p))