------------------------------------------------------------------------
-- The Agda standard library
--
-- Old solver for commutative ring or semiring equalities
------------------------------------------------------------------------

-- Uses ideas from the Coq ring tactic. See "Proving Equalities in a
-- Commutative Ring Done Right in Coq" by Grégoire and Mahboubi. The
-- code below is not optimised like theirs, though (in particular, our
-- Horner normal forms are not sparse).
--
-- At first the `WeaklyDecidable` type may at first glance look useless
-- as there is no guarantee that it doesn't always return `nothing`.
-- However the implementation of it affects the power of the solver. The
-- more equalities it returns, the more expressions the ring solver can
-- solve.

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles
open import Algebra.Solver.Ring.AlmostCommutativeRing
open import Relation.Binary.Definitions using (WeaklyDecidable)

module Algebra.Solver.Ring
  {r₁ r₂ r₃ r₄}
  (Coeff : RawRing r₁ r₄)            -- Coefficient "ring".
  (R : AlmostCommutativeRing r₂ r₃)  -- Main "ring".
  (morphism : Coeff -Raw-AlmostCommutative⟶ R)
  (_coeff≟_ : WeaklyDecidable (Induced-equivalence morphism))
  where

open import Algebra.Core
open import Algebra.Solver.Ring.Lemmas Coeff R morphism
private module C = RawRing Coeff
open AlmostCommutativeRing R
  renaming (zero to *-zero; zeroˡ to *-zeroˡ; zeroʳ to *-zeroʳ)
open import Algebra.Definitions _≈_
open import Algebra.Morphism
open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
open import Algebra.Properties.Semiring.Exp semiring

open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Binary.Reasoning.Setoid setoid
import Relation.Binary.PropositionalEquality.Core as ≡
import Relation.Binary.Reflection as Reflection

open import Data.Nat.Base using (ℕ; suc; zero)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Vec.Base using (Vec; []; _∷_; lookup)
open import Data.Maybe.Base using (just; nothing)
open import Function.Base using (_⟨_⟩_; _$_)
open import Level using (_⊔_)

infix   :-_ -H_ -N_
infixr  _:×_ _:^_ _^N_
infix   _*x+_ _*x+HN_ _*x+H_
infixl  _:*_ _*N_ _*H_ _*NH_ _*HN_
infixl  _:+_ _:-_ _+H_ _+N_
infix   _≈H_ _≈N_

private
  variable
    n : ℕ


------------------------------------------------------------------------
-- Polynomials

data Op : Set where
  [+] : Op
  [*] : Op

-- The polynomials are indexed by the number of variables.

data Polynomial (m : ℕ) : Set r₁ where
  op   : (o : Op) (p₁ : Polynomial m) (p₂ : Polynomial m) → Polynomial m
  con  : (c : C.Carrier) → Polynomial m
  var  : (x : Fin m) → Polynomial m
  _:^_ : (p : Polynomial m) (n : ℕ) → Polynomial m
  :-_  : (p : Polynomial m) → Polynomial m

-- Short-hand notation.

_:+_ : Polynomial n → Polynomial n → Polynomial n
_:+_ = op [+]

_:*_ : Polynomial n → Polynomial n → Polynomial n
_:*_ = op [*]

_:-_ : Polynomial n → Polynomial n → Polynomial n
x :- y = x :+ :- y

_:×_ : ℕ → Polynomial n → Polynomial n
zero :× p = con C.0#
suc m :× p = p :+ m :× p

-- Semantics.

sem : Op → Op₂ Carrier
sem [+] = _+_
sem [*] = _*_

-- An environment contains one value for every variable.

Env : ℕ → Set _
Env = Vec Carrier

⟦_⟧ : Polynomial n → Env n → Carrier
⟦ op o p₁ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ ⟨ sem o ⟩ ⟦ p₂ ⟧ ρ
⟦ con c      ⟧ ρ = ⟦ c ⟧′
⟦ var x      ⟧ ρ = lookup ρ x
⟦ p :^ n     ⟧ ρ = ⟦ p ⟧ ρ ^ n
⟦ :- p       ⟧ ρ = - ⟦ p ⟧ ρ

------------------------------------------------------------------------
-- Normal forms of polynomials

-- A univariate polynomial of degree d,
--
--     p = a_d x^d + a_{d-1}x^{d-1} + … + a_0,
--
-- is represented in Horner normal form by
--
--     p = ((a_d x + a_{d-1})x + …)x + a_0.
--
-- Note that Horner normal forms can be represented as lists, with the
-- empty list standing for the zero polynomial of degree "-1".
--
-- Given this representation of univariate polynomials over an
-- arbitrary ring, polynomials in any number of variables over the
-- ring C can be represented via the isomorphisms
--
--     C[] ≅ C
--
-- and
--
--     C[X_0,...X_{n+1}] ≅ C[X_0,...,X_n][X_{n+1}].

mutual

  -- The polynomial representations are indexed by the polynomial's
  -- degree.

  data HNF : ℕ → Set r₁ where
    ∅     : HNF (suc n)
    _*x+_ : HNF (suc n) → Normal n → HNF (suc n)

  data Normal : ℕ → Set r₁ where
    con  : C.Carrier → Normal zero
    poly : HNF (suc n) → Normal (suc n)

  -- Note that the data types above do /not/ ensure uniqueness of
  -- normal forms: the zero polynomial of degree one can be
  -- represented using both ∅ and ∅ *x+ con C.0#.

mutual

  -- Semantics.

  ⟦_⟧H : HNF (suc n) → Env (suc n) → Carrier
  ⟦ ∅       ⟧H _       = 0#
  ⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ

  ⟦_⟧N : Normal n → Env n → Carrier
  ⟦ con c  ⟧N _ = ⟦ c ⟧′
  ⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ

------------------------------------------------------------------------
-- Equality and decidability

mutual

  -- Equality.

  data _≈H_ : HNF n → HNF n → Set (r₁ ⊔ r₃) where
    ∅     : _≈H_ {suc n} ∅ ∅
    _*x+_ : ∀ {n} {p₁ p₂ : HNF (suc n)} {c₁ c₂ : Normal n} →
            p₁ ≈H p₂ → c₁ ≈N c₂ → (p₁ *x+ c₁) ≈H (p₂ *x+ c₂)

  data _≈N_ : Normal n → Normal n → Set (r₁ ⊔ r₃) where
    con  : ∀ {c₁ c₂} → ⟦ c₁ ⟧′ ≈ ⟦ c₂ ⟧′ → con c₁ ≈N con c₂
    poly : ∀ {n} {p₁ p₂ : HNF (suc n)} → p₁ ≈H p₂ → poly p₁ ≈N poly p₂

mutual

  -- Equality is weakly decidable.

  infix  _≟H_ _≟N_

  _≟H_ : WeaklyDecidable (_≈H_ {n = n})
  ∅           ≟H ∅           = just ∅
  ∅           ≟H (_ *x+ _)   = nothing
  (_ *x+ _)   ≟H ∅           = nothing
  (p₁ *x+ c₁) ≟H (p₂ *x+ c₂) with p₁ ≟H p₂ | c₁ ≟N c₂
  ... | just p₁≈p₂ | just c₁≈c₂ = just (p₁≈p₂ *x+ c₁≈c₂)
  ... | _          | nothing    = nothing
  ... | nothing    | _          = nothing

  _≟N_ : WeaklyDecidable (_≈N_ {n = n})
  con c₁ ≟N con c₂ with c₁ coeff≟ c₂
  ... | just c₁≈c₂ = just (con c₁≈c₂)
  ... | nothing    = nothing
  poly p₁ ≟N poly p₂ with p₁ ≟H p₂
  ... | just p₁≈p₂ = just (poly p₁≈p₂)
  ... | nothing    = nothing

mutual

  -- The semantics respect the equality relations defined above.

  ⟦_⟧H-cong : {p₁ p₂ : HNF (suc n)} →
              p₁ ≈H p₂ → ∀ ρ → ⟦ p₁ ⟧H ρ ≈ ⟦ p₂ ⟧H ρ
  ⟦ ∅               ⟧H-cong _       = refl
  ⟦ p₁≈p₂ *x+ c₁≈c₂ ⟧H-cong (x ∷ ρ) =
    (⟦ p₁≈p₂ ⟧H-cong (x ∷ ρ) ⟨ *-cong ⟩ refl)
      ⟨ +-cong ⟩
    ⟦ c₁≈c₂ ⟧N-cong ρ

  ⟦_⟧N-cong : {p₁ p₂ : Normal n} →
              p₁ ≈N p₂ → ∀ ρ → ⟦ p₁ ⟧N ρ ≈ ⟦ p₂ ⟧N ρ
  ⟦ con c₁≈c₂  ⟧N-cong _ = c₁≈c₂
  ⟦ poly p₁≈p₂ ⟧N-cong ρ = ⟦ p₁≈p₂ ⟧H-cong ρ

------------------------------------------------------------------------
-- Ring operations on Horner normal forms

-- Zero.

0H : HNF (suc n)
0H = ∅

0N : Normal n
0N {zero}  = con C.0#
0N {suc n} = poly 0H

mutual

  -- One.

  1H : HNF (suc n)
  1H {n} = ∅ *x+ 1N {n}

  1N : Normal n
  1N {zero}  = con C.1#
  1N {suc n} = poly 1H

-- A simplifying variant of _*x+_.

_*x+HN_ : HNF (suc n) → Normal n → HNF (suc n)
(p *x+ c′) *x+HN c = (p *x+ c′) *x+ c
∅          *x+HN c with c ≟N 0N
... | just c≈0 = ∅
... | nothing  = ∅ *x+ c

mutual

  -- Addition.

  _+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n)
  ∅           +H p           = p
  p           +H ∅           = p
  (p₁ *x+ c₁) +H (p₂ *x+ c₂) = (p₁ +H p₂) *x+HN (c₁ +N c₂)

  _+N_ : Normal n → Normal n → Normal n
  con c₁  +N con c₂  = con (c₁ C.+ c₂)
  poly p₁ +N poly p₂ = poly (p₁ +H p₂)

-- Multiplication.

_*x+H_ : HNF (suc n) → HNF (suc n) → HNF (suc n)
p₁         *x+H (p₂ *x+ c) = (p₁ +H p₂) *x+HN c
∅          *x+H ∅          = ∅
(p₁ *x+ c) *x+H ∅          = (p₁ *x+ c) *x+ 0N

mutual

  _*NH_ : Normal n → HNF (suc n) → HNF (suc n)
  c *NH ∅          = ∅
  c *NH (p *x+ c′) with c ≟N 0N
  ... | just c≈0 = ∅
  ... | nothing  = (c *NH p) *x+ (c *N c′)

  _*HN_ : HNF (suc n) → Normal n → HNF (suc n)
  ∅          *HN c = ∅
  (p *x+ c′) *HN c with c ≟N 0N
  ... | just c≈0 = ∅
  ... | nothing  = (p *HN c) *x+ (c′ *N c)

  _*H_ : HNF (suc n) → HNF (suc n) → HNF (suc n)
  ∅           *H _           = ∅
  (_ *x+ _)   *H ∅           = ∅
  (p₁ *x+ c₁) *H (p₂ *x+ c₂) =
    ((p₁ *H p₂) *x+H (p₁ *HN c₂ +H c₁ *NH p₂)) *x+HN (c₁ *N c₂)

  _*N_ : Normal n → Normal n → Normal n
  con c₁  *N con c₂  = con (c₁ C.* c₂)
  poly p₁ *N poly p₂ = poly (p₁ *H p₂)

-- Exponentiation.

_^N_ : Normal n → ℕ → Normal n
p ^N zero  = 1N
p ^N suc n = p *N (p ^N n)

mutual

  -- Negation.

  -H_ : HNF (suc n) → HNF (suc n)
  -H p = (-N 1N) *NH p

  -N_ : Normal n → Normal n
  -N con c  = con (C.- c)
  -N poly p = poly (-H p)

------------------------------------------------------------------------
-- Normalisation

normalise-con : C.Carrier → Normal n
normalise-con {zero}  c = con c
normalise-con {suc n} c = poly (∅ *x+HN normalise-con c)

normalise-var : Fin n → Normal n
normalise-var zero    = poly ((∅ *x+ 1N) *x+ 0N)
normalise-var (suc i) = poly (∅ *x+HN normalise-var i)

normalise : Polynomial n → Normal n
normalise (op [+] t₁ t₂) = normalise t₁ +N normalise t₂
normalise (op [*] t₁ t₂) = normalise t₁ *N normalise t₂
normalise (con c)        = normalise-con c
normalise (var i)        = normalise-var i
normalise (t :^ k)       = normalise t ^N k
normalise (:- t)         = -N normalise t

-- Evaluation after normalisation.

⟦_⟧↓ : Polynomial n → Env n → Carrier
⟦ p ⟧↓ ρ = ⟦ normalise p ⟧N ρ

------------------------------------------------------------------------
-- Homomorphism lemmas

0N-homo : ∀ {n} ρ → ⟦ 0N {n} ⟧N ρ ≈ 0#
0N-homo []      = 0-homo
0N-homo (x ∷ ρ) = refl

-- If c is equal to 0N, then c is semantically equal to 0#.

0≈⟦0⟧ : ∀ {n} {c : Normal n} → c ≈N 0N → ∀ ρ → 0# ≈ ⟦ c ⟧N ρ
0≈⟦0⟧ {c = c} c≈0 ρ = sym (begin
  ⟦ c  ⟧N ρ  ≈⟨ ⟦ c≈0 ⟧N-cong ρ ⟩
  ⟦ 0N ⟧N ρ  ≈⟨ 0N-homo ρ ⟩
  0#         ∎)

1N-homo : ∀ {n} ρ → ⟦ 1N {n} ⟧N ρ ≈ 1#
1N-homo []      = 1-homo
1N-homo (x ∷ ρ) = begin
  0# * x + ⟦ 1N ⟧N ρ  ≈⟨ refl ⟨ +-cong ⟩ 1N-homo ρ ⟩
  0# * x + 1#         ≈⟨ lemma₆ _ _ ⟩
  1#                  ∎

-- _*x+HN_ is equal to _*x+_.

*x+HN≈*x+ : ∀ {n} (p : HNF (suc n)) (c : Normal n) →
            ∀ ρ → ⟦ p *x+HN c ⟧H ρ ≈ ⟦ p *x+ c ⟧H ρ
*x+HN≈*x+ (p *x+ c′) c ρ       = refl
*x+HN≈*x+ ∅          c (x ∷ ρ) with c ≟N 0N
... | just c≈0 = begin
  0#                 ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟩
  ⟦ c ⟧N ρ           ≈⟨ sym $ lemma₆ _ _ ⟩
  0# * x + ⟦ c ⟧N ρ  ∎
... | nothing = refl

∅*x+HN-homo : ∀ {n} (c : Normal n) x ρ →
              ⟦ ∅ *x+HN c ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ
∅*x+HN-homo c x ρ with c ≟N 0N
... | just c≈0 = 0≈⟦0⟧ c≈0 ρ
... | nothing = lemma₆ _ _

mutual

  +H-homo : ∀ {n} (p₁ p₂ : HNF (suc n)) →
            ∀ ρ → ⟦ p₁ +H p₂ ⟧H ρ ≈ ⟦ p₁ ⟧H ρ + ⟦ p₂ ⟧H ρ
  +H-homo ∅           p₂          ρ       = sym (+-identityˡ _)
  +H-homo (p₁ *x+ x₁) ∅           ρ       = sym (+-identityʳ _)
  +H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
    ⟦ (p₁ +H p₂) *x+HN (c₁ +N c₂) ⟧H (x ∷ ρ)                           ≈⟨ *x+HN≈*x+ (p₁ +H p₂) (c₁ +N c₂) (x ∷ ρ) ⟩

    ⟦ p₁ +H p₂ ⟧H (x ∷ ρ) * x + ⟦ c₁ +N c₂ ⟧N ρ                        ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ +N-homo c₁ c₂ ρ ⟩

    (⟦ p₁ ⟧H (x ∷ ρ) + ⟦ p₂ ⟧H (x ∷ ρ)) * x + (⟦ c₁ ⟧N ρ + ⟦ c₂ ⟧N ρ)  ≈⟨ lemma₁ _ _ _ _ _ ⟩

    (⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ c₁ ⟧N ρ) +
    (⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ)                                  ∎

  +N-homo : ∀ {n} (p₁ p₂ : Normal n) →
            ∀ ρ → ⟦ p₁ +N p₂ ⟧N ρ ≈ ⟦ p₁ ⟧N ρ + ⟦ p₂ ⟧N ρ
  +N-homo (con c₁)  (con c₂)  _ = +-homo _ _
  +N-homo (poly p₁) (poly p₂) ρ = +H-homo p₁ p₂ ρ

*x+H-homo :
  ∀ {n} (p₁ p₂ : HNF (suc n)) x ρ →
  ⟦ p₁ *x+H p₂ ⟧H (x ∷ ρ) ≈
  ⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ p₂ ⟧H (x ∷ ρ)
*x+H-homo ∅         ∅ _ _ = sym $ lemma₆ _ _
*x+H-homo (p *x+ c) ∅ x ρ = begin
  ⟦ p *x+ c ⟧H (x ∷ ρ) * x + ⟦ 0N ⟧N ρ  ≈⟨ refl ⟨ +-cong ⟩ 0N-homo ρ ⟩
  ⟦ p *x+ c ⟧H (x ∷ ρ) * x + 0#         ∎
*x+H-homo p₁         (p₂ *x+ c₂) x ρ = begin
  ⟦ (p₁ +H p₂) *x+HN c₂ ⟧H (x ∷ ρ)                         ≈⟨ *x+HN≈*x+ (p₁ +H p₂) c₂ (x ∷ ρ) ⟩
  ⟦ p₁ +H p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ                    ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
  (⟦ p₁ ⟧H (x ∷ ρ) + ⟦ p₂ ⟧H (x ∷ ρ)) * x + ⟦ c₂ ⟧N ρ      ≈⟨ lemma₀ _ _ _ _ ⟩
  ⟦ p₁ ⟧H (x ∷ ρ) * x + (⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ)  ∎

mutual

  *NH-homo :
    ∀ {n} (c : Normal n) (p : HNF (suc n)) x ρ →
    ⟦ c *NH p ⟧H (x ∷ ρ) ≈ ⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)
  *NH-homo c ∅          x ρ = sym (*-zeroʳ _)
  *NH-homo c (p *x+ c′) x ρ with c ≟N 0N
  ... | just c≈0 = begin
    0#                                            ≈⟨ sym (*-zeroˡ _) ⟩
    0# * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)         ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟨ *-cong ⟩ refl ⟩
    ⟦ c ⟧N ρ  * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)  ∎
  ... | nothing = begin
    ⟦ c *NH p ⟧H (x ∷ ρ) * x + ⟦ c *N c′ ⟧N ρ                 ≈⟨ (*NH-homo c p x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c c′ ρ ⟩
    (⟦ c ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)) * x + (⟦ c ⟧N ρ * ⟦ c′ ⟧N ρ)  ≈⟨ lemma₃ _ _ _ _ ⟩
    ⟦ c ⟧N ρ * (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ)               ∎

  *HN-homo :
    ∀ {n} (p : HNF (suc n)) (c : Normal n) x ρ →
    ⟦ p *HN c ⟧H (x ∷ ρ) ≈ ⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ
  *HN-homo ∅          c x ρ = sym (*-zeroˡ _)
  *HN-homo (p *x+ c′) c x ρ with c ≟N 0N
  ... | just c≈0 = begin
    0#                                           ≈⟨ sym (*-zeroʳ _) ⟩
    (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * 0#        ≈⟨ refl ⟨ *-cong ⟩ 0≈⟦0⟧ c≈0 ρ ⟩
    (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ  ∎
  ... | nothing = begin
    ⟦ p *HN c ⟧H (x ∷ ρ) * x + ⟦ c′ *N c ⟧N ρ                 ≈⟨ (*HN-homo p c x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c′ c ρ ⟩
    (⟦ p ⟧H (x ∷ ρ) * ⟦ c ⟧N ρ) * x + (⟦ c′ ⟧N ρ * ⟦ c ⟧N ρ)  ≈⟨ lemma₂ _ _ _ _ ⟩
    (⟦ p ⟧H (x ∷ ρ) * x + ⟦ c′ ⟧N ρ) * ⟦ c ⟧N ρ               ∎

  *H-homo : ∀ {n} (p₁ p₂ : HNF (suc n)) →
            ∀ ρ → ⟦ p₁ *H p₂ ⟧H ρ ≈ ⟦ p₁ ⟧H ρ * ⟦ p₂ ⟧H ρ
  *H-homo ∅           p₂          ρ       = sym $ *-zeroˡ _
  *H-homo (p₁ *x+ c₁) ∅           ρ       = sym $ *-zeroʳ _
  *H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
    ⟦ ((p₁ *H p₂) *x+H ((p₁ *HN c₂) +H (c₁ *NH p₂))) *x+HN
      (c₁ *N c₂) ⟧H (x ∷ ρ)                                              ≈⟨ *x+HN≈*x+ ((p₁ *H p₂) *x+H ((p₁ *HN c₂) +H (c₁ *NH p₂)))
                                                                                      (c₁ *N c₂) (x ∷ ρ) ⟩
    ⟦ (p₁ *H p₂) *x+H
      ((p₁ *HN c₂) +H (c₁ *NH p₂)) ⟧H (x ∷ ρ) * x +
    ⟦ c₁ *N c₂ ⟧N ρ                                                      ≈⟨ (*x+H-homo (p₁ *H p₂) ((p₁ *HN c₂) +H (c₁ *NH p₂)) x ρ
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            *N-homo c₁ c₂ ρ ⟩
    (⟦ p₁ *H p₂ ⟧H (x ∷ ρ) * x +
     ⟦ (p₁ *HN c₂) +H (c₁ *NH p₂) ⟧H (x ∷ ρ)) * x +
    ⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ                                                ≈⟨ (((*H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl)
                                                                                ⟨ +-cong ⟩
                                                                              (+H-homo (p₁ *HN c₂) (c₁ *NH p₂) (x ∷ ρ)))
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            refl ⟩
    (⟦ p₁ ⟧H (x ∷ ρ) * ⟦ p₂ ⟧H (x ∷ ρ) * x +
     (⟦ p₁ *HN c₂ ⟧H (x ∷ ρ) + ⟦ c₁ *NH p₂ ⟧H (x ∷ ρ))) * x +
    ⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ                                                ≈⟨ ((refl ⟨ +-cong ⟩ (*HN-homo p₁ c₂ x ρ ⟨ +-cong ⟩ *NH-homo c₁ p₂ x ρ))
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            refl ⟩
    (⟦ p₁ ⟧H (x ∷ ρ) * ⟦ p₂ ⟧H (x ∷ ρ) * x +
     (⟦ p₁ ⟧H (x ∷ ρ) * ⟦ c₂ ⟧N ρ + ⟦ c₁ ⟧N ρ * ⟦ p₂ ⟧H (x ∷ ρ))) * x +
    (⟦ c₁ ⟧N ρ * ⟦ c₂ ⟧N ρ)                                              ≈⟨ lemma₄ _ _ _ _ _ ⟩

    (⟦ p₁ ⟧H (x ∷ ρ) * x + ⟦ c₁ ⟧N ρ) *
    (⟦ p₂ ⟧H (x ∷ ρ) * x + ⟦ c₂ ⟧N ρ)                                    ∎

  *N-homo : ∀ {n} (p₁ p₂ : Normal n) →
            ∀ ρ → ⟦ p₁ *N p₂ ⟧N ρ ≈ ⟦ p₁ ⟧N ρ * ⟦ p₂ ⟧N ρ
  *N-homo (con c₁)  (con c₂)  _ = *-homo _ _
  *N-homo (poly p₁) (poly p₂) ρ = *H-homo p₁ p₂ ρ

^N-homo : ∀ {n} (p : Normal n) (k : ℕ) →
          ∀ ρ → ⟦ p ^N k ⟧N ρ ≈ ⟦ p ⟧N ρ ^ k
^N-homo p zero    ρ = 1N-homo ρ
^N-homo p (suc k) ρ = begin
  ⟦ p *N (p ^N k) ⟧N ρ       ≈⟨ *N-homo p (p ^N k) ρ ⟩
  ⟦ p ⟧N ρ * ⟦ p ^N k ⟧N ρ   ≈⟨ refl ⟨ *-cong ⟩ ^N-homo p k ρ ⟩
  ⟦ p ⟧N ρ * (⟦ p ⟧N ρ ^ k)  ∎

mutual

  -H‿-homo : ∀ {n} (p : HNF (suc n)) →
             ∀ ρ → ⟦ -H p ⟧H ρ ≈ - ⟦ p ⟧H ρ
  -H‿-homo p (x ∷ ρ) = begin
    ⟦ (-N 1N) *NH p ⟧H (x ∷ ρ)     ≈⟨ *NH-homo (-N 1N) p x ρ ⟩
    ⟦ -N 1N ⟧N ρ * ⟦ p ⟧H (x ∷ ρ)  ≈⟨ trans (-N‿-homo 1N ρ) (-‿cong (1N-homo ρ)) ⟨ *-cong ⟩ refl ⟩
    - 1# * ⟦ p ⟧H (x ∷ ρ)          ≈⟨ lemma₇ _ ⟩
    - ⟦ p ⟧H (x ∷ ρ)               ∎

  -N‿-homo : ∀ {n} (p : Normal n) →
             ∀ ρ → ⟦ -N p ⟧N ρ ≈ - ⟦ p ⟧N ρ
  -N‿-homo (con c)  _ = -‿homo _
  -N‿-homo (poly p) ρ = -H‿-homo p ρ

------------------------------------------------------------------------
-- Correctness

correct-con : ∀ {n} (c : C.Carrier) (ρ : Env n) →
              ⟦ normalise-con c ⟧N ρ ≈ ⟦ c ⟧′
correct-con c []      = refl
correct-con c (x ∷ ρ) = begin
  ⟦ ∅ *x+HN normalise-con c ⟧H (x ∷ ρ)  ≈⟨ ∅*x+HN-homo (normalise-con c) x ρ ⟩
  ⟦ normalise-con c ⟧N ρ            ≈⟨ correct-con c ρ ⟩
  ⟦ c ⟧′                                   ∎

correct-var : ∀ {n} (i : Fin n) →
              ∀ ρ → ⟦ normalise-var i ⟧N ρ ≈ lookup ρ i
correct-var (suc i) (x ∷ ρ) = begin
  ⟦ ∅ *x+HN normalise-var i ⟧H (x ∷ ρ)  ≈⟨ ∅*x+HN-homo (normalise-var i) x ρ ⟩
  ⟦ normalise-var i ⟧N ρ                ≈⟨ correct-var i ρ ⟩
  lookup ρ i                            ∎
correct-var zero (x ∷ ρ) = begin
  (0# * x + ⟦ 1N ⟧N ρ) * x + ⟦ 0N ⟧N ρ  ≈⟨ ((refl ⟨ +-cong ⟩ 1N-homo ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ 0N-homo ρ ⟩
  (0# * x + 1#) * x + 0#                ≈⟨ lemma₅ _ ⟩
  x                                     ∎

correct : ∀ {n} (p : Polynomial n) → ∀ ρ → ⟦ p ⟧↓ ρ ≈ ⟦ p ⟧ ρ
correct (op [+] p₁ p₂) ρ = begin
  ⟦ normalise p₁ +N normalise p₂ ⟧N ρ  ≈⟨ +N-homo (normalise p₁) (normalise p₂) ρ ⟩
  ⟦ p₁ ⟧↓ ρ + ⟦ p₂ ⟧↓ ρ                ≈⟨ correct p₁ ρ ⟨ +-cong ⟩ correct p₂ ρ ⟩
  ⟦ p₁ ⟧ ρ + ⟦ p₂ ⟧ ρ                  ∎
correct (op [*] p₁ p₂) ρ = begin
  ⟦ normalise p₁ *N normalise p₂ ⟧N ρ  ≈⟨ *N-homo (normalise p₁) (normalise p₂) ρ ⟩
  ⟦ p₁ ⟧↓ ρ * ⟦ p₂ ⟧↓ ρ                ≈⟨ correct p₁ ρ ⟨ *-cong ⟩ correct p₂ ρ ⟩
  ⟦ p₁ ⟧ ρ * ⟦ p₂ ⟧ ρ                  ∎
correct (con c)  ρ = correct-con c ρ
correct (var i)  ρ = correct-var i ρ
correct (p :^ k) ρ = begin
  ⟦ normalise p ^N k ⟧N ρ  ≈⟨ ^N-homo (normalise p) k ρ ⟩
  ⟦ p ⟧↓ ρ ^ k             ≈⟨ correct p ρ ⟨ ^-cong ⟩ ≡.refl {x = k} ⟩
  ⟦ p ⟧ ρ ^ k              ∎
correct (:- p) ρ = begin
  ⟦ -N normalise p ⟧N ρ  ≈⟨ -N‿-homo (normalise p) ρ ⟩
  - ⟦ p ⟧↓ ρ             ≈⟨ -‿cong (correct p ρ) ⟩
  - ⟦ p ⟧ ρ              ∎

------------------------------------------------------------------------
-- "Tactic.

open Reflection setoid var ⟦_⟧ ⟦_⟧↓ correct public
  using (prove; solve) renaming (_⊜_ to _:=_)

-- For examples of how solve and _:=_ can be used to
-- semi-automatically prove ring equalities, see, for instance,
-- Data.Digit or Data.Nat.DivMod.