Algebra.Ring.Solver

{-
Adaptation of the ring solver from the Agda standard library to work
with the 1Lab's weird primitives.
Agda's ring solver was originally implemented by Nils Anders Danielsson,
and the referenced version includes contributions by Matthew Daggit,
Guillaume Allais, Donnacha Oisín Kidney, and Markus Wageringel.
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).
-}
open import 1Lab.Reflection.Variables
open import 1Lab.Reflection.Solver
open import 1Lab.Reflection
open import 1Lab.Rewrite

open import Algebra.Ring.Cat.Initial
open import Algebra.Ring.Commutative
open import Algebra.Group.Ab
open import Algebra.Prelude
open import Algebra.Group
open import Algebra.Ring

open import Data.Fin.Base
open import Data.Int.HIT
open import Data.List hiding (lookup)
open import Data.Dec
open import Data.Nat

module Algebra.Ring.Solver where

module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
  private
    module R = CRing-on cring
    ℤ↪R-rh = Int-is-initial (el _ R.has-is-set , R.has-ring-on) .centre
    module ℤ↪R = is-ring-hom (ℤ↪R-rh .preserves)
    embed-coe = ℤ↪R-rh .hom

  data Poly   : Nat → Type ℓ
  data Normal : Nat → Type ℓ

  data Poly where
    ∅     : ∀ {n} → Poly n
    _*x+_ : ∀ {n} → Poly (suc n) → Normal n → Poly (suc n)

  data Normal where
    con  : Int → Normal 0
    poly : ∀ {n} → Poly (suc n) → Normal (suc n)

  Ep : ∀ {n} → Poly (suc n) → Vec R (suc n) → R
  En : ∀ {n} → Normal n → Vec R n → R

  Ep ∅ i = R.0r
  Ep (p *x+ c) (x ∷ e) = Ep p (x ∷ e) R.* x R.+ En c e

  En (con x) i = embed-coe (lift x)
  En (poly x) i = Ep x i

  0h : ∀ {n} → Poly n
  0n : ∀ {n} → Normal n
  0h = ∅
  0n {zero} = con 0
  0n {suc n} = poly 0h

  1h : ∀ {n} → Poly (suc n)
  1n : ∀ {n} → Normal n

  1h {n} = ∅ *x+ 1n {n}
  1n {zero} = con 1
  1n {suc n} = poly 1h

  -- The more cases that we can approximate here, the more powerful the
  -- solver becomes.
  _==ₕ_ : ∀ {n} (x y : Poly n) → Maybe (x ≡ y)
  _==ₙ_ : ∀ {n} (x y : Normal n) → Maybe (x ≡ y)

  ∅ ==ₕ ∅ = just refl
  ∅ ==ₕ (_ *x+ _) = nothing
  (_ *x+ _) ==ₕ ∅ = nothing
  (p *x+ x) ==ₕ (q *x+ y) with p ==ₕ q | x ==ₙ y
  ... | just p=q | just x=y = just $ ap₂ _*x+_ p=q x=y
  ... | just _   | nothing = nothing
  ... | nothing  | just _  = nothing
  ... | nothing  | nothing = nothing

  con c ==ₙ con d with c ≡? d
  ... | yes c=d = just (ap con c=d)
  ... | no ¬c=d = nothing
  poly x ==ₙ poly y with x ==ₕ y
  ... | just x=y = just $ ap poly x=y
  ... | nothing  = nothing

  _*x+ₙ_ : ∀ {n} → Poly (suc n) → Normal n → Poly (suc n)
  (p *x+ c') *x+ₙ c = (p *x+ c') *x+ c
  ∅          *x+ₙ c with c ==ₙ 0n
  ... | just c≈0 = ∅
  ... | nothing  = ∅ *x+ c

  _+ₚ_ : ∀ {n} → Poly (suc n) → Poly (suc n) → Poly (suc n)
  _+ₙ_ : ∀ {n} → Normal n → Normal n → Normal n

  ∅         +ₚ y         = y
  y         +ₚ ∅         = y
  (p *x+ x) +ₚ (q *x+ y) = (p +ₚ q) *x+ₙ (x +ₙ y)

  con x  +ₙ con y = con (x +ℤ y)
  poly x +ₙ poly y = poly (x +ₚ y)

  _*x+ₚ_ : ∀ {n} → Poly (suc n) → Poly (suc n) → Poly (suc n)
  p *x+ₚ (q *x+ d) = (p +ₚ q) *x+ₙ d
  ∅ *x+ₚ ∅         = ∅
  (p *x+ c) *x+ₚ ∅ = (p *x+ c) *x+ 0n

  _*ₙₚ_ : ∀ {n} → Normal n → Poly (suc n) → Poly (suc n)
  _*ₚₙ_ : ∀ {n} → Poly (suc n) → Normal n → Poly (suc n)
  _*ₚ_  : ∀ {n} → Poly (suc n) → Poly (suc n) → Poly (suc n)
  _*ₙ_  : ∀ {n} → Normal n → Normal n → Normal n

  infix 30 _*ₙₚ_ _*ₚₙ_ _*ₚ_ _*ₙ_

  c *ₙₚ ∅ = ∅
  c *ₙₚ (p *x+ d) with c ==ₙ 0n
  ... | just _  = ∅
  ... | nothing = (c *ₙₚ p) *x+ (c *ₙ d)

  ∅ *ₚₙ y = ∅
  (p *x+ c) *ₚₙ d with d ==ₙ 0n
  ... | just _  = ∅
  ... | nothing = (p *ₚₙ d) *x+ (c *ₙ d)

  con x  *ₙ con y  = con (x *ℤ y)
  poly x *ₙ poly y = poly (x *ₚ y)

  ∅ *ₚ _ = ∅
  (p *x+ c) *ₚ ∅ = ∅
  (p *x+ c) *ₚ (q *x+ d) = ((p *ₚ q) *x+ₚ (p *ₚₙ d +ₚ c *ₙₚ q)) *x+ₙ (c *ₙ d)

  -ₙ_ : ∀ {n} → Normal n → Normal n
  -ₚ_ : ∀ {n} → Poly (suc n) → Poly (suc n)

  -ₙ con x = con (negate x)
  -ₙ poly x = poly (-ₚ x)

  -ₚ x = (-ₙ 1n) *ₙₚ x

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

  data Polynomial (m : Nat) : Type ℓ where
    op   : (o : Op) (p q : Polynomial m) → Polynomial m
    con  : (c : Int) → Polynomial m
    var  : (x : Fin m) → Polynomial m
    :-_  : (p : Polynomial m) → Polynomial m

  -- Short-hand notation.

  infix 40 _:-_
  infix 30 _:*_

  _:+_ : ∀ {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} → Nat → Polynomial n → Polynomial n
  zero :× p = con 0
  suc m :× p = p :+ (m :× p)

  sem : Op → R → R → R
  sem [+] = R._+_
  sem [*] = R._*_

  ⟦_⟧ : ∀ {n} → Polynomial n → Vec R n → R
  ⟦ op o p₁ p₂ ⟧ ρ = sem o (⟦ p₁ ⟧ ρ) (⟦ p₂ ⟧ ρ)
  ⟦ con c      ⟧ ρ = embed-coe (lift c)
  ⟦ var x      ⟧ ρ = lookup ρ x
  ⟦ :- p       ⟧ ρ = R.- ⟦ p ⟧ ρ

  ---

  normal-coe : ∀ {n} → Int → Normal n
  normal-coe {zero} x  = con x
  normal-coe {suc n} x = poly (∅ *x+ₙ normal-coe x)

  normal-var : ∀ {n} → Fin n → Normal n
  normal-var fzero    = poly ((∅ *x+ 1n) *x+ 0n)
  normal-var (fsuc f) = poly (∅ *x+ₙ normal-var f)

  normal : ∀ {n} → Polynomial n → Normal n
  normal (op [+] x y) = normal x +ₙ normal y
  normal (op [*] x y) = normal x *ₙ normal y
  normal (con c) = normal-coe c
  normal (var x) = normal-var x
  normal (:- x) = -ₙ (normal x)

  ⟦_⟧ₙ : ∀ {n} → Polynomial n → Vec R n → R
  ⟦ x ⟧ₙ ρ = En (normal x) ρ

  0n-hom : ∀ {n} (ρ : Vec R n) → En 0n ρ ≡ R.0r
  0n-hom [] = ℤ↪R.pres-0
  0n-hom (x ∷ ρ) = refl

  1n-hom : ∀ {n} (ρ : Vec R n) → En 1n ρ ≡ R.1r
  1n-hom [] = ℤ↪R.pres-id
  1n-hom (x ∷ ρ) =
    (R.0r R.* x) R.+ (En 1n ρ) ≡⟨ R.eliml R.*-zerol ⟩
    En 1n ρ                    ≡⟨ 1n-hom ρ ⟩
    R.1r                       ∎

  *x+ₙ-sound
    : ∀ {n} (p : Poly (suc n)) (c : Normal n) ρ
    → Ep (p *x+ₙ c) ρ ≡ Ep (p *x+ c) ρ
  *x+ₙ-sound ∅ c (e ∷ ρ) with c ==ₙ 0n
  ... | just x = sym $
    Ep (∅ *x+ ⌜ c ⌝) (e ∷ ρ)   ≡⟨ ap! x ⟩
    Ep (∅ *x+ 0n) (e ∷ ρ)      ≡⟨⟩
    (R.0r R.* e) R.+ En 0n ρ ≡⟨ R.eliml R.*-zerol ⟩
    En 0n ρ                  ≡⟨ 0n-hom ρ ⟩
    R.0r                               ∎
  ... | nothing = refl
  *x+ₙ-sound (p *x+ x) c ρ = refl

  ∅*x+ₙ-hom
    : ∀ {n} (c : Normal n) x ρ
    → Ep (∅ *x+ₙ c) (x ∷ ρ) ≡ En c ρ
  ∅*x+ₙ-hom c x ρ with c ==ₙ 0n
  ... | just x = sym (ap (λ c → En c ρ) x ∙ 0n-hom ρ)
  ... | nothing = R.eliml R.*-zerol

  +ₚ-hom
    : ∀ {n} (p q : Poly (suc n)) ρ
    → Ep (p +ₚ q) ρ ≡ Ep p ρ R.+ Ep q ρ
  +ₙ-hom
    : ∀ {n} (p q : Normal n) ρ
    → En (p +ₙ q) ρ ≡ En p ρ R.+ En q ρ

  +ₚ-hom ∅ q ρ = sym R.+-idl
  +ₚ-hom (p *x+ x) ∅ ρ = sym R.+-idr
  +ₚ-hom (p *x+ c) (q *x+ d) (x ∷ ρ) =
    Ep ((p +ₚ q) *x+ₙ (c +ₙ d)) (x ∷ ρ)                                 ≡⟨ *x+ₙ-sound (p +ₚ q) (c +ₙ d) (x ∷ ρ) ⟩
    Ep ((p +ₚ q) *x+ (c +ₙ d)) (x ∷ ρ)                                  ≡⟨⟩
    ⌜ Ep (p +ₚ q) (x ∷ ρ) ⌝ R.* x R.+ En (c +ₙ d) ρ                     ≡⟨ ap! (+ₚ-hom p q (x ∷ ρ)) ⟩
    (Ep p (x ∷ ρ) R.+ Ep q (x ∷ ρ)) R.* x R.+ ⌜ En (c +ₙ d) ρ ⌝         ≡⟨ ap! (+ₙ-hom c d ρ) ⟩
    ⌜ (Ep p (x ∷ ρ) R.+ Ep q (x ∷ ρ)) R.* x ⌝ R.+ (En c ρ R.+ En d ρ)   ≡⟨ ap! R.*-distribr  ⟩
    Ep p (x ∷ ρ) R.* x R.+ Ep q (x ∷ ρ) R.* x R.+ (En c ρ R.+ En d ρ)   ≡⟨ R.a.pullr (R.pulll R.+-commutes) ⟩
    Ep p (x ∷ ρ) R.* x R.+ (En c ρ R.+ Ep q (x ∷ ρ) R.* x R.+ En d ρ)   ≡⟨ R.a.extendl (R.a.pulll refl) ⟩
    Ep p (x ∷ ρ) R.* x R.+ En c ρ R.+ (Ep q (x ∷ ρ) R.* x R.+ En d ρ)   ∎
  +ₙ-hom (con x)  (con y)  ρ = ℤ↪R.pres-+ (lift x) (lift y)
  +ₙ-hom (poly p) (poly q) ρ = +ₚ-hom p q ρ

  *x+-hom
    : ∀ {n} (p q : Poly (suc n)) x ρ
    → Ep (p *x+ₚ q) (x ∷ ρ)
    ≡ Ep p (x ∷ ρ) R.* x R.+ Ep q (x ∷ ρ)
  *x+-hom ∅ ∅ x ρ = R.introl R.*-zerol
  *x+-hom (p *x+ c) ∅ x ρ = ap₂ R._+_ refl (0n-hom ρ)
  *x+-hom p (q *x+ d) x ρ =
    Ep (p *x+ₚ (q *x+ d)) (x ∷ ρ)                          ≡⟨⟩
    Ep ((p +ₚ q) *x+ₙ d) (x ∷ ρ)                           ≡⟨ *x+ₙ-sound (p +ₚ q) d (x ∷ ρ) ⟩
    ⌜ Ep (p +ₚ q) (x ∷ ρ) ⌝ R.* x R.+ En d ρ               ≡⟨ ap! (+ₚ-hom p q (x ∷ ρ)) ⟩
    ⌜ (Ep p (x ∷ ρ) R.+ Ep q (x ∷ ρ)) R.* x ⌝ R.+ En d ρ   ≡⟨ ap! R.*-distribr ⟩
    Ep p (x ∷ ρ) R.* x R.+ Ep q (x ∷ ρ) R.* x R.+ En d ρ   ≡⟨ R.pullr refl ⟩
    Ep p (x ∷ ρ) R.* x R.+ (Ep q (x ∷ ρ) R.* x R.+ En d ρ) ∎

  *ₙₚ-hom
    : ∀ {n} (c : Normal n) (p : Poly (suc n)) x ρ
    → Ep (c *ₙₚ p) (x ∷ ρ) ≡ En c ρ R.* Ep p (x ∷ ρ)
  *ₚₙ-hom
    : ∀ {n} (c : Normal n) (p : Poly (suc n)) x ρ
    → Ep (p *ₚₙ c) (x ∷ ρ) ≡ Ep p (x ∷ ρ) R.* En c ρ
  *ₙ-hom : ∀ {n} (c d : Normal n) ρ → En (c *ₙ d) ρ ≡ En c ρ R.* En d ρ
  *ₚ-hom : ∀ {n} (p q : Poly (suc n)) ρ → Ep (p *ₚ q) ρ ≡ Ep p ρ R.* Ep q ρ

  *ₚ-hom ∅ q ρ = sym R.*-zerol
  *ₚ-hom (p *x+ c) ∅ ρ = sym R.*-zeror
  *ₚ-hom (p *x+ c) (q *x+ d) (x ∷ ρ) =
      *x+ₙ-sound ((p *ₚ q) *x+ₚ ((p *ₚₙ d) +ₚ (c *ₙₚ q))) _ (x ∷ ρ)
    ∙ ap₂ R._+_ (ap₂ R._*_ (*x+-hom (p *ₚ q) ((p *ₚₙ d) +ₚ (c *ₙₚ q)) x ρ) refl) refl
    ∙ ap₂ R._+_ (ap₂ R._*_ (ap₂ R._+_ (ap (R._* x) (*ₚ-hom p q (x ∷ ρ)))
        (+ₚ-hom (p *ₚₙ d) (c *ₙₚ q) (x ∷ ρ))) refl
        ∙ ap₂ R._*_ (ap₂ R._+_ refl (ap₂ R._+_ (*ₚₙ-hom d p x ρ) (*ₙₚ-hom c q x ρ)))
        refl) refl
    ∙ ap₂ R._+_ refl (*ₙ-hom c d ρ) ∙ lemma _ _ _ _ _
    where
    lemma
      : ∀ p q x d c
      → (p R.* q R.* x R.+ ((p R.* d) R.+ (c R.* q))) R.* x R.+ (c R.* d)
      ≡ (p R.* x R.+ c) R.* (q R.* x R.+ d)
    lemma a c x d b =
      (a R.* c R.* x R.+ (a R.* d R.+ b R.* c)) R.* x R.+ b R.* d                 ≡⟨ ap₂ R._+_ R.*-distribr refl ⟩
      (a R.* c R.* x R.* x R.+ (a R.* d R.+ b R.* c) R.* x) R.+ b R.* d           ≡⟨ sym R.+-associative ⟩
      a R.* c R.* x R.* x R.+ ((a R.* d R.+ b R.* c) R.* x R.+ b R.* d)           ≡⟨ ap₂ R._+_ lem₁ (ap₂ R._+_ lem₂ refl) ⟩
      a R.* x R.* (c R.* x) R.+ (a R.* x R.* d R.+ b R.* (c R.* x) R.+ b R.* d)   ≡⟨ ap₂ R._+_ refl (sym R.+-associative) ⟩
      a R.* x R.* (c R.* x) R.+ (a R.* x R.* d R.+ (b R.* (c R.* x) R.+ b R.* d)) ≡⟨ R.+-associative ⟩
      a R.* x R.* (c R.* x) R.+ a R.* x R.* d R.+ (b R.* (c R.* x) R.+ b R.* d)   ≡˘⟨ ap₂ R._+_ R.*-distribl R.*-distribl ⟩
      a R.* x R.* (c R.* x R.+ d) R.+ b R.* (c R.* x R.+ d)                       ≡˘⟨ R.*-distribr ⟩
      (a R.* x R.+ b) R.* (c R.* x R.+ d)                                         ∎
      where
      lem₁' =
        a R.* c R.* x     ≡˘⟨ R.*-associative ⟩
        a R.* ⌜ c R.* x ⌝ ≡⟨ ap! R.*-commutes ⟩
        a R.* (x R.* c)   ≡⟨ R.*-associative ⟩
        a R.* x R.* c     ∎

      lem₁ =
        a R.* c R.* x R.* x    ≡⟨ ap₂ R._*_ lem₁' refl ⟩
        a R.* x R.* c R.* x    ≡˘⟨ R.*-associative ⟩
        a R.* x R.* (c R.* x)  ∎

      lem₂ =
        (a R.* d R.+ b R.* c) R.* x           ≡⟨ R.*-distribr ⟩
        a R.* d R.* x R.+ b R.* c R.* x       ≡˘⟨ ap₂ R._+_ R.*-associative R.*-associative ⟩
        a R.* ⌜ d R.* x ⌝ R.+ b R.* (c R.* x) ≡⟨ ap! R.*-commutes ⟩
        a R.* (x R.* d) R.+ b R.* (c R.* x)   ≡⟨ ap₂ R._+_ R.*-associative refl ⟩
        a R.* x R.* d R.+ b R.* (c R.* x)     ∎

  *ₙ-hom (con x) (con y) ρ = ℤ↪R.pres-* (lift x) (lift y)
  *ₙ-hom (poly p) (poly q) ρ = *ₚ-hom p q ρ

  *ₙₚ-hom c ∅ x ρ = sym R.*-zeror
  *ₙₚ-hom c (p *x+ d) x ρ with c ==ₙ 0n
  ... | just c=0 = sym (ap₂ R._*_ (ap (λ e → En e ρ) c=0 ∙ 0n-hom ρ) refl ∙ R.*-zerol)
  ... | nothing =
      ap₂ R._+_ (ap (R._* x) (*ₙₚ-hom c p x ρ) ∙ sym R.*-associative) (*ₙ-hom c d ρ)
    ∙ sym R.*-distribl

  *ₚₙ-hom c ∅ x ρ = sym R.*-zerol
  *ₚₙ-hom c (p *x+ d) x ρ with c ==ₙ 0n
  ... | just c=0 = sym (ap₂ R._*_ refl (ap (λ e → En e ρ) c=0 ∙ 0n-hom ρ) ∙ R.*-zeror)
  ... | nothing  =
      ap₂ R._+_ (ap (R._* x) (*ₚₙ-hom c p x ρ) ·· sym R.*-associative ·· ap₂ R._*_ refl R.*-commutes ∙ R.*-associative)
        (*ₙ-hom d c ρ)
    ∙ sym R.*-distribr

  -ₚ-hom : ∀ {n} (p : Poly (suc n)) ρ → Ep (-ₚ p) ρ ≡ R.- Ep p ρ
  -ₙ-hom : ∀ {n} (n : Normal n) ρ → En (-ₙ n) ρ ≡ R.- En n ρ

  -ₚ-hom p (x ∷ ρ) =
      *ₙₚ-hom (-ₙ 1n) p x ρ
    ∙ ap₂ R._*_ (-ₙ-hom 1n ρ ∙ ap R.-_ (1n-hom ρ)) refl
    ∙ sym R.neg-*-l ∙ ap R.-_ R.*-idl
  -ₙ-hom (con x) ρ = ℤ↪R.pres-neg {x = lift x}
  -ₙ-hom (poly x) ρ = -ₚ-hom x ρ

  sound-coe
    : ∀ {n} (c : Int) (ρ : Vec R n) → En (normal-coe c) ρ ≡ embed-coe (lift c)
  sound-coe c [] = refl
  sound-coe c (x ∷ ρ) = ∅*x+ₙ-hom (normal-coe c) x ρ ∙ sound-coe c ρ

  sound-var : ∀ {n} (j : Fin n) ρ → En (normal-var j) ρ ≡ lookup ρ j
  sound-var fzero (x ∷ ρ) =
    Ep (∅ *x+ 1n) (x ∷ ρ) R.* x R.+ En 0n ρ ≡⟨ R.elimr (0n-hom ρ) ⟩
    ⌜ Ep (∅ *x+ 1n) (x ∷ ρ) ⌝ R.* x         ≡⟨ ap! (R.eliml R.*-zerol ∙ 1n-hom ρ) ⟩
    R.1r R.* x                              ≡⟨ R.*-idl ⟩
    x                                       ∎
  sound-var (fsuc j) (x ∷ ρ) = ∅*x+ₙ-hom (normal-var j) x ρ ∙ sound-var j ρ

  sound : ∀ {n} (p : Polynomial n) ρ → En (normal p) ρ ≡ ⟦ p ⟧ ρ
  sound (op [+] p q) ρ = +ₙ-hom (normal p) (normal q) ρ ∙ ap₂ R._+_ (sound p ρ) (sound q ρ)
  sound (op [*] p q) ρ = *ₙ-hom (normal p) (normal q) ρ ∙ ap₂ R._*_ (sound p ρ) (sound q ρ)
  sound (con c) ρ = sound-coe c ρ
  sound (var x) ρ = sound-var x ρ
  sound (:- p) ρ = -ₙ-hom (normal p) ρ ∙ ap R.-_ (sound p ρ)

  expand : ∀ {n} → Polynomial n → Vec R n → R
  expand e ρ = ⟦ e ⟧ ρ

  solve
    : ∀ {n} (p q : Polynomial n) (r : Vec R n)
    → En (normal p) r ≡ En (normal q) r → ⟦ p ⟧ r ≡ ⟦ q ⟧ r
  solve p q r prf = sym (sound p r) ·· prf ·· sound q r

  private
    test-distrib : ∀ x y z → x R.* (y R.+ z) ≡ y R.* x R.+ z R.* x
    test-distrib x y z =
      solve (var 0 :* (var 1 :+ var 2)) ((var 1 :* var 0) :+ (var 2 :* var 0)) (x ∷ y ∷ z ∷ []) refl

    test-identities : ∀ x → x R.+ (R.0r R.* R.1r) ≡ (R.1r R.+ R.0r) R.* x
    test-identities x =
      solve (var 0 :+ (con 0 :* con 1)) ((con 1 :+ con 0) :* var 0) (x ∷ []) refl

module Reflection where
  private
    pattern ring-args cring args = (_ hm∷ _ hm∷ cring v∷ args)
    pattern is-ring-args is-ring args = (_ hm∷ _ hm∷ _ hm∷ _ hm∷ _ hm∷ is-ring v∷ args)
    pattern is-group-args is-group args = (_ hm∷ _ hm∷ _ hm∷ is-group v∷ args)
    pattern ring-field field-name cring args =
      def field-name (ring-args (def (quote CRing-on.has-ring-on) (ring-args cring [])) args)
    pattern group-field field-name cring args =
      def field-name
        (is-group-args
          (def (quote is-ring.+-group)
            (is-ring-args (ring-field (quote Ring-on.has-is-ring) cring []) []))
          args)

    mk-cring-args : Term → List (Arg Term) → List (Arg Term)
    mk-cring-args cring args = unknown h∷ unknown h∷ cring v∷ args

    pattern “1” cring = ring-field (quote Ring-on.1r) cring []
    pattern “*” cring x y = ring-field (quote Ring-on._*_) cring (x v∷ y v∷ [])
    pattern “+” cring x y = ring-field (quote Ring-on._+_) cring (x v∷ y v∷ [])
    pattern “0” cring = group-field (quote is-abelian-group.1g) cring []
    pattern “-” cring x = group-field (quote is-abelian-group.inverse) cring (x v∷ [])

  “expand” : Term → Term → Term → Term
  “expand” cring p env = def (quote Impl.expand) (mk-cring-args cring (unknown h∷ p v∷ env v∷ []))

  “solve” : Term → Term → Term → Term → Term
  “solve” cring lhs rhs env =
    def (quote Impl.solve) (mk-cring-args cring (unknown h∷ lhs v∷ rhs v∷ env v∷ “refl” v∷ []))

  build-expr : ∀ {ℓ} {A : Type ℓ} → Term → Variables A → Term → TC (Term × Variables A)
  build-expr cring vs (“0” cring') = do
    unify cring cring'
    z ← quoteTC (diff 0 0)
    pure $ con (quote Impl.Polynomial.con) (z v∷ []) , vs
  build-expr cring vs (“1” cring') = do
    unify cring cring'
    o ← quoteTC (diff 1 0)
    pure $ con (quote Impl.Polynomial.con) (o v∷ []) , vs
  build-expr cring vs (“*” cring' t1 t2) = do
    unify cring cring'
    e1 , vs ← build-expr cring vs t1
    e2 , vs ← build-expr cring vs t2
    pure $ def (quote Impl._:*_) (mk-cring-args cring $ e1 v∷ e2 v∷ []) , vs
  build-expr cring vs (“+” cring' t1 t2) = do
    unify cring cring'
    e1 , vs ← build-expr cring vs t1
    e2 , vs ← build-expr cring vs t2
    pure $ def (quote Impl._:+_) (mk-cring-args cring $ e1 v∷ e2 v∷ []) , vs
  build-expr cring vs (“-” cring' tm) = do
    unify cring cring'
    e , vs ← build-expr cring vs tm
    pure $ con (quote Impl.Polynomial.:-_) (e v∷ []) , vs
  build-expr cring vs tm = do
    (v , vs) ← bind-var vs tm
    pure $ con (quote Impl.Polynomial.var) (v v∷ []) , vs

  dont-reduce : List Name
  dont-reduce =
    quote Number.fromNat ∷
    quote is-abelian-group.1g ∷
    quote Ring-on.1r ∷
    quote is-abelian-group.inverse ∷
    quote Ring-on._*_ ∷
    quote Ring-on._+_ ∷
    []

  cring-solver : ∀ {ℓ} {A : Type ℓ} → CRing-on A → TC (VariableSolver A)
  cring-solver {A = A} cring = do
    cring-tm ← quoteTC cring
    pure $ var-solver dont-reduce (build-expr cring-tm) (“solve” cring-tm) (“expand” cring-tm)

  repr-macro : ∀ {ℓ} {A : Type ℓ} → CRing-on A → Term → Term → TC ⊤
  repr-macro cring tm hole = do
    solver ← cring-solver cring
    mk-var-repr solver tm

  expand-macro : ∀ {ℓ} {A : Type ℓ} → CRing-on A → Term → Term → TC ⊤
  expand-macro cring tm hole = do
    solver ← cring-solver cring
    mk-var-normalise solver tm hole

  solve-macro : ∀ {ℓ} {A : Type ℓ} → CRing-on A → Term → TC ⊤
  solve-macro cring hole = do
    solver ← cring-solver cring
    mk-var-solver solver hole

macro
  cring-repr! : ∀ {ℓ} → CRing ℓ → Term → Term → TC ⊤
  cring-repr! cring tm = Reflection.repr-macro (cring .snd) tm

  cring-simpl! : ∀ {ℓ} → CRing ℓ → Term → Term → TC ⊤
  cring-simpl! cring tm = Reflection.expand-macro (cring .snd) tm

  cring-on! : ∀ {ℓ} {A : Type ℓ} → CRing-on A → Term → TC ⊤
  cring-on! cring = Reflection.solve-macro cring

  cring! : ∀ {ℓ} → CRing ℓ → Term → TC ⊤
  cring! cring = Reflection.solve-macro (cring .snd)

private module TestCRing {ℓ} (R : CRing ℓ) where
  module R = CRing-on (R .snd)

  test-distrib : ∀ x y z → x R.* (y R.+ z) ≡ (y R.* x) R.+ (z R.* x)
  test-distrib x y z = cring! R

  test-identities : ∀ x → x R.+ (R.0r R.* R.1r) ≡ (R.1r R.+ R.0r) R.* x
  test-identities x = cring! R