Zulip Chat Archive

Stream: lean4

Topic: simp fails if no progress

Scott Morrison (Jul 20 2023 at 09:39):

I've managed to get simp to fail if it doesn't make progress.

  • the Lean PR implementing it lean4#2334
  • the Lean PR turning it on by default lean4#2336
  • the Std PR std4#190 (currently depending on a custom toolchain)
  • the Mathlib PR #6019 (currently depending on a custom toolchain, and a custom Std branch)

Scott Morrison (Jul 20 2023 at 09:39):

Reviews at any point along that chain welcome. :-)

Scott Morrison (Jul 20 2023 at 09:40):

(Thanks @Mario Carneiro for the implementation help!)

Julian Berman (Jul 20 2023 at 09:43):

There's a 4 missing from the first linkifier I think

Ruben Van de Velde (Jul 20 2023 at 09:49):

Files changed 214

Sounds like fun :)

Eric Wieser (Jul 20 2023 at 09:50):

Is there a nice way to make make_two_goals; simp only consider "no progress" if simp doesn't progres on either goal?

Scott Morrison (Jul 20 2023 at 10:11):

We could have an any_goals combinator, which fails unless the tactic succeeds on at least one goal. In fact I think we had this in mathlib3.

Eric Wieser (Jul 20 2023 at 10:17):

Can you remind me what the advantage of tracking "no changes" inside simp vs outside simp as a combinator is?

Eric Wieser (Jul 20 2023 at 10:17):

Does it need information that's only available within simp?

Mario Carneiro (Jul 20 2023 at 10:20):

we had to modify the implementation a bit, but the way it works now, it could quite easily be done outside of simp: it fails with no progress iff the returned goal is a singleton of the input goal (the exact same MVarId)

Mario Carneiro (Jul 20 2023 at 10:21):

but I think we want it to be the default behavior anyway

Eric Wieser (Jul 20 2023 at 10:33):

I wonder if we want it to be the default for all tactics except those which opt-out somehow

Scott Morrison (Jul 20 2023 at 11:00):

While we could achieve the same result from something wrapping simp, that outside wrapper would then be depending on something that is observationally true about simp (namely, that if it makes no progress the returned goal is identically the same MVarId), but not strictly part of the specification of simp. I'd prefer that simp is "responsible" for ensuring that it fails correctly.

(For smaller tactics this distinction is perhaps less important, but simp is complicated!)

Eric Wieser (Jul 20 2023 at 11:58):

Thanks, that makes sense to me

Eric Wieser (Jul 20 2023 at 11:59):

I think the only other thing that concerns me is that simp { fail_if_no_progress := false} is long so people will type try simp instead, which isn't really the right thing

Jannis Limperg (Jul 20 2023 at 12:00):

I have some code lying around which implements a more extensional answer to the question "do two mvars represent the same goal?". It's mostly a straightforward check for syntactic equality of the hypotheses and the target (possibly ignoring mdata), though we have to match up FVarIds which may be different in the two goals. The only difficulty is, as always, the treatment of unassigned metavariables: if two metavariables occur in the same position in the goals, we have to (a) recursively check that they are equal and (b) make sure that henceforth these two metavariables are paired up, so when we see one in one goal, we have to see the other in the other goal.

Eric Wieser (Jul 20 2023 at 12:02):

If detecting if progress was made is something that is best for the tactic itself to do, could there be a standard way to communicate that to the ; combinator, and to allow something like allow_no_progress { simp at hx, simp } which means the same as your simp { fail_if_no_progress := false} at hx, simp { fail_if_no_progress := false}?

Kyle Miller (Jul 20 2023 at 12:07):

I've wondered about what sort of protocol we could have to communicate additional general configuration to tactics. For example, what if ? tac was how you could get a "Try this" for any tactic that supports it? This allowing no progress could be another such configuration.

Could this be implemented using set_option tactic.allow_no_progress true in tac and set_option tactic.try_this true in tac?

Scott Morrison (Jul 20 2023 at 12:07):

Not sure if everyone has seen this pr #3757 of @Thomas Murrills', which provides a highly configurable way to test if progress has been made.

Jannis Limperg (Jul 20 2023 at 12:34):

I had not, thank you! Related discussion.

Scott Morrison (Jul 31 2023 at 00:04):

In order to merge these PRs, it would be good to have clear consensus about changing the behaviour of simp to fail if it doesn't make progress.

The situation at present is that we have four PRs

  • the Lean PR implementing it lean4#2334 (coauthored with Mario)
  • the Lean PR turning it on by default lean4#2336
  • the Std PR std4#190 (currently depending on a custom toolchain)
  • the Mathlib PR #6019 (currently depending on a custom toolchain, and a custom Std branch)

For context, we have a general fail_if_no_progress combinator, which is currently not particularly capable, but Thomas Murrils' PR #3757 gives it many configuration options.

Thus is would be possible to achieve a "simp that fails if it makes no progress" without modifying the behaviour of simp, and instead wrapping it whenever needed. However, this would be depending on something that is observationally true about simp (namely, that if it makes no progress then the returned goal is identically the same MVarId), but not strictly part of the specification of simp. The PRs above make simp "responsible" for ensuring that it fails correctly.

The arguments in favour of having simp fail if it makes no progress by default are:

  • It's easier when writing proofs to see if any progress happened
  • simp_rw proofs will show errors when the simp set changes and causes a step to become ineffective
  • It is easier for tactics that use simp as a step to do flow control depending on whether it made progress

The argument against having simp fail if it makes no progress by default are:

  • Many tactics that use simp as a pre-processing step need to write try simp [...] or simp (config := {failIfUnchanged := false}) [...] now.
  • We need to slightly modify the behaviour of simp_all, so that the ordering of the hypotheses afterwards may have changed slightly. This did not appear to affect Mathlib.

I'll post a poll as the next message. It would be good if people could indicate their choice on that, and hopefully if there is positive consensus we'll be able to link to here from the release notes justifying this change.

Scott Morrison (Jul 31 2023 at 00:13):

/poll Should the default behaviour of simp be to fail if it makes no progress?

Scott Morrison (Jul 31 2023 at 00:14):

Finally, here are all the past discussions of this that I could find:

Last updated: Dec 20 2023 at 11:08 UTC