polynomial algebra over a ring

polynomials.agda

open import Level using (suc; _⊔_)
open import Function using (id; _∘_)

open import Data.List as List using (
    List; []; _∷_; [_]; map; reverse; align; alignWith; foldr; head; last; drop; length
    )
import Data.List.Properties as List
import Data.List.Relation.Unary.All as All
import Data.List.Relation.Binary.Pointwise as PW

open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Product as Product using (_×_; _,_)
open import Data.Maybe as Maybe using (Maybe; fromMaybe)
import Data.Maybe.Relation.Unary.All as Maybe
import Data.These as These
import Data.These.Properties as These
open import Data.Nat as ℕ using (ℕ)
import Data.Nat.Properties as ℕ
open import Algebra.Bundles using (CommutativeRing)
open import Relation.Nullary as Dec using (¬_; Dec)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_) renaming (refl to ≡-refl)
import Relation.Binary.Reasoning.Setoid as Reasoning

-- two crucial choices have to be made regarding definition of polynomials
--  1. whether to make it normalized or not
--      if normalized:
--        degree is known
--        equality is list equality
--      if not:
--        no need to prove normalization
--  2. whether to make it LE or BE
--      if LE:
--        basic polynomial operations (_+_, _*_, _∣_, _≈_) are simple
--      if BE:
--        complex operations (degree, division, normalized proofs for product) are simple
--
-- and a third one, which is whether to allow 0-length coefficients or always force non-empty list

module polynomials {c} {ℓ} (ring : CommutativeRing c ℓ) where
    private
        module R where
            open CommutativeRing ring public

    open CommutativeRing ring renaming (Carrier to Rₛ) using ()
    --    Carrier to R; _≈_ to _≈R_; _+_ to _+R_; _*_ to _*R_; ) using ()

    Polynomial = List Rₛ
    -- coefficients, with least significant being head

    0# : Polynomial
    0# = []

    -- scalars can be embedded as polynomials

    scalar : Rₛ → Polynomial
    scalar = [_]

    1# : Polynomial
    1# = scalar R.1#

    -- evaluation, N-th coefficient

    private
        evalStep = λ x k res → k R.+ x R.* res

    _∣_ : Polynomial → Rₛ → Rₛ
    P ∣ x = foldr (evalStep x) R.0# P

    _⟨_⟩ : List Rₛ → ℕ → Rₛ
    [] ⟨ k ⟩            = R.0#
    (x ∷ P) ⟨ ℕ.zero ⟩  = x
    (x ∷ P) ⟨ ℕ.suc k ⟩ = P ⟨ k ⟩

    -- polynomials are an R-module

    infix 6 -_
    infixl 6 _+_ _-_
    infixl 7 _*_ _*S_

    _*S_ : Rₛ → Polynomial → Polynomial
    k *S P = map (k R.*_) P

    -_ : Polynomial → Polynomial
    -_ = map (R.-_)

    _+_ : Polynomial → Polynomial → Polynomial
    _+_ = alignWith (These.fold id id R._+_)

    _-_ : Polynomial → Polynomial → Polynomial
    P - Q = P + (- Q)

    -- polynomials are an R-algebra

    private
        *-step = λ K res → K ⟨ 0 ⟩ ∷ (drop 1 K + res)

    _*_ : Polynomial → Polynomial → Polynomial
    P * Q = foldr *-step 0# (map (_*S Q) P)

    -- degree predicates

    private
        pred : ℕ → Maybe ℕ
        pred 0         = Maybe.nothing
        pred (ℕ.suc n) = Maybe.just n

    -- Norm≤ : ℕ → Polynomial → Set ℓ
    -- Norm≤ n P = drop n P ≈ 0#

    -- Norm≡ : ℕ → Polynomial → Set ℓ
    -- Norm≡ n P = IsBelowDegree n P × Maybe.All ((R._≉ R.0#) ∘ P ⟨_⟩) (pred n)

    IsBelowDegree : ℕ → Polynomial → Set ℓ
    IsBelowDegree n P = ∀ {k} → n ℕ.≤ k → P ⟨ k ⟩ R.≈ R.0#

    FitsDegree : ℕ → Polynomial → Set ℓ
    FitsDegree = IsBelowDegree ∘ ℕ.suc

    IsDegree : ℕ → Polynomial → Set ℓ
    -- IsDegree n P = FitsDegree n P × (P ⟨ n ⟩ R.≉ R.0# ⊎ n ≡ 0)
    IsDegree 0 P = FitsDegree 0 P
    IsDegree n P = FitsDegree n P × P ⟨ n ⟩ R.≉ R.0#

    IsDegree⇒FitsDegree : ∀ {n P} → IsDegree n P → FitsDegree n P
    IsDegree⇒FitsDegree {0}       deg       = deg
    IsDegree⇒FitsDegree {ℕ.suc n} (deg , _) = deg

    FitsDegree∧NonZero⇒IsDegree : ∀ {n P} → FitsDegree n P → P ⟨ n ⟩ R.≉ R.0# → IsDegree n P
    FitsDegree∧NonZero⇒IsDegree {0}       deg _  = deg
    FitsDegree∧NonZero⇒IsDegree {ℕ.suc n} deg nz = deg , nz

    -- special polynomials

    root : Rₛ → Polynomial
    root r = (R.- r) ∷ 1#

    identity = root R.0#

    -- equality

    infix 4 _≈_ _≉_

    data _≈_ (P Q : Polynomial) : Set ℓ where
      mk≈ : (∀ k → P ⟨ k ⟩ R.≈ Q ⟨ k ⟩) → P ≈ Q

    ≈⟨⟩ : ∀ {P Q} → P ≈ Q → ∀ k → P ⟨ k ⟩ R.≈ Q ⟨ k ⟩
    ≈⟨⟩ (mk≈ f) = f

    _≉_ : Polynomial → Polynomial → Set ℓ
    P ≉ Q = ¬ (P ≈ Q)

    -- lower / raise degree

    lower : ℕ → Polynomial → Polynomial
    lower = drop

    raise : ℕ → Polynomial → Polynomial
    raise ℕ.zero    P = P
    raise (ℕ.suc k) P = R.0# ∷ P

    -- normalization

    IsNormalized : Polynomial → Set (c ⊔ ℓ)
    IsNormalized P = Maybe.All (R._≉ R.0#) (last P)

    0#normal : IsNormalized 0#
    0#normal = Maybe.nothing

    -- properties of _≈_

    refl : ∀ {P} → P ≈ P
    refl = mk≈ λ k → R.refl

    sym : ∀ {P Q} → P ≈ Q → Q ≈ P
    sym P≈Q = mk≈ λ k → R.sym (≈⟨⟩ P≈Q k)

    trans : ∀ {P Q R} → P ≈ Q → Q ≈ R → P ≈ R
    trans P≈Q Q≈R = mk≈ λ k → R.trans (≈⟨⟩ P≈Q k) (≈⟨⟩ Q≈R k)

    setoid : Setoid c ℓ
    setoid = record {
        Carrier = Polynomial; _≈_ = _≈_;
        isEquivalence = record { refl = refl; sym = sym; trans = trans } }

    -- properties of fromList, raise, drop

    ⟨⟩-lower : ∀ n P k → (lower n P) ⟨ k ⟩ ≡ P ⟨ n ℕ.+ k ⟩
    ⟨⟩-lower ℕ.zero    P       k = PropEq.refl
    ⟨⟩-lower (ℕ.suc n) []      k = PropEq.refl
    ⟨⟩-lower (ℕ.suc n) (x ∷ P) k = ⟨⟩-lower n P k

    lower-≈ : ∀ n {P Q} → P ≈ Q → lower n P ≈ lower n Q
    lower-≈ n {P} {Q} P≈Q = mk≈ helper
      where
        helper : ∀ k → (lower n P) ⟨ k ⟩ R.≈ (lower n Q) ⟨ k ⟩
        helper k
          rewrite ⟨⟩-lower n P k
          rewrite ⟨⟩-lower n Q k
          = ≈⟨⟩ P≈Q (n ℕ.+ k)

    head-≈ : ∀ {P Q} → P ≈ Q → P ⟨ 0 ⟩ R.≈ Q ⟨ 0 ⟩
    head-≈ P = ≈⟨⟩ P 0
    tail-≈ = lower-≈ 1
    uncons-≈ : ∀ {P Q} → P ≈ Q → (P ⟨ 0 ⟩ R.≈ Q ⟨ 0 ⟩) × (lower 1 P ≈ lower 1 Q)
    uncons-≈ P≈Q = head-≈ P≈Q , tail-≈ P≈Q

    ∷-≈ : ∀ {k l P Q} → k R.≈ l → P ≈ Q → k ∷ P ≈ l ∷ Q
    ∷-≈ k≈l P≈Q = mk≈ λ where
      0         → k≈l
      (ℕ.suc k) → ≈⟨⟩ P≈Q k

    zero≈0 : scalar R.0# ≈ 0#
    zero≈0 = mk≈ λ where
      0         → R.refl
      (ℕ.suc k) → R.refl

    scalar-≈ : ∀ {k l} → k R.≈ l → scalar k ≈ scalar l
    scalar-≈ k≈l = mk≈ λ where
      0         → k≈l
      (ℕ.suc k) → R.refl

    -- normalization

    -- -- -- module _ (≈?0 : ∀ k → Dec (k R.≈ R.0#)) where
    -- -- --     normalized : Polynomial → Polynomial
    -- -- --     normalized P = {!   !}

    -- -- --     normalized-≈ : ∀ P → normalized P ≈ P
    -- -- --     normalized-≈ P = {!   !}

    -- -- --     normalized-idempotent : ∀ P → normalized (normalized P) ≡ normalized P
    -- -- --     normalized-idempotent P = ?

    -- (stronger) list equality

    open import Data.List.Relation.Binary.Equality.Setoid R.setoid
        as ListEq using (_≋_)

    -- ≋⇒≈ : ∀ {P Q} → P ≋ Q → P ≈ Q
    -- ≋⇒≈ P≋Q k = {!   !}

    -- ≈⇒≋ : ∀ {P Q} → P ≈ Q → length P ≡ length Q → P ≋ Q
    -- ≈⇒≋ P≈Q leneq = {!   !}

    -- properties of _+_

    +-⟨⟩ : ∀ P Q k → P ⟨ k ⟩ R.+ Q ⟨ k ⟩ R.≈ (P + Q) ⟨ k ⟩
    +-⟨⟩ []      []      0 = R.+-identityˡ R.0#
    +-⟨⟩ []      (x ∷ Q) 0 = R.+-identityˡ x
    +-⟨⟩ (x ∷ P) []      0 = R.+-identityʳ x
    +-⟨⟩ (x ∷ P) (y ∷ Q) 0 = R.refl
    +-⟨⟩ []      []      (ℕ.suc k) = R.+-identityˡ R.0#
    +-⟨⟩ []      (x ∷ Q) (ℕ.suc k) rewrite List.map-id Q = R.+-identityˡ (Q ⟨ k ⟩)
    +-⟨⟩ (x ∷ P) []      (ℕ.suc k) rewrite List.map-id P = R.+-identityʳ (P ⟨ k ⟩)
    +-⟨⟩ (x ∷ P) (y ∷ Q) (ℕ.suc k) = +-⟨⟩ P Q k

    +-comm : ∀ P Q → P + Q ≈ Q + P
    +-comm P Q = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
        (P + Q) ₖ    ≈⟨ R.sym (+-⟨⟩ P Q k) ⟩
        P ₖ R.+ Q ₖ  ≈⟨ R.+-comm (P ₖ) (Q ₖ) ⟩
        Q ₖ R.+ P ₖ  ≈⟨ +-⟨⟩ Q P k ⟩
        (Q + P) ₖ    ∎
      where open Reasoning R.setoid

    +-assoc : ∀ P Q R → (P + Q) + R ≈ P + (Q + R)
    +-assoc P Q R = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
        ((P + Q) + R) ₖ        ≈⟨ R.sym (+-⟨⟩ (P + Q) R k) ⟩
        (P + Q) ₖ R.+ R ₖ      ≈⟨ R.sym (R.+-congʳ (+-⟨⟩ P Q k)) ⟩
        (P ₖ R.+ Q ₖ) R.+ R ₖ  ≈⟨ R.+-assoc (P ₖ) (Q ₖ) (R ₖ) ⟩
        P ₖ R.+ (Q ₖ R.+ R ₖ)  ≈⟨ R.+-congˡ (+-⟨⟩ Q R k) ⟩
        P ₖ R.+ (Q + R) ₖ      ≈⟨ +-⟨⟩ P (Q + R) k ⟩
        (P + (Q + R)) ₖ        ∎
      where open Reasoning R.setoid

    +-cong : ∀ {P Q R S} → P ≈ Q → R ≈ S → P + R ≈ Q + S
    +-cong {P} {Q} {R} {S} P≈Q R≈S = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
        (P + R) ₖ    ≈⟨ R.sym (+-⟨⟩ P R k) ⟩
        P ₖ R.+ R ₖ  ≈⟨ R.+-cong (≈⟨⟩ P≈Q k) (≈⟨⟩ R≈S k) ⟩
        Q ₖ R.+ S ₖ  ≈⟨ +-⟨⟩ Q S k ⟩
        (Q + S) ₖ    ∎
      where open Reasoning R.setoid

    -- properties of _*S_

    *S-⟨⟩ : ∀ l P k → (l *S P) ⟨ k ⟩ R.≈ l R.* P ⟨ k ⟩
    *S-⟨⟩ l []      ℕ.zero    = R.sym (R.zeroʳ l)
    *S-⟨⟩ l []      (ℕ.suc k) = R.sym (R.zeroʳ l)
    *S-⟨⟩ l (x ∷ P) ℕ.zero    = R.refl
    *S-⟨⟩ l (x ∷ P) (ℕ.suc k) = *S-⟨⟩ l P k

    *S-idˡ : ∀ P → R.1# *S P ≈ P
    *S-idˡ P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in
      R.trans (*S-⟨⟩ R.1# P k) (R.*-identityˡ (P ₖ))

    *S-zeroˡ : ∀ P → R.0# *S P ≈ 0#
    *S-zeroˡ P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in
      R.trans (*S-⟨⟩ R.0# P k) (R.zeroˡ (P ₖ))

    *S-cong : ∀ {l m P Q} → l R.≈ m → P ≈ Q → l *S P ≈ m *S Q
    *S-cong {l} {m} {P} {Q} l≈m P≈Q = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
        (l *S P) ₖ  ≈⟨ *S-⟨⟩ l P k ⟩
        l R.* P ₖ   ≈⟨ R.*-cong l≈m (≈⟨⟩ P≈Q k) ⟩
        m R.* Q ₖ   ≈⟨ R.sym (*S-⟨⟩ m Q k) ⟩
        (m *S Q) ₖ  ∎
      where open Reasoning R.setoid

    *S-distrˡ : ∀ l P Q → l *S (P + Q) ≈ l *S P + l *S Q
    *S-distrˡ l P Q = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
        (l *S (P + Q)) ₖ           ≈⟨ *S-⟨⟩ l (P + Q) k ⟩
        l R.* (P + Q) ₖ            ≈⟨ R.sym (R.*-congˡ (+-⟨⟩ P Q k)) ⟩
        l R.* (P ₖ R.+ Q ₖ)        ≈⟨ R.distribˡ l (P ₖ) (Q ₖ) ⟩
        l R.* P ₖ R.+ l R.* Q ₖ    ≈⟨ R.sym (R.+-cong (*S-⟨⟩ l P k) (*S-⟨⟩ l Q k)) ⟩
        (l *S P) ₖ R.+ (l *S Q) ₖ  ≈⟨ +-⟨⟩ (l *S P) (l *S Q) k ⟩
        (l *S P + l *S Q) ₖ        ∎
      where open Reasoning R.setoid

    *S-distrʳ : ∀ l m P → (l R.+ m) *S P ≈ l *S P + m *S P
    *S-distrʳ l m P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
        ((l R.+ m) *S P) ₖ         ≈⟨ *S-⟨⟩ (l R.+ m) P k ⟩
        (l R.+ m) R.* P ₖ          ≈⟨ R.distribʳ (P ₖ) l m ⟩
        l R.* P ₖ R.+ m R.* P ₖ    ≈⟨ R.sym (R.+-cong (*S-⟨⟩ l P k) (*S-⟨⟩ m P k)) ⟩
        (l *S P) ₖ R.+ (m *S P) ₖ  ≈⟨ +-⟨⟩ (l *S P) (m *S P) k ⟩
        (l *S P + m *S P) ₖ        ∎
      where open Reasoning R.setoid

    *S-compat : ∀ l m P → (l R.* m) *S P ≈ l *S (m *S P)
    *S-compat l m P = mk≈ λ k → let _ₖ = _⟨ k ⟩ in begin
        ((l R.* m) *S P) ₖ  ≈⟨ *S-⟨⟩ (l R.* m) P k ⟩
        (l R.* m) R.* P ₖ   ≈⟨ R.*-assoc l m (P ₖ) ⟩
        l R.* (m R.* P ₖ)   ≈⟨ R.sym (R.*-congˡ (*S-⟨⟩ m P k)) ⟩
        l R.* (m *S P) ₖ    ≈⟨ R.sym (*S-⟨⟩ l (m *S P) k) ⟩
        (l *S (m *S P)) ₖ   ∎
      where open Reasoning R.setoid

    -- properties of _*_

    private
      *-step-cong : ∀ {P Q R S} → P ≈ Q → R ≈ S → *-step P R ≈ *-step Q S
      *-step-cong {P} {Q} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q =
        ∷-≈ p≈q (+-cong P≈Q R≈S)

      *-step-zero : ∀ {P Q} → P ≈ 0# → Q ≈ 0# → *-step P Q ≈ 0#
      *-step-zero P≈0 Q≈0 = trans (*-step-cong P≈0 Q≈0) zero≈0

    *-cong : ∀ {P Q R S} → P ≈ Q → R ≈ S → P * R ≈ Q * S
    *-cong {[]}    {[]}    {R} {S} P≈Q R≈S = refl
    *-cong {[]}    {q ∷ Q} {R} {S} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← *-cong P≈Q R≈S = sym (*-step-zero (trans (*S-cong (R.sym p≈q) refl) (*S-zeroˡ S)) (sym ih))
    *-cong {p ∷ P} {[]}    {R} {S} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← *-cong P≈Q R≈S = *-step-zero (trans (*S-cong p≈q refl) (*S-zeroˡ R)) ih
    *-cong {p ∷ P} {q ∷ Q} {R} {S} P≈Q R≈S with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← *-cong P≈Q R≈S = *-step-cong (*S-cong p≈q R≈S) ih

    -- properties of _∣_

    private
        -0≈0 : R.- R.0# R.≈ R.0#
        -0≈0 = R.trans (R.sym (R.+-identityˡ _)) (R.-‿inverseʳ R.0#)

        x-0≈x : ∀ x → x R.- R.0# R.≈ x
        x-0≈x x = R.trans (R.+-congˡ -0≈0) (R.+-identityʳ x)

        x+y0≈x : ∀ x y → x R.+ y R.* R.0# R.≈ x
        x+y0≈x x y = R.trans (R.+-congˡ (R.zeroʳ y)) (R.+-identityʳ x)

        x+0y≈x : ∀ x y → x R.+ R.0# R.* y R.≈ x
        x+0y≈x x y = R.trans (R.+-congˡ (R.zeroˡ y)) (R.+-identityʳ x)

    scalar-∣ : ∀ x k → (scalar k ∣ x) R.≈ k
    scalar-∣ x k = x+y0≈x k x

    root-∣ : ∀ r x → (root r ∣ x) R.≈ x R.- r
    root-∣ r x = begin
        (R.- r) R.+ x R.* (R.1# R.+ x R.* R.0#)  ≈⟨ R.+-comm _ _ ⟩
        x R.* (R.1# R.+ x R.* R.0#) R.- r        ≈⟨ R.+-congʳ (R.*-congˡ (x+y0≈x R.1# x)) ⟩
        x R.* R.1# R.- r                         ≈⟨ R.+-congʳ (R.*-identityʳ x) ⟩
        x R.- r                                  ∎
      where open Reasoning R.setoid

    identity-∣ : ∀ x → (identity ∣ x) R.≈ x
    identity-∣ x = R.trans (root-∣ R.0# x) (x-0≈x x)

    private
        evalStep-cong : ∀ {x y} → x R.≈ y
                      → ∀ {k l a b} → k R.≈ l → a R.≈ b
                      → evalStep x k a R.≈ evalStep y l b
        evalStep-cong x≈y k≈l a≈b = R.+-cong k≈l (R.*-cong x≈y a≈b)

        evalStep-zeroʳ : ∀ {x k a} → a R.≈ R.0# → evalStep x k a R.≈ k
        evalStep-zeroʳ {x} {k} {a} a≈0 = R.trans (R.+-congˡ lemma) (R.+-identityʳ k)
          where
            lemma = R.trans (R.*-congˡ a≈0) (R.zeroʳ x)

        evalStep-+ : ∀ x pk qk pa qa →
            evalStep x (pk R.+ qk) (pa R.+ qa) R.≈
            evalStep x pk pa R.+ evalStep x qk qa
        evalStep-+ x pk qk pa qa = begin
            (pk R.+ qk) R.+ x R.* (pa R.+ qa)        ≈⟨ R.+-congˡ (R.distribˡ x pa qa) ⟩
            (pk R.+ qk) R.+ (x R.* pa R.+ x R.* qa)  ≈⟨ transpose-sum pk qk _ _ ⟩
            (pk R.+ x R.* pa) R.+ (qk R.+ x R.* qa)  ∎
          where
            open Reasoning R.setoid
            _∙_ = R._+_ -- FIXME: move this out to a lemma file
            transpose-sum : ∀ a b c d → _
            transpose-sum a b c d = begin
                (a ∙ b) ∙ (c ∙ d)  ≈⟨ R.+-assoc a b (c ∙ d) ⟩
                a ∙ (b ∙ (c ∙ d))  ≈⟨ R.+-congˡ (R.sym (R.+-assoc b c d)) ⟩
                a ∙ ((b ∙ c) ∙ d)  ≈⟨ R.+-congˡ (R.+-congʳ (R.+-comm b c)) ⟩
                a ∙ ((c ∙ b) ∙ d)  ≈⟨ R.+-congˡ (R.+-assoc c b d) ⟩
                a ∙ (c ∙ (b ∙ d))  ≈⟨ R.sym (R.+-assoc a c (b ∙ d)) ⟩
                (a ∙ c) ∙ (b ∙ d)  ∎

        evalStep-*S : ∀ k x l a → k R.* (evalStep x l a) R.≈ evalStep x (k R.* l) (k R.* a)
        evalStep-*S k x l a = R.trans (R.distribˡ k l _) (R.+-congˡ lemma)
          where
            open Reasoning R.setoid
            lemma = begin -- FIXME: move this out to a lemma file
                k R.* (x R.* a)  ≈⟨ R.sym (R.*-assoc k x a) ⟩
                (k R.* x) R.* a  ≈⟨ R.*-congʳ (R.*-comm k x) ⟩
                (x R.* k) R.* a  ≈⟨ R.*-assoc x k a ⟩
                x R.* (k R.* a)  ∎

    ∣-zeroʳ : ∀ P → P ∣ R.0# R.≈ P ⟨ 0 ⟩
    ∣-zeroʳ []      = R.refl
    ∣-zeroʳ (x ∷ P) = R.trans (R.+-congˡ (R.zeroˡ _)) (R.+-identityʳ _)

    ∣-cong : ∀ {P Q x y} → P ≈ Q → x R.≈ y → P ∣ x R.≈ Q ∣ y
    ∣-cong {[]}    {[]}    P≈Q x≈y = head-≈ P≈Q
    ∣-cong {p ∷ P} {[]}    P≈Q x≈y with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← ∣-cong P≈Q x≈y = R.trans (evalStep-zeroʳ ih) p≈q
    ∣-cong {[]}    {q ∷ Q} P≈Q x≈y with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← ∣-cong P≈Q x≈y = R.trans p≈q (R.sym (evalStep-zeroʳ (R.sym ih)))
    ∣-cong {p ∷ P} {q ∷ Q} P≈Q x≈y with p≈q , P≈Q ← uncons-≈ P≈Q with ih ← ∣-cong P≈Q x≈y = evalStep-cong x≈y p≈q ih

    *S-∣ : ∀ k P x → k R.* (P ∣ x) R.≈ (k *S P) ∣ x
    *S-∣ k []      x = R.zeroʳ k
    *S-∣ k (p ∷ P) x = R.trans
      (evalStep-*S k x p (P ∣ x))
      (evalStep-cong R.refl R.refl (*S-∣ k P x))

    +-∣ : ∀ P Q x → P ∣ x R.+ Q ∣ x R.≈ (P + Q) ∣ x
    +-∣ []      []      x = R.+-identityˡ R.0#
    +-∣ (p ∷ P) []      x rewrite List.map-id P = R.+-identityʳ _
    +-∣ []      (q ∷ Q) x rewrite List.map-id Q = R.+-identityˡ _
    +-∣ (p ∷ P) (q ∷ Q) x = R.trans
      (R.sym (evalStep-+ x p q (P ∣ x) (Q ∣ x)))
      (evalStep-cong R.refl R.refl (+-∣ P Q x))

    -- basic degree proof manipulation

    degree<length : ∀ P → IsBelowDegree (length P) P
    degree<length [] {k = ℕ.zero}  _ = R.refl
    degree<length [] {k = ℕ.suc k} _ = R.refl
    degree<length (x ∷ l) (ℕ.s≤s k≥l) = degree<length l k≥l

    degree-inj : ∀ {P n m}
               → IsBelowDegree n P
               → n ℕ.≤ m
               → IsBelowDegree m P
    degree-inj degn n≤m m≤k = degn (ℕ.≤-trans n≤m m≤k)

    degree<⊓ : ∀ {P m n}
             → IsBelowDegree m P
             → IsBelowDegree n P
             → IsBelowDegree (m ℕ.⊓ n) P
    degree<⊓ {P} {m} {n} mdeg ndeg with ℕ.≤-total m n
    ... | inj₁ m≤n rewrite ℕ.m≤n⇒m⊓n≡m m≤n = mdeg
    ... | inj₂ n≤m rewrite ℕ.m≥n⇒m⊓n≡n n≤m = ndeg

    -- operations preserve degree in some way

    ≈-degree : ∀ {P Q n}
             → IsBelowDegree n P
             → P ≈ Q
             → IsBelowDegree n Q
    ≈-degree deg P≈Q {k} n≤k = R.trans (R.sym (≈⟨⟩ P≈Q k)) (deg n≤k)

    *S-degree : ∀ {k P n}
              → IsBelowDegree n P
              → IsBelowDegree n (k *S P)
    *S-degree {l} {P} deg {k} n≤k = begin
        (l *S P)ₖ   ≈⟨ *S-⟨⟩ l P k ⟩
        l R.* P ₖ   ≈⟨ R.*-congˡ (deg n≤k) ⟩
        l R.* R.0#  ≈⟨ R.zeroʳ l ⟩
        R.0#        ∎
      where
        open Reasoning R.setoid
        _ₖ = _⟨ k ⟩

    -- -- -- +-degree : ∀ {P Q n m}
    -- -- --          → IsBelowDegree n P
    -- -- --          → IsBelowDegree m Q
    -- -- --          → IsBelowDegree (n ℕ.⊓ m) (P + Q)
    -- -- -- +-degree Pdeg Qdeg k = {!   !}

    -- -- -- *-degree : ∀ {P Q n m}
    -- -- --          → FitsDegree n P
    -- -- --          → FitsDegree m Q
    -- -- --          → FitsDegree (n ℕ.+ m) (P * Q)
    -- -- -- *-degree Pdeg Qdeg k = {!   !}