noisy ring

Stream: maths

[Kevin Buzzard]

import tactic.ring

example (s : ℚ) : (λ (q : ℚ), 3 * q + 4) ((λ (r : ℚ), (r - 4) / 3) s) = s :=
by ring -- succeeds, *and* prints `Try this: ring_nf`

[Johan Commelin]

Does by ring_nf close the goal?

[Kevin Buzzard]

yes and it's not noisy either :-)

[Patrick Massot]

I have also seen this behavior in the past, and this is pretty annoying, especially in the context where you are trying to teach a limited number of tactics.

[Reid Barton]

"People like you ended up buying: ring_nf"

[David Loeffler]

Is ring_nf faster than ring (when it works)? That would at least be some kind of justification. If not then it's definitely a bug.

[David Ang]

Does ring1 work? I think ring is something like ring1 <|> ring_nf

[Kevin Buzzard]

ring1 fails!

[Kevin Buzzard]

is_def_eq tactic failed, the following expressions are not definitionally equal (remark: is_def_eq tactic does modify the metavariable assignment)
  tactic.ring.horner 1 ((λ (q : ℚ), 3 * q + 4) ((λ (r : ℚ), (r - 4) / 3) s)) 1 0 : ℚ
and
  tactic.ring.horner 1 s 1 0 : ℚ
state:
s : ℚ
⊢ (λ (q : ℚ), 3 * q + 4) ((λ (r : ℚ), (r - 4) / 3) s) = s

[Kevin Buzzard]

I would not expect these things to be defeq. by dsimp; ring works fine, so it's the unexpanded lambdas which are causing the problem. Perhaps the moral is "expand your lambdas first"?

[Mario Carneiro]

ring succeeds and suggests ring_nf exactly in the case where ring1 would fail and ring_nf would succeed. If you don't want to teach ring_nf and pretend it doesn't exist, just use ring1 instead

[Kevin Buzzard]

But ring1 doesn't work here and it should, right?

[Mario Carneiro]

should it?

[Mario Carneiro]

ring uses defeq to determine whether two different atoms should be identified, but it does not do reduction when matching the shape of the expression. I guess it probably should, it used to when it was using qq match directly (before one of the optimization PRs)

[Kevin Buzzard]

I see -- you're perhaps saying that this is a "mission creep" situation where it's the user's job to get rid of the lambdas

[Mario Carneiro]

there is a well placed whnfR that will I think fix this particular situation, but there will be other cases where dsimp; ring will do more than ring alone