```------------------------------------------------------------------------
-- 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.Binary
open import Relation.Nullary using (yes; no)
open import Relation.Binary.Reasoning.Setoid setoid
import Relation.Binary.PropositionalEquality as PropEq
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
open import Level using (_⊔_)

infix  9 :-_ -H_ -N_
infixr 9 _:×_ _:^_ _^N_
infix  8 _*x+_ _*x+HN_ _*x+H_
infixl 8 _:*_ _*N_ _*H_ _*NH_ _*HN_
infixl 7 _:+_ _:-_ _+H_ _+N_
infix  4 _≈H_ _≈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.

_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:+_ = op [+]

_:*_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:*_ = op [*]

_:-_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
x :- y = x :+ :- y

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

-- Semantics.

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

⟦_⟧ : ∀ {n} → Polynomial n → Vec Carrier 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
∅     : ∀ {n} → HNF (suc n)
_*x+_ : ∀ {n} → HNF (suc n) → Normal n → HNF (suc n)

data Normal : ℕ → Set r₁ where
con  : C.Carrier → Normal zero
poly : ∀ {n} → 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 : ∀ {n} → HNF (suc n) → Vec Carrier (suc n) → Carrier
⟦ ∅       ⟧H _       = 0#
⟦ p *x+ c ⟧H (x ∷ ρ) = ⟦ p ⟧H (x ∷ ρ) * x + ⟦ c ⟧N ρ

⟦_⟧N : ∀ {n} → Normal n → Vec Carrier n → Carrier
⟦ con c  ⟧N _ = ⟦ c ⟧′
⟦ poly p ⟧N ρ = ⟦ p ⟧H ρ

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

mutual

-- Equality.

data _≈H_ : ∀ {n} → HNF n → HNF n → Set (r₁ ⊔ r₃) where
∅     : ∀ {n} → _≈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_ : ∀ {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.

_≟H_ : ∀ {n} → 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_ : ∀ {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 : ∀ {n} {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 :
∀ {n} {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 : ∀ {n} → HNF (suc n)
0H = ∅

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

mutual

-- One.

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

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

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

_*x+HN_ : ∀ {n} → 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

_+H_ : ∀ {n} → 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_ : ∀ {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_ : ∀ {n} → 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_ : ∀ {n} → 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_ : ∀ {n} → 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_ : ∀ {n} → 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_ : ∀ {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_ : ∀ {n} → Normal n → ℕ → Normal n
p ^N zero  = 1N
p ^N suc n = p *N (p ^N n)

mutual

-- Negation.

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

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

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

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

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

normalise : ∀ {n} → 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.

⟦_⟧↓ : ∀ {n} → Polynomial n → Vec Carrier 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) (ρ : Vec Carrier 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 ⟩ PropEq.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.
```