Decidability requirement for ring solvers is too strong

[mwageringel]

The current ring solver implementation requires the induced coefficient equality to be decidable. As a result, it seems difficult or impossible to use the ring solver for arbitrary rings without decidable equality (please correct me if I am wrong). For example, to prove properties that follow from the ring properties, in a similar fashion to the other solvers, this is the best I could come up with.

open import Algebra
open import Data.Nat using (_≟_)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Relation.Nullary using (Dec; yes; no; ¬_)

module _ {r₁ r₂} (R : CommutativeSemiring r₁ r₂) where

  open CommutativeSemiring R
  open import Algebra.Operations.Semiring semiring

  -- This should not be needed.
  module _ (char0 : ∀ {m n} → ¬ m ≡ n → ¬ m × 1# ≈ n × 1#) where

    dec : ∀ m n → Dec (m × 1# ≈ n × 1#)
    dec m n with m ≟ n
    ... | yes ≡.refl = yes refl
    ... | no ¬p = no (char0 ¬p)

    open import Algebra.Solver.Ring.NaturalCoefficients R dec

    distributivity : ∀ x y z → x * (y + z) ≈ x * y + x * z
    distributivity = solve 3 (λ x y z → x :* (y :+ z) := x :* y :+ x :* z) refl

This still requires some sort of proof that the ring is of characteristic 0 which is not usually available, but also should not be necessary for proving distributivity. Indeed, the inequality proofs coming from decidable equality are not actually used in the ring solver. After all, the solvers are only used for proving equalities, not inequalities.

My suggestion is to replace the Dec _≈_ by Maybe _≈_ in all ring solvers. That way, the solver can be instantiated with the best equality proofs available, but they are allowed to be a proper subset of those equality proofs that would be provided by Dec. In the example above, the char0 requirement can be dropped. For more specific instances of rings which have decidable coefficient equality, you can simply project Dec to Maybe and retain all the capabilities of the solver.

I tested this change on the library and everything still seems to work fine. This simplifies using the ring solvers. For example in Function.Related.TypeIsomorphisms.Solver, all the hard work was proving the inequalities, which is not needed after the proposed change, so the implementation of that solver becomes very short.

I would be happy to provide a pull request if you think this is a useful addition. Let me know if there are any problems I did not think of.

[MatthewDaggitt]

So if I understand the above correctly, you're saying we can relax the decidability module parameter in Algebra.Solver.Ring? If it is strictly weaker then that sounds great! Feel free to submit a PR and we'll take it look?

[mwageringel]

Yes, that is exactly what I meant. I will put together a PR in the next few days.

[MatthewDaggitt]

Closed with 5827d71