lean#4290 Closed simp tries using the forward version of use

Stream: lean4

[Yaël Dillies]

Not sure where to put this so that it is seen, but I just noticed that my issue lean#4290 wasn't quite fully fixed. If someone could reopen it, it would be great!

[Bhavik Mehta]

My impression was that your new example is intended behaviour!

[Kyle Miller]

I just left a comment on the issue:

I'd say that is a different issue, and in particular you're now asking for a new feature.

simp treats constants specially. It does not see foo_eq_bar n as having anything to do with foo_eq_bar, because once the term isn't just a constant, it goes through an elaboration process.

It seems reasonable, but there are a number of questions. The first that come to mind:

• if you have simp [foo_eq_bar n], should that erase the generic foo_eq_bar?
• if you have simp [← fun n => foo_eq_bar n] should that erase foo_eq_bar? (Why I ask: simp abstracts metavariables, so it would have to process lambdas. The question is "should simp detect the lemma to erase syntactically or post-elaboration".)
• would you be surprised if simp [← id foo_eq_bar n] erased id, if id were marked with @[simp]?

[Yaël Dillies]

I perfectly understand why this happens (identifier vs proof term), but from a usability point of view it is quite sad that specifying an argument can lead to your simp suddenly looping

[Yaël Dillies]

To answer your questions following that usability PoV:

• Yes, that's what the user expects when they specify an argument
• I see no use case for lambdas in simp (never saw one in four years of Lean), so happy to see it unsupported
• I can't come up with a reasonable example where applying a lemma changes its shape enough for it to act like a different lemma when rewritten backwards (it's actually even quite hard to come up with an appropriate description here)

[Yaël Dillies]

Basically, all I want is for simp to detect a plain application of a lemma, no more.

[Yaël Dillies]

This will solve all the cases I encountered where simp did something "clearly stupid" by rewriting with the same lemma back and forth many times

[Eric Wieser]

My reading of the lambda point is that the lambdas are inserted implicitly, so simp [add_comm _ b] ends up the same as simp [fun a => add_comm a b].

[Eric Wieser]

But in principle the loop-detection step could happen prior to this transformation

[Bhavik Mehta]

For the first point, I disagree that's what the user expects. If foo_eq_bar is a simp lemma, and I call simp [foo_eq_bar n], then I don't expect anything at all to be removed from the simp set!

[Eric Wieser]

I'd expect simp [foo_eq_bar n] to mean simp [foo_eq_bar n, - ←foo_eq_bar n] if that were legal syntax, but that might not be well-specified

[Kyle Miller]

Yaël Dillies said:

• Yes, that's what the user expects when they specify an argument

I'm a Lean user too, and this user wouldn't necessarily expect this, hence my question.

all I want is for simp to detect a plain application of a lemma, no more.

Does that mean you would not expect @foo_eq_bar n or (foo_eq_bar n) to have special support? Only foo_eq_bar n? I would find this to be surprising.

• I see no use case for lambdas in simp (never saw one in four years of Lean), so happy to see it unsupported

Eric is correct, lambdas are inserted implicitly. This is what "simp abstracts metavariables" means. It's very relevant, and I ask because I'm sure that you would bring up this issue again if simp lemma terms that elaborate to lambdas did not erase lemmas.

Yaël Dillies said:

This will solve all the cases I encountered where simp did something "clearly stupid" by rewriting with the same lemma back and forth many times

Please collect examples!