------------------------------------------------------------------------
-- The Agda standard library
--
-- An implementation of the ring solver that requires you to manually
-- pass the equation you wish to solve.
------------------------------------------------------------------------

-- You'll probably want to use `Tactic.RingSolver` instead which uses
-- reflection to automatically extract the equation.

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

open import Tactic.RingSolver.Core.AlmostCommutativeRing

module Tactic.RingSolver.NonReflective
  {ℓ₁ ℓ₂} (ring : AlmostCommutativeRing ℓ₁ ℓ₂)
  (let open AlmostCommutativeRing ring)
  where

open import Algebra.Morphism
open import Function.Base using (id; _⟨_⟩_)
open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
open import Data.Maybe.Base
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base using (_×_; proj₁; proj₂; _,_)
open import Data.Vec.Base using (Vec)
open import Data.Vec.N-ary

open import Tactic.RingSolver.Core.Polynomial.Parameters
open import Tactic.RingSolver.Core.Expression public
open import Algebra.Properties.Semiring.Exp.TCOptimised semiring

module Ops where
  zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x
  zero-homo x _ with just p ← 0≟ x = p

  homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂
  homo = record
    { from = record
      { rawRing = AlmostCommutativeRing.rawRing ring
      ; isZero  = λ x → is-just (0≟ x)
      }
    ; to = record
      { isAlmostCommutativeRing = record
          { isCommutativeSemiring = isCommutativeSemiring
          ; -‿cong       = -‿cong
          ; -‿*-distribˡ = -‿*-distribˡ
          ; -‿+-comm     = -‿+-comm
          }
      }
    ; morphism      = -raw-almostCommutative⟶ ring
    ; Zero-C⟶Zero-R = zero-homo
    }
  open Eval rawRing id public

  open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)

  norm : ∀ {n} → Expr Carrier n → Poly n
  norm (Κ x)   = κ x
  norm (Ι x)   = ι x
  norm (x ⊕ y) = norm x ⊞ norm y
  norm (x ⊗ y) = norm x ⊠ norm y
  norm (⊝ x)   = ⊟ norm x
  norm (x ⊛ i) = norm x ⊡ i

  ⟦_⇓⟧ : ∀ {n} → Expr Carrier n → Vec Carrier n → Carrier
  $\begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2188}{\htmlId{2188}{\htmlClass{Bound}{\text{expr}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2128}{\htmlId{2193}{\htmlClass{Function Operator}{\text{⇓⟧}}}}\, \,\htmlId{2196}{\htmlClass{Symbol}{\text{=}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#1924}{\htmlId{2200}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2188}{\htmlId{2205}{\htmlClass{Bound}{\text{expr}}}}\, \end{pmatrix} \,\htmlId{2213}{\htmlClass{Keyword}{\text{where}}}\,

    \,\htmlId{2224}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{2229}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Semantics.html}{\htmlId{2236}{\htmlClass{Module}{\text{Tactic.RingSolver.Core.Polynomial.Semantics}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#1308}{\htmlId{2280}{\htmlClass{Function}{\text{homo}}}}\,
      \,\htmlId{2291}{\htmlClass{Keyword}{\text{renaming}}}\, (\begin{pmatrix} \,\htmlId{2305}{\htmlClass{Symbol}{\text{to}}}\, \begin{pmatrix})

  \,\href{Tactic.RingSolver.NonReflective.html#2317}{\htmlId{2317}{\htmlClass{Function}{\text{correct}}}}\, \,\htmlId{2325}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2327}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{2329}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2330}{\htmlId{2330}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{2331}{\htmlClass{Symbol}{\text{}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2334}{\htmlId{2334}{\htmlClass{Bound}{\text{expr}}}}\, \,\htmlId{2339}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{2341}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{2346}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2330}{\htmlId{2354}{\htmlClass{Bound}{\text{n}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2357}{\htmlId{2357}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2359}{\htmlClass{Symbol}{\text{→}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2334}{\htmlId{2363}{\htmlClass{Bound}{\text{expr}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2128}{\htmlId{2368}{\htmlClass{Function Operator}{\text{⇓⟧}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2357}{\htmlId{2371}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{2373}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2334}{\htmlId{2377}{\htmlClass{Bound}{\text{expr}}}}\, \end{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2357}{\htmlId{2384}{\htmlClass{Bound}{\text{ρ}}}}\,
  \,\href{Tactic.RingSolver.NonReflective.html#2317}{\htmlId{2388}{\htmlClass{Function}{\text{correct}}}}\, \,\htmlId{2396}{\htmlClass{Symbol}{\text{{}}}\,\,\htmlId{2397}{\htmlClass{Argument}{\text{n}}}\, \,\htmlId{2399}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2401}{\htmlId{2401}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{2402}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{2404}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2406}{\htmlClass{Function}{\text{go}}}}\,
    \,\htmlId{2413}{\htmlClass{Keyword}{\text{where}}}\,
    \,\htmlId{2423}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{2428}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.html}{\htmlId{2435}{\htmlClass{Module}{\text{Tactic.RingSolver.Core.Polynomial.Homomorphism}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#1308}{\htmlId{2482}{\htmlClass{Function}{\text{homo}}}}\,

    \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2492}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2495}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2497}{\htmlClass{Symbol}{\text{∀}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2500}{\htmlId{2500}{\htmlClass{Bound}{\text{expr}}}}\, \,\htmlId{2505}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{2507}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{2512}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2401}{\htmlId{2520}{\htmlClass{Bound}{\text{n}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2523}{\htmlId{2523}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2525}{\htmlClass{Symbol}{\text{→}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2500}{\htmlId{2529}{\htmlClass{Bound}{\text{expr}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2128}{\htmlId{2534}{\htmlClass{Function Operator}{\text{⇓⟧}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2523}{\htmlId{2537}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{2539}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2500}{\htmlId{2543}{\htmlClass{Bound}{\text{expr}}}}\, \end{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2523}{\htmlId{2550}{\htmlClass{Bound}{\text{ρ}}}}\,
    \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2556}{\htmlClass{Function}{\text{go}}}}\, (\,\href{Tactic.RingSolver.Core.Expression.html#558}{\htmlId{2560}{\htmlClass{InductiveConstructor}{\text{Κ}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2562}{\htmlId{2562}{\htmlClass{Bound}{\text{x}}}}\,)   \,\href{Tactic.RingSolver.NonReflective.html#2567}{\htmlId{2567}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2569}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants.html#663}{\htmlId{2571}{\htmlClass{Function}{\text{κ-hom}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2562}{\htmlId{2577}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2567}{\htmlId{2579}{\htmlClass{Bound}{\text{ρ}}}}\,
    \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2585}{\htmlClass{Function}{\text{go}}}}\, (\,\href{Tactic.RingSolver.Core.Expression.html#609}{\htmlId{2589}{\htmlClass{InductiveConstructor}{\text{Ι}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2591}{\htmlId{2591}{\htmlClass{Bound}{\text{x}}}}\,)   \,\href{Tactic.RingSolver.NonReflective.html#2596}{\htmlId{2596}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2598}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables.html#953}{\htmlId{2600}{\htmlClass{Function}{\text{ι-hom}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2591}{\htmlId{2606}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2596}{\htmlId{2608}{\htmlClass{Bound}{\text{ρ}}}}\,
    \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2614}{\htmlClass{Function}{\text{go}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2618}{\htmlId{2618}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#660}{\htmlId{2620}{\htmlClass{InductiveConstructor Operator}{\text{⊕}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2622}{\htmlId{2622}{\htmlClass{Bound}{\text{y}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2625}{\htmlId{2625}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2627}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition.html#1285}{\htmlId{2629}{\htmlClass{Function}{\text{⊞-hom}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#1924}{\htmlId{2636}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2618}{\htmlId{2641}{\htmlClass{Bound}{\text{x}}}}\,) (\,\href{Tactic.RingSolver.NonReflective.html#1924}{\htmlId{2645}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2622}{\htmlId{2650}{\htmlClass{Bound}{\text{y}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2625}{\htmlId{2653}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2655}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1648}{\htmlId{2657}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2663}{\htmlClass{Function Operator}{\text{⟩}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2666}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2618}{\htmlId{2669}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2625}{\htmlId{2671}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2673}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Algebra.Structures.html#13637}{\htmlId{2675}{\htmlClass{Function}{\text{+-cong}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2682}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2684}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2622}{\htmlId{2687}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2625}{\htmlId{2689}{\htmlClass{Bound}{\text{ρ}}}}\,)
    \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2696}{\htmlClass{Function}{\text{go}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2700}{\htmlId{2700}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#711}{\htmlId{2702}{\htmlClass{InductiveConstructor Operator}{\text{⊗}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2704}{\htmlId{2704}{\htmlClass{Bound}{\text{y}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2707}{\htmlId{2707}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2709}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication.html#9614}{\htmlId{2711}{\htmlClass{Function}{\text{⊠-hom}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#1924}{\htmlId{2718}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2700}{\htmlId{2723}{\htmlClass{Bound}{\text{x}}}}\,) (\,\href{Tactic.RingSolver.NonReflective.html#1924}{\htmlId{2727}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2704}{\htmlId{2732}{\htmlClass{Bound}{\text{y}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2707}{\htmlId{2735}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2737}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1648}{\htmlId{2739}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2745}{\htmlClass{Function Operator}{\text{⟩}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2748}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2700}{\htmlId{2751}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2707}{\htmlId{2753}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2755}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Algebra.Structures.html#13202}{\htmlId{2757}{\htmlClass{Function}{\text{*-cong}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2764}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2766}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2704}{\htmlId{2769}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2707}{\htmlId{2771}{\htmlClass{Bound}{\text{ρ}}}}\,)
    \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2778}{\htmlClass{Function}{\text{go}}}}\, (\,\href{Tactic.RingSolver.Core.Expression.html#825}{\htmlId{2782}{\htmlClass{InductiveConstructor Operator}{\text{⊝}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2784}{\htmlId{2784}{\htmlClass{Bound}{\text{x}}}}\,)   \,\href{Tactic.RingSolver.NonReflective.html#2789}{\htmlId{2789}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2791}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation.html#1764}{\htmlId{2793}{\htmlClass{Function}{\text{⊟-hom}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#1924}{\htmlId{2800}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2784}{\htmlId{2805}{\htmlClass{Bound}{\text{x}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2789}{\htmlId{2808}{\htmlClass{Bound}{\text{ρ}}}}\,   \,\href{Function.Base.html#4322}{\htmlId{2812}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1648}{\htmlId{2814}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2820}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#995}{\htmlId{2822}{\htmlClass{Function}{\text{-‿cong}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2830}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2784}{\htmlId{2833}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2789}{\htmlId{2835}{\htmlClass{Bound}{\text{ρ}}}}\,)
    \,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2842}{\htmlClass{Function}{\text{go}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2846}{\htmlId{2846}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#768}{\htmlId{2848}{\htmlClass{InductiveConstructor Operator}{\text{⊛}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2850}{\htmlId{2850}{\htmlClass{Bound}{\text{i}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2853}{\htmlId{2853}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2855}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation.html#3304}{\htmlId{2857}{\htmlClass{Function}{\text{⊡-hom}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#1924}{\htmlId{2864}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2846}{\htmlId{2869}{\htmlClass{Bound}{\text{x}}}}\,) \,\href{Tactic.RingSolver.NonReflective.html#2850}{\htmlId{2872}{\htmlClass{Bound}{\text{i}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2853}{\htmlId{2874}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2876}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1648}{\htmlId{2878}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4322}{\htmlId{2884}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Algebra.Properties.Semiring.Exp.TCOptimised.html#1170}{\htmlId{2886}{\htmlClass{Function}{\text{^-congˡ}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2850}{\htmlId{2894}{\htmlClass{Bound}{\text{i}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2492}{\htmlId{2897}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2846}{\htmlId{2900}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2853}{\htmlId{2902}{\htmlClass{Bound}{\text{ρ}}}}\,)

  \,\htmlId{2908}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{2913}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Relation.Binary.Reflection.html}{\htmlId{2920}{\htmlClass{Module}{\text{Relation.Binary.Reflection}}}}\, \,\href{Algebra.Structures.html#1873}{\htmlId{2947}{\htmlClass{Function}{\text{setoid}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#609}{\htmlId{2954}{\htmlClass{InductiveConstructor}{\text{Ι}}}}\, \begin{pmatrix} \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2317}{\htmlId{2965}{\htmlClass{Function}{\text{correct}}}}\, \,\htmlId{2973}{\htmlClass{Keyword}{\text{public}}}\,

\,\href{Tactic.RingSolver.NonReflective.html#2981}{\htmlId{2981}{\htmlClass{Function}{\text{solve}}}}\, \,\htmlId{2987}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2989}{\htmlClass{Symbol}{\text{∀}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{2992}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{2994}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Builtin.Nat.html#203}{\htmlId{2996}{\htmlClass{Datatype}{\text{ℕ}}}}\,) \,\htmlId{2999}{\htmlClass{Symbol}{\text{→}}}\,
        (\,\href{Tactic.RingSolver.NonReflective.html#3010}{\htmlId{3010}{\htmlClass{Bound}{\text{f}}}}\, \,\htmlId{3012}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Data.Vec.N-ary.html#1168}{\htmlId{3014}{\htmlClass{Function}{\text{N-ary}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3020}{\htmlClass{Bound}{\text{n}}}}\, (\,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3023}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3028}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3036}{\htmlClass{Bound}{\text{n}}}}\,) (\,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3040}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3045}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3053}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{3055}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3057}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3062}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3070}{\htmlClass{Bound}{\text{n}}}}\,) \,\htmlId{3074}{\htmlClass{Symbol}{\text{→}}}\,
        \,\href{Data.Vec.N-ary.html#2526}{\htmlId{3084}{\htmlClass{Function}{\text{Eqʰ}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3088}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{3090}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3095}{\htmlClass{Function}{\text{curryⁿ}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2128}{\htmlId{3103}{\htmlClass{Function Operator}{\text{Ops.⟦\_⇓⟧}}}}\, (\,\href{Data.Product.Base.html#636}{\htmlId{3113}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3120}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3130}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3010}{\htmlId{3132}{\htmlClass{Bound}{\text{f}}}}\,) (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3139}{\htmlClass{Function}{\text{curryⁿ}}}}\, (\,\href{Tactic.RingSolver.NonReflective.html#2128}{\htmlId{3147}{\htmlClass{Function Operator}{\text{Ops.⟦\_⇓⟧}}}}\, (\,\href{Data.Product.Base.html#650}{\htmlId{3157}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3164}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3174}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3010}{\htmlId{3176}{\htmlClass{Bound}{\text{f}}}}\,) \,\htmlId{3182}{\htmlClass{Symbol}{\text{→}}}\,
        \,\href{Data.Vec.N-ary.html#2282}{\htmlId{3192}{\htmlClass{Function}{\text{Eq}}}}\,  \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3196}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{3198}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3203}{\htmlClass{Function}{\text{curryⁿ}}}}\, (\,\href{Tactic.RingSolver.Core.Expression.html#1073}{\htmlId{3211}{\htmlClass{Function Operator}{\text{Ops.⟦\_⟧}}}}\,  (\,\href{Data.Product.Base.html#636}{\htmlId{3221}{\htmlClass{Field}{\text{proj₁}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3228}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3238}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3010}{\htmlId{3240}{\htmlClass{Bound}{\text{f}}}}\,) (\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3247}{\htmlClass{Function}{\text{curryⁿ}}}}\, (\,\href{Tactic.RingSolver.Core.Expression.html#1073}{\htmlId{3255}{\htmlClass{Function Operator}{\text{Ops.⟦\_⟧}}}}\,  (\,\href{Data.Product.Base.html#650}{\htmlId{3265}{\htmlClass{Field}{\text{proj₂}}}}\, (\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3272}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2992}{\htmlId{3282}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3010}{\htmlId{3284}{\htmlClass{Bound}{\text{f}}}}\,)
\,\href{Tactic.RingSolver.NonReflective.html#2981}{\htmlId{3290}{\htmlClass{Function}{\text{solve}}}}\, \,\htmlId{3296}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Binary.Reflection.html#2522}{\htmlId{3298}{\htmlClass{Function}{\text{Ops.solve}}}}\,
\,\htmlId{3308}{\htmlClass{Symbol}{\text{{-#}}}\, \,\htmlId{3312}{\htmlClass{Keyword}{\text{INLINE}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2981}{\htmlId{3319}{\htmlClass{Function}{\text{solve}}}}\, \,\htmlId{3325}{\htmlClass{Symbol}{\text{#-}}}}\,

\,\htmlId{3330}{\htmlClass{Keyword}{\text{infixl}}}\, \,\htmlId{3337}{\htmlClass{Number}{\text{6}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3343}{\htmlId{3339}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#3343}{\htmlId{3343}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3347}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{3349}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{3351}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Tactic.RingSolver.NonReflective.html#3352}{\htmlId{3352}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3354}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Builtin.Nat.html#203}{\htmlId{3356}{\htmlClass{Datatype}{\text{ℕ}}}}\,\,\htmlId{3357}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{3359}{\htmlClass{Symbol}{\text{→}}}\,
      \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3367}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3372}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3352}{\htmlId{3380}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3382}{\htmlClass{Symbol}{\text{→}}}\,
      \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3390}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3395}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3352}{\htmlId{3403}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3405}{\htmlClass{Symbol}{\text{→}}}\,
      \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3413}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3418}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3352}{\htmlId{3426}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{3428}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3430}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3435}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3352}{\htmlId{3443}{\htmlClass{Bound}{\text{n}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#3343}{\htmlId{3445}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3449}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Sigma.html#235}{\htmlId{3451}{\htmlClass{InductiveConstructor Operator}{\text{\_,\_}}}}\,
\,\htmlId{3455}{\htmlClass{Symbol}{\text{{-#}}}\, \,\htmlId{3459}{\htmlClass{Keyword}{\text{INLINE}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3343}{\htmlId{3466}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3470}{\htmlClass{Symbol}{\text{#-}}}}\,