WIP Add Rational RingSolver

[lemastero]

Changes

• add Data.Rational.Tactic.RingSolver
• example or Rational.RingSolver
• add Data.Rational.Unnormalised.Tactic.RingSolver
• example or Rational.Unnormalised.RingSolver
• update CHANGELOG

Fix #1879

[MatthewDaggitt]

Thanks, looks great! As you say if you could add some examples in README.Data.Rational(.Unnormalised) that would be awesome.

[jamesmckinna]

I'd be strongly tempted to lift this out as a definition in Data.Rational.Base, or else as a property (cf. Relation.Binary.WeaklyDecidable, for which we currently lack analogues at arity 0, 1) in Data.Rational.Properties.

Suggested name for such a refactored f: isZero-weakly-decidable?

That way, the imports for your solver modules then become very much simplified, in favour of those that are already currently used by the Rational.* modules...

... and there's (potentially) a downstream benefit in being able to reuse the definition of the corresponding Unnormalised function in the definition of this one.

[dancewithheart]

I have revived this work in #2965 and following this remark - the helper weak zero decidable were
moved into the corresponding Properties.

[jamesmckinna]

Ditto.!

[jamesmckinna]

Re: refactoring suggestion

I think that it's possible that a 'better' approach is available via leveraging the construction in the (old) Algebra.RingSolver.Simple module: namely to turn a Decidable equality into a WeaklyDecidable one, and thereby define a 'smart' constructor for AlmostCommutativeRings.

Now, equality on Rational(.Unnormalised) is already proven Decidable (in *.Properties), so there might (even) be no need to define a separate f/isZero-weakly-decidable function at all.

[jamesmckinna]

Re: refactoring (meta-comment)

I think there's a tension, especially as a new developer, between contributing a PR with as 'small' footprint as possible (which can have as a consequence a 'wide' collection of imports, and (lots of) local definitions), and refactoring it to distribute the various pieces over the library (as I suggested above). But I do think the latter is eventually the way to go, for the sake of leveraging the power already present in the library.

For the PR at hand: The definitions of the Solvers for Nat and Integer might be instructive in this regard, where the import interfaces/implementations are just about as minimal as you can get...

[lemastero]

if you could add some examples in README.Data.Rational(.Unnormalised) that would be awesome.

There is clearly something wrong with RingSolvers in this PR. I defined very simple example here:

open import Data.Integer using (+_)
open import Data.Rational
open import Data.Rational.Properties

1/4 : ℚ
1/4 = + 1 / 4

3/4 : ℚ
3/4 = + 3 / 4

open import Relation.Binary.PropositionalEquality -- using (_≡_; refl)
open import Data.Rational.Tactic.RingSolver

lemma : ∀ x y → x + y + 1/4 + ½ ≃ 3/4 + y + x
lemma = {! solve-∀  !}

but this fails with:

Malformed call to solve.Expected target type to be like: ∀ x y → x + y ≈ y + x.Instead: _19
when checking that the expression unquote solve-∀ has type _19

I think RingSolver does not like PropositionalEquality (but it does not like equality define in Rational.Properties either).

I will try to see if I can create example with existing SemiringSolver for begin with and do refactoring proposed, by @jamesmckinna.

[jamesmckinna]

Ok, so this is clearly very troubling behaviour!
I'm not in fact myself any kind of expert on the various Solver implementations, so a shout-out to... hmm not sure...

@oisdk do you have any insight here to offer?

[gallais]

Given that the goal looks like a meta variable, it may be that the tactic is being
run too early. You may want to block on the meta so that you can wait for it to
be solved and then call the tactic once again.

Cf. the blockOnMeta call in this chunk of tactical I developed for #2033
and where I was facing similar issues.

[lemastero]

I've found some resources on semigroup/ring solvers in Agda:

• Automatic Ring Solving
• The solver for equations in commutative rings in agda/cubical - Felix Cherubini (video)
• Automatically and Effiently Illustrating Polynomial Equalities in Agda - Donnacha Oisín Kidney
• Evidence-providing problem solvers in Agda - Uma Zalakain

I will try to traverse the subject and fold it into better understanding - what is the problem here.