Algebra.Solver.Ring allows us to specify a coefficient ring, but not here

[onestruggler]

This line fixed the coefficient ring to be the target ring:

agda-stdlib/src/Tactic/RingSolver/NonReflective.agda

Line 37 in b0505d6

homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂

It seems that it should be in some file like "Algebra.Solver.Ring.Simple".

Probably due to this, it seems that I cannot use "Tactic.RingSolver" on abstract rings since I cannot provide an "AlmostCommutativeRing" (from an abstract ring), which requires a field "0≟_ : (x : Carrier) → Maybe (0# ≈ x)". I cannot do pattern matching on "#0", or in general on elements of an abstract ring.

The paper "Proving Equalities in a Commutative Ring Done Right in Coq" says their mothod works for abstract rings in paper's abstract. Algebra.Solver.Ring seems to work for abstract rings, but I haven't checked this yet.

[onestruggler]

Algebra.Solver.Ring works for abstract rings, and I just checked this.

  test : ∀ x y z -> (x ∧ y) ∧ (z ∧ z) ≈ x ∧ (y ∧ z) ∧ z
  test = solve 3 (\ x y z ->  (x :* y) :* (z :* z) := x :* ((y :* z) :* z)) refl

Here x y z belong to an abstract BooleanAlgebra, which is also a ⊕-∧-commutativeRing. I use Bool for the coefficent ring. The ring solver solves this well. One annoying thing is the infixity problem of ∧ and :*, one of which is infixl and the other is infixr. As you can see, I have to put explicit parenthese in the second line. I will raise another issue for this problem.

If needed, here is the full code (you need change the top level module name accordingly):

module CS4.FinIndexed.BooleanAlgebraSolver
  {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
  where
  
  open BooleanAlgebra B
  open import Algebra.Lattice.Properties.BooleanAlgebra B
  open import Relation.Binary.Reasoning.Setoid setoid
  open DefaultXorRing  
  open import Algebra.Bundles using (CommutativeRing)
  open CommutativeRing ⊕-∧-commutativeRing using ()

  open import Data.Bool using (Bool ; true ; false)
    renaming (_∧_ to _∧'_ ; _∨_ to _∨'_ ; _xor_ to _⊕'_)
  open import Data.Bool.Properties using (xor-∧-commutativeRing)

  import Algebra.Solver.Ring as RS
  open import Algebra.Solver.Ring.AlmostCommutativeRing
  open import Relation.Binary.Definitions using (WeaklyDecidable)

  open import Data.Maybe using (just ; nothing)
  open import Function using (id)
  import Algebra.Morphism.Definitions as MorphismDefinitions
  open MorphismDefinitions Bool Carrier _≈_

  -- We use prime to differentiate this name from the one in RS.
  ⟦_⟧' : Bool -> Carrier
  ⟦_⟧' false = ⊥
  ⟦_⟧' true = ⊤
  
  +-homo : Homomorphic₂ ⟦_⟧' _⊕'_ _⊕_
  +-homo false false = sym (⊕-identityʳ ⊥)
  +-homo false true = sym (⊕-identityˡ ⊤)
  +-homo true false = sym (⊕-identityʳ ⊤)
  +-homo true true = sym claim
    where
    claim : (⊤ ∨ ⊤) ∧ ¬ (⊤ ∧ ⊤) ≈ ⊥
    claim = begin
      (⊤ ∨ ⊤) ∧ ¬ (⊤ ∧ ⊤) ≈⟨ ∧-cong refl (¬-cong (∧-identityˡ ⊤)) ⟩
      (⊤ ∨ ⊤) ∧ ¬ ⊤ ≈⟨ ∧-cong refl ⊤≉⊥ ⟩
      (⊤ ∨ ⊤) ∧ ⊥ ≈⟨ ∧-zeroʳ (⊤ ∨ ⊤) ⟩
      ⊥ ∎ 

  *-homo : Homomorphic₂ ⟦_⟧' _∧'_ _∧_
  *-homo false false = sym (∧-zeroʳ ⊥)
  *-homo false true = sym (∧-zeroˡ ⊤)
  *-homo true false = sym (∧-zeroʳ ⊤)
  *-homo true true = sym (∧-identityˡ ⊤)

  -‿homo : Homomorphic₁ ⟦_⟧' id id
  -‿homo false = refl
  -‿homo true = refl

  0-homo : Homomorphic₀ ⟦_⟧' false ⊥
  0-homo = refl

  1-homo : Homomorphic₀ ⟦_⟧' true ⊤
  1-homo = refl

  R = fromCommutativeRing ⊕-∧-commutativeRing
  rawRingCoeff = CommutativeRing.rawRing xor-∧-commutativeRing

  morphism : rawRingCoeff -Raw-AlmostCommutative⟶ R
  morphism = record
           { ⟦_⟧ = ⟦_⟧'
           ; +-homo = +-homo
           ; *-homo = *-homo
           ; -‿homo = -‿homo
           ; 0-homo = 0-homo
           ; 1-homo = 1-homo
           }

  _coeff≟_ : WeaklyDecidable (Induced-equivalence morphism)
  false coeff≟ false = just refl
  false coeff≟ true = nothing
  true coeff≟ false = nothing
  true coeff≟ true = just refl

  open RS rawRingCoeff R morphism _coeff≟_ public

  test : ∀ x y z -> (x ∧ y) ∧ (z ∧ z) ≈ x ∧ (y ∧ z) ∧ z
  test = solve 3 (\ x y z ->  (x :* y) :* (z :* z) := x :* ((y :* z) :* z)) refl

[jamesmckinna]

My understanding of the Ring Solver architecture is that it is intended always to be sound, but becomes 'more complete' according to the discriminatory power of the user-supplied (weak) decision procedure 0≟_ for equality (in your example: coeff≟)...
... but I'm not clear what the consequences are of choosing const nothing in the case of a general abstract Ring?

More generally, I'm not sure I exactly understand either the title of this issue (where is 'here', for example?), or what point you are making in the first paragraph... I seem to be missing a lot of detail? Can you say a bit more about what the exact issue is here?

[MatthewDaggitt]

There's no one explicitly in charge of the ring solver code, so if you have a sensible change that would allow it to work for the abstract rings, we would definitely welcome a PR!

[onestruggler]

There's no one explicitly in charge of the ring solver code, so if you have a sensible change that would allow it to work for the abstract rings, we would definitely welcome a PR!

I will give it a try.