Tactic.RingSolver doesn't work over generic rings

[MatthewDaggitt]

Currently the reflective interface for Tactic.RingSolver only works over concrete instances of rings (see https://github.com/oisdk/agda-ring-solver/issues/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 :smile:

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

Awesome :tada:

[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?

[MatthewDaggitt]

Relevant piece of code:

https://github.com/agda/agda-stdlib/blob/53e45bb1b9d7d3c36c4bba222bf31a30dc6719d0/src/Tactic/RingSolver.agda#L263-L265

Hmm that's an excellent spot. Sorry my brain isn't quite awake yet, do we need full-blown substitution or just a selective lifting of the DB indices? I'm afraid I don't have any good suggestions though.

[felixwellen]

I think it is enough to just lift DB indices. I wrote something I am not proud of for the cubical library, which works in the cases I am interested in: https://github.com/agda/cubical/blob/master/Cubical/Algebra/CommRingSolver/Reflection.agda#L269-L277

[MatthewDaggitt]

Hmmm actually there might be something in here:

https://github.com/agda/agda-stdlib/blob/master/src/Reflection/AST/DeBruijn.agda

Maybe strengthen is what we're after?

[MatthewDaggitt]

If not then, feel free to add your hack to that file with a suitable label that says it's probably not fully functioning yet...

[felixwellen]

That might be just what we need... I'll look into it and start PRs accordingly if it works/comment here if it doesn't.

[felixwellen]

I discussed this with @andreasabel and we concluded that the weakening function in the code you mentioned should do what we need. It might take a bit of time, until I can turn that into a PR.

[felixwellen]

The situation is a bit more complicated than I thought: The code that constructs the call to the ring sovler is different than what I did in cubical library. Does someone know which arguments here

https://github.com/agda/agda-stdlib/blob/master/src/Tactic/RingSolver.agda#L296

actually end up under a lambda and need their deBruijn-indices lifted? I was thinking about just changing prendVLams, but that's nonsense, since the variables, lhs, rhs worked, so their deBruijn indices must be right in the end. Is there test-code anywhere or examples for the ring solver which I can use to test (and document new use cases once they work)? We have something in the cubical library here:

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

[MatthewDaggitt]

Does someone know which arguments here actually end up under a lambda and need their deBruijn-indices lifted?

Okay just had a medium-level dive into the code. So if I understand it correctly, the LHS and RHS expressions start off underneath a set of pi bindings. These are then stripped away here:

https://github.com/agda/agda-stdlib/blob/53e45bb1b9d7d3c36c4bba222bf31a30dc6719d0/src/Tactic/RingSolver.agda#L290

The LHS and RHS are then equated, and then the same number of lambda bindings as there were pi bindings are then prepended to the result. So if I'm understanding it correctly, no alteration of DB indices is required?

@felixwellen, obviously if you have a concrete example that fails then my reasoning is wrong :smile:

Is there test-code anywhere or examples for the ring solver which I can use to test (and document new use cases once they work)? We have something in the cubical library here:

https://github.com/agda/agda-stdlib/blob/master/README/Tactic/RingSolver.agda

[felixwellen]

Yes, that is what I understand as well. The problem I suspected, is with the variable 'ring'. It should be outside the pi when we start and under the lambdas in the end. At least that's the problem I had with the cubical ring solver. Maybe there is some smart way around that here - I don't undestand the relevant code yet.

[MatthewDaggitt]

Do you have a concrete example that fails?

The problem I suspected, is with the variable 'ring'. It should be outside the pi when we start and under the lambdas in the end

Hmm yes so we have to lift the DB indices in the ring by the number of pi/lambda binders right?

[felixwellen]

I finally wrote down some tests/examples. As it turns out, integers seem not to normalize correctly (don't understand why). This is the first example (-module) here:

https://github.com/felixwellen/agda-stdlib/blob/issue-1116-generic-ring-solve/src/Tactic/RingSolver/Examples.agda

And then, the same lemma doesn't solve for generic rings. I also found out (last example in the file), that the stdlib-solver errors with a good message, when the CommutativeRing argument is not just a name. So to run into the deBruijn error, one has to accept general expressions of type AlmostCommutativeRing first.