Solving generic rings

[aljce]

open import Level using (_⊔_)
open import Algebra using (CommutativeRing)

open import Data.Maybe using (nothing)
open import Data.List using (List)
open List

module Prelude.Modular {c ℓ} (R : CommutativeRing c ℓ) where

open CommutativeRing R using (_≈_; setoid; 0#; 1#; _+_; _*_; _-_)
  renaming (Carrier to C)

open import Polynomial.Simple.AlmostCommutativeRing using (AlmostCommutativeRing; fromCommutativeRing)
open import Polynomial.Simple.Reflection using (solveOver)

ACR : AlmostCommutativeRing c ℓ
ACR = fromCommutativeRing R λ _ → nothing

record _≈_[mod_] (x : C) (y : C) (n : C) : Set (c ⊔ ℓ) where
  constructor modulo
  field
    k : C
    x-y≈k*n : x - y ≈ k * n

refl : ∀ {x} {n} → x ≈ x [mod n ]
refl {x} {n} = modulo 0# (solveOver (x ∷ n ∷ []) ACR)

Errors with

CommutativeRing._*_ /= CommutativeRing._+_
when checking that the expression
Polynomial.Simple.Solver.Ops.correct {_} {_} ACR {_}
(Polynomial.Expr.Expr._⊗_ {_}
 {AlmostCommutativeRing.Carrier {_} {_} ACR} {2}
 (Polynomial.Expr.Expr.Κ {_}
  {AlmostCommutativeRing.Carrier {_} {_} ACR} {2}
  (CommutativeRing.0# {_} {_} R))
 (Polynomial.Expr.Expr.Ι {_}
  {AlmostCommutativeRing.Carrier {_} {_} ACR} {2}
  (Data.Fin.Base.Fin.zero {_})))
(Data.Vec.Base.Vec._∷_ {_} {_} {_} n
 (Data.Vec.Base.Vec._∷_ {_} {_} {_} x
  (Data.Vec.Base.Vec.[] {_} {_})))
has type
(ACR AlmostCommutativeRing.≈
 Polynomial.Simple.Solver.Ops.⟦ ACR ⇓⟧
 (Polynomial.Expr.Expr.Κ (x - x))
 (n Data.Vec.Base.Vec.∷ x Data.Vec.Base.Vec.∷ Data.Vec.Base.Vec.[]))

Is it possible to solve rings that aren't currently instantiated

[aljce]

Actually this usually isn't helpful because you often have equalities as arguments to your proof. Like in:

sym : ∀ {x y} {n} → x ≈ y [mod n ] → y ≈ x [mod n ]

[aljce]

Actually I do have uses for this.

[aljce]

Here are some oddities. The solver can solve:

lemma : ∀ a b c d → a * b + c * (a * d) ≈ a * (b + c * d)
lemma = solve ACR

but not

lemma : ∀ a b c d e → a * b + c * (a * e + b * d + (c * (d * e))) ≈ (a + c * d) * (b + c * e)
lemma = solve ACR

[oisdk]

The solver needs the coefficients to compute to work properly. i.e. 1 + 2 should compute to 3, otherwise the solver won’t be able to solve the identity.

That doesn’t mean you can’t work with generic rings, though (although it will need some extra work). The solver is designed so that it can have a different type for the coefficients as for the target ring. You could use this in combination with a free ring (that is homomorphic to a generic ring) as the coefficient. You would need to update the reflection code as well to work with this.

The reason your second example can’t be solved is that it requires computation on the indices, while the first does not. I’m not sure of the specifics exactly, but it looks like the second is probably looking for a 1 + 1 = 2 somewhere.

Hope that helps!