------------------------------------------------------------------------
-- 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
$\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#2554}{\htmlId{3306}{\htmlClass{InductiveConstructor}{\text{op}}}}\, \,\href{Algebra.Solver.Ring.html#3309}{\htmlId{3309}{\htmlClass{Bound}{\text{o}}}}\, \,\href{Algebra.Solver.Ring.html#3311}{\htmlId{3311}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#3314}{\htmlId{3314}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#3311}{\htmlId{3325}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ ⟨ sem o ⟩ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#3314}{\htmlId{3344}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ
$\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#2627}{\htmlId{3353}{\htmlClass{InductiveConstructor}{\text{con}}}}\, \,\href{Algebra.Solver.Ring.html#3357}{\htmlId{3357}{\htmlClass{Bound}{\text{c}}}}\,      \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#3357}{\htmlId{3372}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$
$\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#2667}{\htmlId{3379}{\htmlClass{InductiveConstructor}{\text{var}}}}\, \,\href{Algebra.Solver.Ring.html#3383}{\htmlId{3383}{\htmlClass{Bound}{\text{x}}}}\,      \end{pmatrix}$ ρ = lookup ρ x
$\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#3409}{\htmlId{3409}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#2703}{\htmlId{3411}{\htmlClass{InductiveConstructor Operator}{\text{:^}}}}\, \,\href{Algebra.Solver.Ring.html#3414}{\htmlId{3414}{\htmlClass{Bound}{\text{n}}}}\,     \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#3409}{\htmlId{3428}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ^ n
$\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#2754}{\htmlId{3440}{\htmlClass{InductiveConstructor Operator}{\text{:-}}}}\, \,\href{Algebra.Solver.Ring.html#3443}{\htmlId{3443}{\htmlClass{Bound}{\text{p}}}}\,       \end{pmatrix}$ ρ = - $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#3443}{\htmlId{3461}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ

------------------------------------------------------------------------
-- 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
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4284}{\htmlId{4714}{\htmlClass{InductiveConstructor}{\text{∅}}}}\,       \end{pmatrix}$ _       = 0#
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4742}{\htmlId{4742}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#4308}{\htmlId{4744}{\htmlClass{InductiveConstructor Operator}{\text{*x+}}}}\, \,\href{Algebra.Solver.Ring.html#4748}{\htmlId{4748}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ (x ∷ ρ) = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4742}{\htmlId{4765}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4748}{\htmlId{4786}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ

  ⟦_⟧N : Normal n → Env n → Carrier
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4391}{\htmlId{4834}{\htmlClass{InductiveConstructor}{\text{con}}}}\, \,\href{Algebra.Solver.Ring.html#4838}{\htmlId{4838}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ _ = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4838}{\htmlId{4850}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4426}{\htmlId{4859}{\htmlClass{InductiveConstructor}{\text{poly}}}}\, \,\href{Algebra.Solver.Ring.html#4864}{\htmlId{4864}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4864}{\htmlId{4875}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ

------------------------------------------------------------------------
-- 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₂} → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#5282}{\htmlId{5293}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#5285}{\htmlId{5303}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ → 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₂ → ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6154}{\htmlId{6210}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6157}{\htmlId{6222}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#5064}{\htmlId{6234}{\htmlClass{InductiveConstructor}{\text{∅}}}}\,               \end{pmatrix}$ _       = refl
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6277}{\htmlId{6277}{\htmlClass{Bound}{\text{p₁≈p₂}}}}\, \,\href{Algebra.Solver.Ring.html#5093}{\htmlId{6283}{\htmlClass{InductiveConstructor Operator}{\text{*x+}}}}\, \,\href{Algebra.Solver.Ring.html#6287}{\htmlId{6287}{\htmlClass{Bound}{\text{c₁≈c₂}}}}\, \end{pmatrix}$ (x ∷ ρ) =
    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6277}{\htmlId{6318}{\htmlClass{Bound}{\text{p₁≈p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) ⟨ *-cong ⟩ refl)
      ⟨ +-cong ⟩
    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6287}{\htmlId{6380}{\htmlClass{Bound}{\text{c₁≈c₂}}}}\, \end{pmatrix}$ ρ

  ⟦_⟧N-cong : {p₁ p₂ : Normal n} →
              p₁ ≈N p₂ → ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6412}{\htmlId{6465}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6415}{\htmlId{6477}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#5272}{\htmlId{6489}{\htmlClass{InductiveConstructor}{\text{con}}}}\, \,\href{Algebra.Solver.Ring.html#6493}{\htmlId{6493}{\htmlClass{Bound}{\text{c₁≈c₂}}}}\,  \end{pmatrix}$ _ = c₁≈c₂
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#5332}{\htmlId{6522}{\htmlClass{InductiveConstructor}{\text{poly}}}}\, \,\href{Algebra.Solver.Ring.html#6527}{\htmlId{6527}{\htmlClass{Bound}{\text{p₁≈p₂}}}}\, \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6527}{\htmlId{6547}{\htmlClass{Bound}{\text{p₁≈p₂}}}}\, \end{pmatrix}$ ρ

------------------------------------------------------------------------
-- 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
$\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#9295}{\htmlId{9295}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8898}{\htmlId{9306}{\htmlClass{Function}{\text{normalise}}}}\, \,\href{Algebra.Solver.Ring.html#9295}{\htmlId{9316}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ

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

0N-homo : ∀ {n} ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6715}{\htmlId{9443}{\htmlClass{Function}{\text{0N}}}}\, \,\htmlId{9446}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Algebra.Solver.Ring.html#9434}{\htmlId{9447}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{9448}{\htmlClass{Symbol}{\text{}}}}\, \end{pmatrix}$ ρ ≈ 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# ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#9585}{\htmlId{9624}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ
0≈⟦0⟧ {c = c} c≈0 ρ = sym (begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#9642}{\htmlId{9668}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ ρ  ≈⟨ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#9645}{\htmlId{9682}{\htmlClass{Bound}{\text{c≈0}}}}\, \end{pmatrix}$ ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6715}{\htmlId{9702}{\htmlClass{Function}{\text{0N}}}}\, \end{pmatrix}$ ρ  ≈⟨ 0N-homo ρ ⟩
  0#         ∎)

1N-homo : ∀ {n} ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6838}{\htmlId{9765}{\htmlClass{Function}{\text{1N}}}}\, \,\htmlId{9768}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Algebra.Solver.Ring.html#9756}{\htmlId{9769}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{9770}{\htmlClass{Symbol}{\text{}}}}\, \end{pmatrix}$ ρ ≈ 1#
1N-homo []      = 1-homo
1N-homo (x ∷ ρ) = begin
  0# * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6838}{\htmlId{9844}{\htmlClass{Function}{\text{1N}}}}\, \end{pmatrix}$ ρ  ≈⟨ 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) →
            ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#9997}{\htmlId{10051}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#6936}{\htmlId{10053}{\htmlClass{Function Operator}{\text{*x+HN}}}}\, \,\href{Algebra.Solver.Ring.html#10015}{\htmlId{10059}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#9997}{\htmlId{10070}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{10072}{\htmlClass{InductiveConstructor Operator}{\text{*x+}}}\, \,\href{Algebra.Solver.Ring.html#10015}{\htmlId{10076}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ
*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 ρ ⟩
  $\begin{pmatrix} \,\htmlId{10230}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ           ≈⟨ sym $ lemma₆ _ _ ⟩
  0# * x + $\begin{pmatrix} \,\htmlId{10282}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ  ∎
... | nothing = refl

∅*x+HN-homo : ∀ {n} (c : Normal n) x ρ →
              $\begin{pmatrix} \,\htmlId{10371}{\htmlClass{InductiveConstructor}{\text{∅}}}\, \,\href{Algebra.Solver.Ring.html#6936}{\htmlId{10373}{\htmlClass{Function Operator}{\text{*x+HN}}}}\, \,\href{Algebra.Solver.Ring.html#10335}{\htmlId{10379}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ (x ∷ ρ) ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10335}{\htmlId{10396}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ
∅*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)) →
            ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10518}{\htmlId{10561}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{10564}{\htmlClass{Function Operator}{\text{+H}}}}\, \,\href{Algebra.Solver.Ring.html#10521}{\htmlId{10567}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10518}{\htmlId{10579}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10521}{\htmlId{10591}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ
  +H-homo ∅           p₂          ρ       = sym (+-identityˡ _)
  +H-homo (p₁ *x+ x₁) ∅           ρ       = sym (+-identityʳ _)
  +H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
    $\begin{pmatrix} (\,\href{Algebra.Solver.Ring.html#10738}{\htmlId{10784}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{10787}{\htmlClass{Function Operator}{\text{+H}}}}\, \,\href{Algebra.Solver.Ring.html#10750}{\htmlId{10790}{\htmlClass{Bound}{\text{p₂}}}}\,) \,\href{Algebra.Solver.Ring.html#6936}{\htmlId{10794}{\htmlClass{Function Operator}{\text{*x+HN}}}}\, (\,\href{Algebra.Solver.Ring.html#10745}{\htmlId{10801}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#7299}{\htmlId{10804}{\htmlClass{Function Operator}{\text{+N}}}}\, \,\href{Algebra.Solver.Ring.html#10757}{\htmlId{10807}{\htmlClass{Bound}{\text{c₂}}}}\,) \end{pmatrix}$ (x ∷ ρ)                           ≈⟨ *x+HN≈*x+ (p₁ +H p₂) (c₁ +N c₂) (x ∷ ρ) ⟩

    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10738}{\htmlId{10900}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{10903}{\htmlClass{Function Operator}{\text{+H}}}}\, \,\href{Algebra.Solver.Ring.html#10750}{\htmlId{10906}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10745}{\htmlId{10928}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#7299}{\htmlId{10931}{\htmlClass{Function Operator}{\text{+N}}}}\, \,\href{Algebra.Solver.Ring.html#10757}{\htmlId{10934}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ                        ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ +N-homo c₁ c₂ ρ ⟩

    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10738}{\htmlId{11045}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10750}{\htmlId{11063}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ)) * x + ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10745}{\htmlId{11087}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ρ + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10757}{\htmlId{11099}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ)  ≈⟨ lemma₁ _ _ _ _ _ ⟩

    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10738}{\htmlId{11139}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10745}{\htmlId{11161}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ρ) +
    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10750}{\htmlId{11179}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#10757}{\htmlId{11201}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ)                                  ∎

  +N-homo : ∀ {n} (p₁ p₂ : Normal n) →
            ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11265}{\htmlId{11305}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7299}{\htmlId{11308}{\htmlClass{Function Operator}{\text{+N}}}}\, \,\href{Algebra.Solver.Ring.html#11268}{\htmlId{11311}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11265}{\htmlId{11323}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11268}{\htmlId{11335}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ
  +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 ρ →
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11460}{\htmlId{11491}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7436}{\htmlId{11494}{\htmlClass{Function Operator}{\text{*x+H}}}}\, \,\href{Algebra.Solver.Ring.html#11463}{\htmlId{11499}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) ≈
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11460}{\htmlId{11519}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11463}{\htmlId{11541}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ)
*x+H-homo ∅         ∅ _ _ = sym $ lemma₆ _ _
*x+H-homo (p *x+ c) ∅ x ρ = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11611}{\htmlId{11638}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#4308}{\htmlId{11640}{\htmlClass{InductiveConstructor Operator}{\text{*x+}}}}\, \,\href{Algebra.Solver.Ring.html#11617}{\htmlId{11644}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6715}{\htmlId{11665}{\htmlClass{Function}{\text{0N}}}}\, \end{pmatrix}$ ρ  ≈⟨ refl ⟨ +-cong ⟩ 0N-homo ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11611}{\htmlId{11709}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#4308}{\htmlId{11711}{\htmlClass{InductiveConstructor Operator}{\text{*x+}}}}\, \,\href{Algebra.Solver.Ring.html#11617}{\htmlId{11715}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + 0#         ∎
*x+H-homo p₁         (p₂ *x+ c₂) x ρ = begin
  $\begin{pmatrix} (\,\href{Algebra.Solver.Ring.html#11757}{\htmlId{11797}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{11800}{\htmlClass{Function Operator}{\text{+H}}}}\, \,\href{Algebra.Solver.Ring.html#11769}{\htmlId{11803}{\htmlClass{Bound}{\text{p₂}}}}\,) \,\href{Algebra.Solver.Ring.html#6936}{\htmlId{11807}{\htmlClass{Function Operator}{\text{*x+HN}}}}\, \,\href{Algebra.Solver.Ring.html#11776}{\htmlId{11813}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ (x ∷ ρ)                         ≈⟨ *x+HN≈*x+ (p₁ +H p₂) c₂ (x ∷ ρ) ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11757}{\htmlId{11892}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{11895}{\htmlClass{Function Operator}{\text{+H}}}}\, \,\href{Algebra.Solver.Ring.html#11769}{\htmlId{11898}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11776}{\htmlId{11920}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ                    ≈⟨ (+H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ refl ⟩
  ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11757}{\htmlId{12013}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11769}{\htmlId{12031}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ)) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11776}{\htmlId{12054}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ      ≈⟨ lemma₀ _ _ _ _ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11757}{\htmlId{12091}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11769}{\htmlId{12114}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#11776}{\htmlId{12136}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ)  ∎

mutual

  *NH-homo :
    ∀ {n} (c : Normal n) (p : HNF (suc n)) x ρ →
    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#12181}{\htmlId{12225}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Algebra.Solver.Ring.html#7622}{\htmlId{12227}{\htmlClass{Function Operator}{\text{*NH}}}}\, \,\href{Algebra.Solver.Ring.html#12196}{\htmlId{12231}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (x ∷ ρ) ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#12181}{\htmlId{12248}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#12196}{\htmlId{12259}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (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# * ($\begin{pmatrix} \,\htmlId{12467}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{12488}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ)         ≈⟨ 0≈⟦0⟧ c≈0 ρ ⟨ *-cong ⟩ refl ⟩
    $\begin{pmatrix} \,\htmlId{12544}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ  * ($\begin{pmatrix} \,\htmlId{12557}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{12578}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ)  ∎
  ... | nothing = begin
    $\begin{pmatrix} \,\htmlId{12620}{\htmlClass{Bound}{\text{c}}}\, \,\href{Algebra.Solver.Ring.html#7622}{\htmlId{12622}{\htmlClass{Function Operator}{\text{*NH}}}}\, \,\htmlId{12626}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{12647}{\htmlClass{Bound}{\text{c}}}\, \,\href{Algebra.Solver.Ring.html#8167}{\htmlId{12649}{\htmlClass{Function Operator}{\text{*N}}}}\, \,\htmlId{12652}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ                 ≈⟨ (*NH-homo c p x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c c′ ρ ⟩
    ($\begin{pmatrix} \,\htmlId{12749}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\htmlId{12760}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ)) * x + ($\begin{pmatrix} \,\htmlId{12783}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\htmlId{12794}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ)  ≈⟨ lemma₃ _ _ _ _ ⟩
    $\begin{pmatrix} \,\htmlId{12830}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ * ($\begin{pmatrix} \,\htmlId{12842}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{12863}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ)               ∎

  *HN-homo :
    ∀ {n} (p : HNF (suc n)) (c : Normal n) x ρ →
    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#12913}{\htmlId{12957}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#7789}{\htmlId{12959}{\htmlClass{Function Operator}{\text{*HN}}}}\, \,\href{Algebra.Solver.Ring.html#12931}{\htmlId{12963}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ (x ∷ ρ) ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#12913}{\htmlId{12980}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (x ∷ ρ) * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#12931}{\htmlId{12997}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ
  *HN-homo ∅          c x ρ = sym (*-zeroˡ _)
  *HN-homo (p *x+ c′) c x ρ with c ≟N 0N
  ... | just c≈0 = begin
    0#                                           ≈⟨ sym (*-zeroʳ _) ⟩
    ($\begin{pmatrix} \,\htmlId{13193}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{13214}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ) * 0#        ≈⟨ refl ⟨ *-cong ⟩ 0≈⟦0⟧ c≈0 ρ ⟩
    ($\begin{pmatrix} \,\htmlId{13275}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{13296}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ) * $\begin{pmatrix} \,\htmlId{13309}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ  ∎
  ... | nothing = begin
    $\begin{pmatrix} \,\htmlId{13349}{\htmlClass{Bound}{\text{p}}}\, \,\href{Algebra.Solver.Ring.html#7789}{\htmlId{13351}{\htmlClass{Function Operator}{\text{*HN}}}}\, \,\htmlId{13355}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{13376}{\htmlClass{Bound}{\text{c′}}}\, \,\href{Algebra.Solver.Ring.html#8167}{\htmlId{13379}{\htmlClass{Function Operator}{\text{*N}}}}\, \,\htmlId{13382}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ                 ≈⟨ (*HN-homo p c x ρ ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ *N-homo c′ c ρ ⟩
    ($\begin{pmatrix} \,\htmlId{13478}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * $\begin{pmatrix} \,\htmlId{13495}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ) * x + ($\begin{pmatrix} \,\htmlId{13512}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\htmlId{13524}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ)  ≈⟨ lemma₂ _ _ _ _ ⟩
    ($\begin{pmatrix} \,\htmlId{13560}{\htmlClass{Bound}{\text{p}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\htmlId{13581}{\htmlClass{Bound}{\text{c′}}}\, \end{pmatrix}$ ρ) * $\begin{pmatrix} \,\htmlId{13594}{\htmlClass{Bound}{\text{c}}}\, \end{pmatrix}$ ρ               ∎

  *H-homo : ∀ {n} (p₁ p₂ : HNF (suc n)) →
            ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13637}{\htmlId{13680}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7956}{\htmlId{13683}{\htmlClass{Function Operator}{\text{*H}}}}\, \,\href{Algebra.Solver.Ring.html#13640}{\htmlId{13686}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13637}{\htmlId{13698}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13640}{\htmlId{13710}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ
  *H-homo ∅           p₂          ρ       = sym $ *-zeroˡ _
  *H-homo (p₁ *x+ c₁) ∅           ρ       = sym $ *-zeroʳ _
  *H-homo (p₁ *x+ c₁) (p₂ *x+ c₂) (x ∷ ρ) = begin
    $\begin{pmatrix} (\,\href{Algebra.Solver.Ring.html#13849}{\htmlId{13896}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7956}{\htmlId{13899}{\htmlClass{Function Operator}{\text{*H}}}}\, \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{13902}{\htmlClass{Bound}{\text{p₂}}}}\,) \,\href{Algebra.Solver.Ring.html#7436}{\htmlId{13906}{\htmlClass{Function Operator}{\text{*x+H}}}}\, (\,\href{Algebra.Solver.Ring.html#13849}{\htmlId{13913}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7789}{\htmlId{13916}{\htmlClass{Function Operator}{\text{*HN}}}}\, \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{13920}{\htmlClass{Bound}{\text{c₂}}}}\,) \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{13924}{\htmlClass{Function Operator}{\text{+H}}}}\, (\,\href{Algebra.Solver.Ring.html#13856}{\htmlId{13928}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#7622}{\htmlId{13931}{\htmlClass{Function Operator}{\text{*NH}}}}\, \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{13935}{\htmlClass{Bound}{\text{p₂}}}}\,) \,\href{Algebra.Solver.Ring.html#6936}{\htmlId{13941}{\htmlClass{Function Operator}{\text{*x+HN}}}}\,
      (\,\href{Algebra.Solver.Ring.html#13856}{\htmlId{13954}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#8167}{\htmlId{13957}{\htmlClass{Function Operator}{\text{*N}}}}\, \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{13960}{\htmlClass{Bound}{\text{c₂}}}}\,) \end{pmatrix}$ (x ∷ ρ)                                              ≈⟨ *x+HN≈*x+ ((p₁ *H p₂) *x+H ((p₁ *HN c₂) +H (c₁ *NH p₂)))
                                                                                      (c₁ *N c₂) (x ∷ ρ) ⟩
    $\begin{pmatrix} (\,\href{Algebra.Solver.Ring.html#13849}{\htmlId{14194}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7956}{\htmlId{14197}{\htmlClass{Function Operator}{\text{*H}}}}\, \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{14200}{\htmlClass{Bound}{\text{p₂}}}}\,) \,\href{Algebra.Solver.Ring.html#7436}{\htmlId{14204}{\htmlClass{Function Operator}{\text{*x+H}}}}\,
      (\,\href{Algebra.Solver.Ring.html#13849}{\htmlId{14217}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7789}{\htmlId{14220}{\htmlClass{Function Operator}{\text{*HN}}}}\, \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{14224}{\htmlClass{Bound}{\text{c₂}}}}\,) \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{14228}{\htmlClass{Function Operator}{\text{+H}}}}\, (\,\href{Algebra.Solver.Ring.html#13856}{\htmlId{14232}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#7622}{\htmlId{14235}{\htmlClass{Function Operator}{\text{*NH}}}}\, \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{14239}{\htmlClass{Bound}{\text{p₂}}}}\,) \end{pmatrix}$ (x ∷ ρ) * x +
    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13856}{\htmlId{14267}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#8167}{\htmlId{14270}{\htmlClass{Function Operator}{\text{*N}}}}\, \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{14273}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ                                                      ≈⟨ (*x+H-homo (p₁ *H p₂) ((p₁ *HN c₂) +H (c₁ *NH p₂)) x ρ
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            *N-homo c₁ c₂ ρ ⟩
    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13849}{\htmlId{14755}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7956}{\htmlId{14758}{\htmlClass{Function Operator}{\text{*H}}}}\, \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{14761}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x +
     $\begin{pmatrix} (\,\href{Algebra.Solver.Ring.html#13849}{\htmlId{14789}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7789}{\htmlId{14792}{\htmlClass{Function Operator}{\text{*HN}}}}\, \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{14796}{\htmlClass{Bound}{\text{c₂}}}}\,) \,\href{Algebra.Solver.Ring.html#7124}{\htmlId{14800}{\htmlClass{Function Operator}{\text{+H}}}}\, (\,\href{Algebra.Solver.Ring.html#13856}{\htmlId{14804}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#7622}{\htmlId{14807}{\htmlClass{Function Operator}{\text{*NH}}}}\, \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{14811}{\htmlClass{Bound}{\text{p₂}}}}\,) \end{pmatrix}$ (x ∷ ρ)) * x +
    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13856}{\htmlId{14839}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{14851}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ                                                ≈⟨ (((*H-homo p₁ p₂ (x ∷ ρ) ⟨ *-cong ⟩ refl)
                                                                                ⟨ +-cong ⟩
                                                                              (+H-homo (p₁ *HN c₂) (c₁ *NH p₂) (x ∷ ρ)))
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            refl ⟩
    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13849}{\htmlId{15515}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{15533}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x +
     ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13849}{\htmlId{15561}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7789}{\htmlId{15564}{\htmlClass{Function Operator}{\text{*HN}}}}\, \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{15568}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ (x ∷ ρ) + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13856}{\htmlId{15586}{\htmlClass{Bound}{\text{c₁}}}}\, \,\href{Algebra.Solver.Ring.html#7622}{\htmlId{15589}{\htmlClass{Function Operator}{\text{*NH}}}}\, \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{15593}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ))) * x +
    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13856}{\htmlId{15621}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{15633}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ                                                ≈⟨ ((refl ⟨ +-cong ⟩ (*HN-homo p₁ c₂ x ρ ⟨ +-cong ⟩ *NH-homo c₁ p₂ x ρ))
                                                                               ⟨ *-cong ⟩
                                                                             refl)
                                                                              ⟨ +-cong ⟩
                                                                            refl ⟩
    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13849}{\htmlId{16113}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{16131}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x +
     ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13849}{\htmlId{16159}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{16177}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13856}{\htmlId{16189}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{16201}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ))) * x +
    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13856}{\htmlId{16230}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{16242}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ)                                              ≈⟨ lemma₄ _ _ _ _ _ ⟩

    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13849}{\htmlId{16326}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13856}{\htmlId{16348}{\htmlClass{Bound}{\text{c₁}}}}\, \end{pmatrix}$ ρ) *
    ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13861}{\htmlId{16366}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ (x ∷ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#13868}{\htmlId{16388}{\htmlClass{Bound}{\text{c₂}}}}\, \end{pmatrix}$ ρ)                                    ∎

  *N-homo : ∀ {n} (p₁ p₂ : Normal n) →
            ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16454}{\htmlId{16494}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#8167}{\htmlId{16497}{\htmlClass{Function Operator}{\text{*N}}}}\, \,\href{Algebra.Solver.Ring.html#16457}{\htmlId{16500}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16454}{\htmlId{16512}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16457}{\htmlId{16524}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ
  *N-homo (con c₁)  (con c₂)  _ = *-homo _ _
  *N-homo (poly p₁) (poly p₂) ρ = *H-homo p₁ p₂ ρ

^N-homo : ∀ {n} (p : Normal n) (k : ℕ) →
          ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16645}{\htmlId{16687}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#8304}{\htmlId{16689}{\htmlClass{Function Operator}{\text{^N}}}}\, \,\href{Algebra.Solver.Ring.html#16660}{\htmlId{16692}{\htmlClass{Bound}{\text{k}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16645}{\htmlId{16703}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ^ k
^N-homo p zero    ρ = 1N-homo ρ
^N-homo p (suc k) ρ = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16754}{\htmlId{16778}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#8167}{\htmlId{16780}{\htmlClass{Function Operator}{\text{*N}}}}\, (\,\href{Algebra.Solver.Ring.html#16754}{\htmlId{16784}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#8304}{\htmlId{16786}{\htmlClass{Function Operator}{\text{^N}}}}\, \,\href{Algebra.Solver.Ring.html#16761}{\htmlId{16789}{\htmlClass{Bound}{\text{k}}}}\,) \end{pmatrix}$ ρ       ≈⟨ *N-homo p (p ^N k) ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16754}{\htmlId{16833}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16754}{\htmlId{16844}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#8304}{\htmlId{16846}{\htmlClass{Function Operator}{\text{^N}}}}\, \,\href{Algebra.Solver.Ring.html#16761}{\htmlId{16849}{\htmlClass{Bound}{\text{k}}}}\, \end{pmatrix}$ ρ   ≈⟨ refl ⟨ *-cong ⟩ ^N-homo p k ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16754}{\htmlId{16897}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ * ($\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16754}{\htmlId{16909}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ^ k)  ∎

mutual

  -H‿-homo : ∀ {n} (p : HNF (suc n)) →
             ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8405}{\htmlId{16993}{\htmlClass{Function Operator}{\text{-H}}}}\, \,\href{Algebra.Solver.Ring.html#16953}{\htmlId{16996}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ≈ - $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#16953}{\htmlId{17009}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ
  -H‿-homo p (x ∷ ρ) = begin
    $\begin{pmatrix} (\,\href{Algebra.Solver.Ring.html#8463}{\htmlId{17052}{\htmlClass{Function Operator}{\text{-N}}}}\, \,\href{Algebra.Solver.Ring.html#6838}{\htmlId{17055}{\htmlClass{Function}{\text{1N}}}}\,) \,\href{Algebra.Solver.Ring.html#7622}{\htmlId{17059}{\htmlClass{Function Operator}{\text{*NH}}}}\, \,\href{Algebra.Solver.Ring.html#17027}{\htmlId{17063}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (x ∷ ρ)     ≈⟨ *NH-homo (-N 1N) p x ρ ⟩
    $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8463}{\htmlId{17114}{\htmlClass{Function Operator}{\text{-N}}}}\, \,\href{Algebra.Solver.Ring.html#6838}{\htmlId{17117}{\htmlClass{Function}{\text{1N}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#17027}{\htmlId{17129}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (x ∷ ρ)  ≈⟨ trans (-N‿-homo 1N ρ) (-‿cong (1N-homo ρ)) ⟨ *-cong ⟩ refl ⟩
    - 1# * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#17027}{\htmlId{17220}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (x ∷ ρ)          ≈⟨ lemma₇ _ ⟩
    - $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#17027}{\htmlId{17264}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ (x ∷ ρ)               ∎

  -N‿-homo : ∀ {n} (p : Normal n) →
             ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8463}{\htmlId{17351}{\htmlClass{Function Operator}{\text{-N}}}}\, \,\href{Algebra.Solver.Ring.html#17314}{\htmlId{17354}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ≈ - $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#17314}{\htmlId{17367}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ
  -N‿-homo (con c)  _ = -‿homo _
  -N‿-homo (poly p) ρ = -H‿-homo p ρ

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

correct-con : ∀ {n} (c : C.Carrier) (ρ : Env n) →
              $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8633}{\htmlId{17600}{\htmlClass{Function}{\text{normalise-con}}}}\, \,\href{Algebra.Solver.Ring.html#17555}{\htmlId{17614}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#17555}{\htmlId{17625}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$
correct-con c []      = refl
correct-con c (x ∷ ρ) = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4284}{\htmlId{17693}{\htmlClass{InductiveConstructor}{\text{∅}}}}\, \,\href{Algebra.Solver.Ring.html#6936}{\htmlId{17695}{\htmlClass{Function Operator}{\text{*x+HN}}}}\, \,\href{Algebra.Solver.Ring.html#8633}{\htmlId{17701}{\htmlClass{Function}{\text{normalise-con}}}}\, \,\href{Algebra.Solver.Ring.html#17671}{\htmlId{17715}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ (x ∷ ρ)  ≈⟨ ∅*x+HN-homo (normalise-con c) x ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8633}{\htmlId{17772}{\htmlClass{Function}{\text{normalise-con}}}}\, \,\href{Algebra.Solver.Ring.html#17671}{\htmlId{17786}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ ρ            ≈⟨ correct-con c ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#17671}{\htmlId{17829}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$                                   ∎

correct-var : ∀ {n} (i : Fin n) →
              ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8760}{\htmlId{17927}{\htmlClass{Function}{\text{normalise-var}}}}\, \,\href{Algebra.Solver.Ring.html#17892}{\htmlId{17941}{\htmlClass{Bound}{\text{i}}}}\, \end{pmatrix}$ ρ ≈ lookup ρ i
correct-var (suc i) (x ∷ ρ) = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#4284}{\htmlId{18001}{\htmlClass{InductiveConstructor}{\text{∅}}}}\, \,\href{Algebra.Solver.Ring.html#6936}{\htmlId{18003}{\htmlClass{Function Operator}{\text{*x+HN}}}}\, \,\href{Algebra.Solver.Ring.html#8760}{\htmlId{18009}{\htmlClass{Function}{\text{normalise-var}}}}\, \,\href{Algebra.Solver.Ring.html#17978}{\htmlId{18023}{\htmlClass{Bound}{\text{i}}}}\, \end{pmatrix}$ (x ∷ ρ)  ≈⟨ ∅*x+HN-homo (normalise-var i) x ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8760}{\htmlId{18080}{\htmlClass{Function}{\text{normalise-var}}}}\, \,\href{Algebra.Solver.Ring.html#17978}{\htmlId{18094}{\htmlClass{Bound}{\text{i}}}}\, \end{pmatrix}$ ρ                ≈⟨ correct-var i ρ ⟩
  lookup ρ i                            ∎
correct-var zero (x ∷ ρ) = begin
  (0# * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6838}{\htmlId{18226}{\htmlClass{Function}{\text{1N}}}}\, \end{pmatrix}$ ρ) * x + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#6715}{\htmlId{18243}{\htmlClass{Function}{\text{0N}}}}\, \end{pmatrix}$ ρ  ≈⟨ ((refl ⟨ +-cong ⟩ 1N-homo ρ) ⟨ *-cong ⟩ refl) ⟨ +-cong ⟩ 0N-homo ρ ⟩
  (0# * x + 1#) * x + 0#                ≈⟨ lemma₅ _ ⟩
  x                                     ∎

correct : ∀ {n} (p : Polynomial n) → ∀ ρ → $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18438}{\htmlId{18466}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ≈ $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18438}{\htmlId{18477}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ
correct (op [+] p₁ p₂) ρ = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8898}{\htmlId{18520}{\htmlClass{Function}{\text{normalise}}}}\, \,\href{Algebra.Solver.Ring.html#18499}{\htmlId{18530}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#7299}{\htmlId{18533}{\htmlClass{Function Operator}{\text{+N}}}}\, \,\href{Algebra.Solver.Ring.html#8898}{\htmlId{18536}{\htmlClass{Function}{\text{normalise}}}}\, \,\href{Algebra.Solver.Ring.html#18502}{\htmlId{18546}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ  ≈⟨ +N-homo (normalise p₁) (normalise p₂) ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18499}{\htmlId{18604}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18502}{\htmlId{18616}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ                ≈⟨ correct p₁ ρ ⟨ +-cong ⟩ correct p₂ ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18499}{\htmlId{18685}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ + $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18502}{\htmlId{18696}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ                  ∎
correct (op [*] p₁ p₂) ρ = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8898}{\htmlId{18759}{\htmlClass{Function}{\text{normalise}}}}\, \,\href{Algebra.Solver.Ring.html#18738}{\htmlId{18769}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Algebra.Solver.Ring.html#8167}{\htmlId{18772}{\htmlClass{Function Operator}{\text{*N}}}}\, \,\href{Algebra.Solver.Ring.html#8898}{\htmlId{18775}{\htmlClass{Function}{\text{normalise}}}}\, \,\href{Algebra.Solver.Ring.html#18741}{\htmlId{18785}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ  ≈⟨ *N-homo (normalise p₁) (normalise p₂) ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18738}{\htmlId{18843}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18741}{\htmlId{18855}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ                ≈⟨ correct p₁ ρ ⟨ *-cong ⟩ correct p₂ ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18738}{\htmlId{18924}{\htmlClass{Bound}{\text{p₁}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#18741}{\htmlId{18935}{\htmlClass{Bound}{\text{p₂}}}}\, \end{pmatrix}$ ρ                  ∎
correct (con c)  ρ = correct-con c ρ
correct (var i)  ρ = correct-var i ρ
correct (p :^ k) ρ = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8898}{\htmlId{19066}{\htmlClass{Function}{\text{normalise}}}}\, \,\href{Algebra.Solver.Ring.html#19044}{\htmlId{19076}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Algebra.Solver.Ring.html#8304}{\htmlId{19078}{\htmlClass{Function Operator}{\text{^N}}}}\, \,\href{Algebra.Solver.Ring.html#19049}{\htmlId{19081}{\htmlClass{Bound}{\text{k}}}}\, \end{pmatrix}$ ρ  ≈⟨ ^N-homo (normalise p) k ρ ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#19044}{\htmlId{19124}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ^ k             ≈⟨ correct p ρ ⟨ ^-cong ⟩ ≡.refl {x = k} ⟩
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#19044}{\htmlId{19194}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ ^ k              ∎
correct (:- p) ρ = begin
  $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#8463}{\htmlId{19248}{\htmlClass{Function Operator}{\text{-N}}}}\, \,\href{Algebra.Solver.Ring.html#8898}{\htmlId{19251}{\htmlClass{Function}{\text{normalise}}}}\, \,\href{Algebra.Solver.Ring.html#19231}{\htmlId{19261}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ  ≈⟨ -N‿-homo (normalise p) ρ ⟩
  - $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#19231}{\htmlId{19305}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ             ≈⟨ -‿cong (correct p ρ) ⟩
  - $\begin{pmatrix} \,\href{Algebra.Solver.Ring.html#19231}{\htmlId{19356}{\htmlClass{Bound}{\text{p}}}}\, \end{pmatrix}$ ρ              ∎

------------------------------------------------------------------------
-- "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.