Relax decidability module parameter of Algebra.Solver.Ring

[mwageringel]

(See #507)

This replaces the Decidable module parameter in Algebra.Solver.Ring
by a new predicate WeaklyDecidable. It only provides a subset of those
equality proofs that Decidable can provide, and does not provide
inequality proofs.

As a result, ring solvers can now be used in more general situations in
which decidable equality is not available. For this, a new module
Algebra.Solver.Ring.NaturalCoefficients.Default was added which
instantiates the natural coefficients solver for any
CommutativeSemiring, such as ×-⊎-commutativeSemiring in
Function.Related.TypeIsomorphisms.Solver.

---

Any comments are appreciated. Is naming and location of the two new modules Algebra.Solver.Ring.WeaklyDecidable and Algebra.Solver.Ring.NaturalCoefficients.Default appropriate or are there better options?

[mwageringel]

I incorporated the suggestions. As mentioned, I had to move Data.Bool.Base_≟_ to Data.Bool.Properties to avoid import cycles, which is not fully backward compatible, but should not cause many issues either.

[MatthewDaggitt]

Thanks for the PR. Merging in!

[MatthewDaggitt]

Hmm hang on, I just took one last look and have a question. Isn't every relation WeaklyDecidable? I take it that if you just pass the ring solver the constant nothing function, then it won't be able to prove very much?

[mwageringel]

Indeed, being WeaklyDecidable does not have much meaning by itself, as its usefulness depends on the implementation. In that sense, it seems like a useless predicate. I am not aware of a way to specify that the implementation, i.e. the equality proofs it can provide, is as sharp as it can be, other than requiring full decidability.

However (quite to my surprise), even with the constant nothing function, the NaturalCoefficients solver is still able to prove a number of equalities. For example, commutativity, associativity, distributivity and binomial expansions all work, but when the polynomials get more complicated, it can fail. The precise requirements for it to work or fail are not obvious to me. An important example that fails is 0# * x ≈ 0#, as the normal forms on both sides are different. With the constant nothing function, they apparently cannot be proved to be equal, but with a stronger implementation of WeaklyDecidable they can.

By the way, an operator _:×_ is needed to represent the multiplication _×_ between ℕ and ring elements, so I added it as well. For example, it is necessary for this:

test : ∀ x y → (x + y) ^ 3 ≈ x ^ 3 + 3 × x ^ 2 * y + 3 × x * y ^ 2 + y ^ 3
test = solve 2 (λ x y → (x :+ y) :^ 3 := x :^ 3 :+ 3 :× x :^ 2 :* y :+ 3 :× x :* y :^ 2 :+ y :^ 3) refl

[MatthewDaggitt]

Thanks for the clarification and the PR! Merging in. I'll add some documentation afterwards.