Tactic.RingSolver doesn't work over generic rings

[MatthewDaggitt]

Currently the reflective interface for Tactic.RingSolver only works over concrete instances of rings (see oisdk/agda-ring-solver#12). It would be useful to get this working for generic rings as well.

[felixwellen]

I think I solved the same issue for the RingSolver in the cubical library, which made the examples here work:

https://github.com/agda/cubical/blob/master/Cubical/Algebra/RingSolver/Examples.agda

I had to sacrifice the generality of AlmostRings for that, which lead to a separate solver for naturals. Under the hood, it is now a solver for algebras over the integers. And the examples rely on normalization of integers.
Is this still an issue? It might be not too much work to implement my approach together with an stdlib-expert...

[MatthewDaggitt]

Hey, thanks for the heads-up! Yes I've been vaguely following your PRs on it and meant to have a deep dive to grok what your changes were doing at some point. When I was hacking on the standard library one earlier this year, I couldn't quite understand @oisdk's comment in the thread linked above about why computation on the coefficients was relevant? Even when the underlying ring is some generic ring, I don't quite understand why the coefficient ring can't stay the same and be the natural numbers which still compute?

Any chance you could provide a brief high-level explanation of what your fix was?

[felixwellen]

Here is short recap of the problem (all rings commutative):

What (my version of) the ring solver essentially does is to use equality of multivariate polynomials (over the integers) to show that two expressions in a ring are equal. Equality of polynomials, even if they are multivariate, amounts to checking that all coefficients are equal. Also for the Horner forms used in the ring solver, that amounts to checking equality in the given ring.
Now a problem, that might be specific to how I or others implemented translation of ring expressions to Horner forms, is that you sometimes end up with a coefficients of some form like 1-1. This should be zero, but in an abstract ring, its normal form cannot be the same as that of 0.
Let me briefly say where these expressions come from. If you map ring expressions to Horner forms (which you could call a normalization), you need to encode things like 0, 1, -1, x... So in my way of doing it, I use the Horner form 1*X + 0 for x. If I then translate something like x*x, there already will be things like 0*0 appearing as coefficients in the Horner forms. At first I tried to just fix my algorithm for that (and maybe I just didn't think about it enough to be successful with that). But then I thought it is probably a lot easier to use agda to these kinds of things, by using some inductive definition of integers, where all those expressions normalize to the same thing in the end.

Now to the problems with naturals:
My first reflex was actually to generalize the solver for almost rings over almost rings, and have rings over integers as a default to deal with abstract rings. But I ran into problems with that, when I tried to proof the homomorphism properties of evaluation, i.e. that evaluating a ring expression yields the same ring element as evaluating the normal form of the expression.
Again, I didn't think too much about a general fix, so there might be solutions to that (I was only interested in abstract rings...). I think the problem was, that I really needed 'y-y' to be zero for some reason. So I just went from almost rings to rings.
Btw.: I am pretty sure, what I wrote is independent of the integers - plugging those in was just convenient and everything should work for other base rings.

[MatthewDaggitt]

Thank you for the detailed explanation! Hmm I have to confess I only know how the reflective interface for the solver works, not how the solver itself works. I suspect altering it to use our new normalising version of the integers would be a serious undertaking? Not to mention I'm kind of reluctant to add a new formalisation of the integers if at all possible...

Out of interest, was the cubical solver also ported from @oisdk's library or did it have a different origin?

[MatthewDaggitt]

Also another question, are your normalising integers complete? i.e. do you think your solution has totally fixed the problem for all equations over an arbitrary ring, or does it "just" allow a larger range of equations to go through? (I put "just" in inverted commas, as that itself was a large undertaking I'm sure!)

[felixwellen]

Same origin, I looked at @oisdk 's solver and the paper it is based on. I didn't read everything though.

[MatthewDaggitt]

Hmm maybe it wouldn't be such a big effort to port it over then...

[felixwellen]

I don't think it is too much effort, if we do it together - I don't know much about the stdlib. Maybe that's a project for the agda implementer meeting?
Also: The integers I'm using are the same as Data.Integer in the stdlib, so that shoudn't be a problem.
And: I have no idea if the solver is complete in any reasonable sense.

[MatthewDaggitt]

I don't think it is too much effort, if we do it together - I don't know much about the stdlib. Maybe that's a project for the agda implementer meeting?

That sounds like a plan, I've added it as a code sprint. Thanks for pushing this 😄

The integers I'm using are the same as Data.Integer in the stdlib, so that shoudn't be a problem.

Awesome 🎉

[felixwellen]

I'll start to look into that now.

[felixwellen]

There is a a problem I didn't think of yet. In the reflection code, in the function constructCallToSolver, the given ring is substituted into a lambda. As far as I can tell, this substitution should go wrong, if there are any variables involved in the given ring, since their deBrujin-indices are not corrected... This is something I didn't solve properly over at the cubical library - so I don't have a good solution. Does anyone? There has to be some way of substituting, without writing it yourself, right?