Stepping through simp_rw

Stream: mathlib4

[Eric Wieser]

Where do I need to put my cursor to see the intermediate state in this simp_rw?

example {x : ℕ} : 1 + x * 2 = x + x + 1 := by
  simp_rw [mul_two, add_comm]

[Eric Wieser]

Are we missing the equivalent of this save_info rule.pos line in Lean 3?

[Eric Wieser]

It's pretty hard to port a broken simp_rw without being able to step through it

[Eric Wieser]

Especially since it seems simp_rw [foo, bar, baz] now silently continues with baz if bar fails to match anything

[Kevin Buzzard]

Do the devs know that simp is not failing when it's a no-op and it's not as nice? Is this expected behaviour because this is another reason that it's annoying. Should someone open an issue?

[Yury G. Kudryashov]

@Anne Baanen and @Mario Carneiro are listed as the authors of simp_rw in Mathlib4

[Eric Wieser]

I think it's maybe ok for simp to behave that way, but it is definitely a bug for simp_rw

[Yury G. Kudryashov]

IMHO, if simp didn't use an explicitly listed lemma, then it's at least as bad as an unused argument in a function.

[Eric Wieser]

That stance is incompatible withext; simp [foo, bar] where foo is used by the first goal and bar the second, I think

[Yury G. Kudryashov]

You mean ext <;> simp [foo, bar]

[Thomas Murrills]

Could a linter tell if a lemma wasn’t used by at least one goal? I’m not sure how powerful linters are

[Yury G. Kudryashov]

Probably, the right question is "can a linter tell ... without slowing everything down too much?"

[Mario Carneiro]

yes it is possible for a linter to do this, although it needs some additional frameworking. We already have the "unreachable tactic" linter which warns on e.g. example : 1 = 1 := by first | rfl | simp [foo]

[Mario Carneiro]

and it would be nice to extend this to unreachable "parts" of a tactic. To handle the ext <;> simp [foo, bar] situation you have to mark each part of a tactic that can be considered used, and then mark each such part as used whenever it does something as part of the tactic invocation. Then you go through the info tree in the linter and warn whenever there is a part which is marked as usable but never marked as used

[Mario Carneiro]

This is already implemented, but only for entire tactics. For parts of tactics the tactics themselves have to cooperate with the linter and add appropriate annotations into the info tree

[Yury G. Kudryashov]

What does %$e do in | (rwRule| $e:term) => (tactic| simp%$e only [$e:term] $(loc)?) in simp_rw?

[Thomas Murrills]

Oh, interesting! Infotrees are on my list of things I (know that I) don’t understand about lean yet, so it’s nice to see an example of what they get used for.

So is the goal to make it so that unreachable parts of tactics get flagged automatically, even without tactics explicitly cooperating internally? Or is the opt-in cooperation something we want to keep, and we just need better frameworks to handle it?

[Yury G. Kudryashov]

Did simp loose the fail_if_unchanged config option in Lean 4?

[Thomas Murrills]

Yury G. Kudryashov said:

What does %$e do in | (rwRule| $e:term) => (tactic| simp%$e only [$e:term] $(loc)?) in simp_rw?

I’m also curious about this. I’ve seen x%$e used to match an explicit x and name it e, but it’s on the other side of a match here and seems to come from other syntax. Does it somehow update the syntax node generated by simp with info from e in…some way?

[Thomas Murrills]

my guess is that when that generated simp produces e.g. error messages tied to its syntax, it’ll use the ref e for that, even though I’m not sure of how the internals play out/what % “really does” here.

[Mario Carneiro]

Yury G. Kudryashov said:

Did simp loose the fail_if_unchanged config option in Lean 4?

Yes, lean 4 tactics for the most part don't know how to detect if the goal changed. I was thinking about making a general fail_if_unchanged combinator which just checks that the goal list is the same as before and all the original goals are still unassigned

[Mario Carneiro]

Thomas Murrills said:

my guess is that when that generated simp produces e.g. error messages tied to its syntax, it’ll use the ref e for that, even though I’m not sure of how the internals play out/what % “really does” here.

Yes, it annotates the simp token with the info from e, so that for example if simp fails then e will be highlighted

[Mario Carneiro]

Thomas Murrills said:

So is the goal to make it so that unreachable parts of tactics get flagged automatically, even without tactics explicitly cooperating internally?

That's impossible, there is no way to know how an arbitrary tactic interacts with one of its arguments since it could be parsing it or using it in many ways - tactics define their own syntax

[Thomas Murrills]

makes sense, I was thinking there might have been some complicated behind-the-scenes way to trace whether a given input (of any form) winds up influencing the tactic state in some way…now that I write it out that sounds like it would be difficult, costly, and require far more infrastructure than is available to a linter though 😅

[Thomas Murrills]

Mario Carneiro said:

Yury G. Kudryashov said:

Did simp loose the fail_if_unchanged config option in Lean 4?

Yes, lean 4 tactics for the most part don't know how to detect if the goal changed. I was thinking about making a general fail_if_unchanged combinator which just checks that the goal list is the same as before and all the original goals are still unassigned

I implemented fail_if_no_progress for the port of Tactic.Group; I think I’ve learned some things in the short time since I wrote it, though, so I’ll take another look tomorrow…also I don’t do that assignment check, so that’s one thing to change. (also I’m open to making this a separate PR, wasn’t sure.)

[Thomas Murrills]

that’s in !4#2122

[Mario Carneiro]

that sense of "no progress" is quite a bit more expensive to check and I would not use it for most tactics' internal "has anything changed" check

[Mario Carneiro]

but it is a reasonable user-facing tactic combinator

[Thomas Murrills]

hmm, since these are related notions conceptually, should we just have one function/tactic with an argument/config to specify which checking behavior (cheap or costly) it performs? or should they be named differently in your opinion

[Yury G. Kudryashov]

What about a set_option lint.unchanged?

[Yury G. Kudryashov]

So that we can temporarily switch it on while porting.

[Thomas Murrills]

(I feel like I might want to learn about linters soon...there seem to be a couple of interesting potential projects :) )

[Mario Carneiro]

I don't think an option is appropriate here, because it is a semantic change to the tactic's behavior

[Thomas Murrills]

I thought Yury was suggesting also (separately) having an option to lint tactics which do not change the goals, which could be useful (but I’m not sure)

[Mario Carneiro]

oh I see, so catching e.g. calls to skip in a proof, sure that is possible

[Yury G. Kudryashov]

An explicit skip can be used, e.g., in <;> [skip, do_something]

[Yury G. Kudryashov]

I meant something like simp that changed nothing.

[Yury G. Kudryashov]

(or a simp_rw step)

[Eric Wieser]

Does it make sense to split this thread? The discussion seems to have gone a different direction from the original "the goal view isn't updated between rules" question

[Mario Carneiro]

Yury G. Kudryashov said:

An explicit skip can be used, e.g., in <;> [skip, do_something]

It is easy enough to make special cases for this kind of thing in a linter. You wouldn't usually give a lint warning without a very concrete semantics preserving code modification in mind

[Alex J. Best]

I made !4#3738 for the original issue of @Eric Wieser

[Alex J. Best]

One remaining question, inspired by the extended thread above, should we actually use fail_if_no_progress inside simp_rw so that we do see a failure if the user tries to simp_rw with a lemma that doesn't apply?

[Eric Wieser]

We definitely should, though it might be better to do that in a follow-up as I expect some proofs to break

[Damiano Testa]

It might even be a Try this, instead of failing.

[Eric Wieser]

I think fail_if_no_progress does the wrong thing; it doesn't check the lemma was actually used, right?

[Eric Wieser]

If simp_rw [foo, bar] expands to simp only [foo], simp only [bar] then the first simp might just "make progress" via basic kernel reduction and not via foo

[Alex J. Best]

You mean like some beta reduction or whatever? I guess thats possible, maybe simp_rw could just run simp only [] <;> simp only [h] (i.e. do an empty simp first before running any lemmas

[Eric Wieser]

Every intermediate lemma could have the same problem

[Eric Wieser]

Doing one before each step would likely be safe

[Alex J. Best]

Hmm, could you give an example of what you mean? I don't quite understand how un-simp only-reduced terms could show up after a simp only?

[Eric Wieser]

I'm thinking of the case where one of the lemmas has a non-beta-reduced RHS

[Eric Wieser]

But maybe you're right

[Thomas Murrills]

fail_if_no_progress checks if the types of everything are unchanged up to defeq, so presumably basic kernel reductions would count as “no change”.

However, I do have some code I’ve been meaning to PR which gives fail_if_no_progress config options which let you tweak exactly what counts as progress. This includes e.g. the ability to choose to use BEq for expressions instead of defeq, which would reintroduce the kernel reduction distinction but might be less expensive. Lmk if that would be of interest!

[Alex J. Best]

Yes, so much of interest that I was already halfway through doing it myself!

[Alex J. Best]

So I'll happily use your version, is it on a branch somewhere (I really only got around to tweaking the transparency settings, which I found to be insufficient, beq is much better)

[Thomas Murrills]

Yes, it’s on the fail_if_no_progress branch! (Sorry, I was asleep by the time this message came in.) I’ve just (rebased to master/force-pushed) and opened a PR (!4#3757), so it should be at least usable/testable-with.

Warning: I haven’t really looked at it since a few months ago. I last remember thinking there were too many config options. But the basic ones should remain untouched. I’ll try to finish it up today or tomorrow! :)

[Thomas Murrills]

update, since I said I’d do this today: found myself pushing through a headache, and couldn’t do all I hoped to. I’m prioritizing mono, but I hope to get the fail_if_no_progress config options done by Friday (or sooner, if possible). :)

[Alex J. Best]

Ok great, i don't think there is any rush to get this finished, it's a nice feature but not blocking anything so no worries on it taking longer. Hope you feel better @Thomas Murrills .
An update for anyone following along, simp_rw now show goals as you step through and fails if no progress was made (in the beq sense). I've fixed many places in the library where simp_rw wasn't doing anything in the same pr. This could be split up but i don't think the changes are too numerous.

[Eric Wieser]

It might be beneficial to split out the "show goals as you step through" part, as that's very useful when porting

[Eric Wieser]

Did you have that working already, or did one feature require the other?

[Alex J. Best]

Neither feature really requires the other. I don't mind splitting it if it's useful enough.

[Eric Wieser]

I've had a lot of files where being able to step through simp_rw would be very useful for debugging

[Eric Wieser]

Of course, failing when no progress is made is also very useful, but I'd prefer to have one of those features this week rather than both in two weeks

[Alex J. Best]

Ok #3738 is ready then, unfortunately I force pushed as reverting the merge commit was ugly so I had to squash everything.
I've left the fixes to the existing proofs in as those were tested on this exact tactic (just without the logic that complained if they weren't changed). Therefore the diff is a bit large but it should be pretty clear that most lines are just removing a lemma or two from simp_rw.

[Alex J. Best]

#3782 is the follow up

[Eric Wieser]

!4#3738, !4#3782