Ring solver doesn't appear to normalise terms?

[MatthewDaggitt]

@oisdk I've just been testing the new ring solver and I've discovered that the following doesn't work

test : (x : ℕ) → x ≡ x
test x = begin
  x ≡⟨ solve (x ∷ []) ⟩
  z ∎
  where z = x

Unfortunately it did work with the old ring solver. From my (very!) limited knowledge, I'm guessing this might be fixable if we normalise the expressions first?

[MatthewDaggitt]

It also doesn't work for compound expressions, e.g. below:

test : (x : ℕ) → suc x ≡ suc x
test x = begin
  z ≡⟨ solve (z ∷ []) ⟩
  z ∎
  where z = suc x

I seem to remember @gallais discussing this at some point. I think this is probably harder to solve. Again the old ring solver could handle this case.

It also doesn't like this which is particular problematic in Data.Nat.Binary.Properties and Data.Rational.Unnormalised.Properties:

test : ∀ (f : ℕ → ℕ) x → f x ≡ 1 * f x
test f x = solve (f x ∷ [])

[oisdk]

Unfortunately for this kind of solver it would probably be impossible to normalise terms. An expression like this:

1 + x

Can be parsed in the ring solver into the correct AST. But if we normalise it, we would get:

suc x

Which can't, because it doesn't contain the ring operators. (it actually can handle this case, because I have put in a special case for Nat, but it isn't able to handle similar stuff for integers, etc.) In general, we have to avoid normalisation because we lose the names of the ring methods.

To fix the problem, there are two things we can do:

1. Rewrite the goal to be in the form that suits the solver. This would mean renaming f x to some variable in the second example, or avoiding the variable in the first.
2. You could use the old interface with the new backend (Tactic.Ringsolver.NonReflective).

At any rate, it would probably be worth putting together some documentation on these two cases in particular and how to avoid them.

[MatthewDaggitt]

Thanks for the clear explanation of why we can't normalise them! So example 1 is probably out. Mildly irritating but not too much of a problem as arguably it doesn't make the proofs very easy to read if you have aliases all over the place.

However couldn't we do something about the second set of examples? We're actually passing the "unit" we want to solve for, i.e. f x to the solver. So could we carry out your first suggestion automatically via reflection, by going through the expression and rewriting every instance of f x with a fresh variable, solving it and then reinserting f x afterwards?

[oisdk]

I'm not sure how you could spot occurrences of f x around the place: I'll have a think about it and see if I can come up with a solution.

[dylanede]

I've got a case where I have a module that takes in a commutative ring as an argument. In this case, auto-normalising all terms would retain the ring operations, right? Could there perhaps be a way of enabling normalisation in this case? Currently the new ring solver is unusable for me without this.

Regarding the main problem, perhaps what is needed (ideally, ignoring complexity) is a custom "semi-normalisation" that only goes as far as reducing to the ring operations.

Edit: I guess the new ring solver is still usable, just with the old interface, not the new one.

[MatthewDaggitt]

In my spare time I have tried fiddling around with the reflection to get it working for abstract rings, but not having used reflection very much I feel a little bit thrown in at the deep end!

Regarding the main problem, perhaps what is needed (ideally, ignoring complexity) is a custom "semi-normalisation" that only goes as far as reducing to the ring operations.

This would be great, but as you say is probably a fair bit of work.