mathport funext

Stream: mathlib4

[James Gallicchio]

Small issue -- looks like when porting lean3 funext tactic, mathport just put lean4 funext, which doesn't work -- it should probably (?) be replaced with funext _ everywhere it's used

[Mario Carneiro]

what does funext do in lean 3 and lean 4?

[Mario Carneiro]

Usually when tactic behavior doesn't match up it is preferable to fix the tactics rather than automate a wide scale usability regression

[Mario Carneiro]

unless there is an argument for why the new behavior is better than the old one

[James Gallicchio]

Both are basically equivalent to apply funext; intro, is my impression. lean3 funext would autogenerate a name if none was provided, while lean4 funext requires it. since lean4 intro autogenerates a name, funext should probably be modified to do the same

[Kevin Buzzard]

So basically there's a bunch of unhygienic lean 3 code being incorrectly ported

[James Gallicchio]

(Is there a situation where apply funext; intro _ wouldn't work as a translation..? not sure what effect hygiene issues have on porting)

[James Gallicchio]

There's actually a few unrelated mathport issues cropping up in Data.List.Permutation, should I make new threads or just list them here?

[Mario Carneiro]

James Gallicchio said:

Both are basically equivalent to apply funext; intro, is my impression. lean3 funext would autogenerate a name if none was provided, while lean4 funext requires it.

I'm asking what funext does, full stop no extra argument

[Mario Carneiro]

what do you mean by lean4 funext requires it? Is it an error?

[Mario Carneiro]

Kevin Buzzard said:

So basically there's a bunch of unhygienic lean 3 code being incorrectly ported

It's not clear to me that hygiene is the issue here. That would only be if follow up code talks about a or something assuming that the introduced name is a; our use of in lean 3 addresses most of those cases though

[Yaël Dillies]

Not in the case of ext, though. ext gets its name from the variable name that is used in the lambda expression.

[Mario Carneiro]

James Gallicchio said:

There's actually a few unrelated mathport issues cropping up in Data.List.Permutation, should I make new threads or just list them here?

You can put them in one thread, but the thread should be called Data.List.Permutation in that case

[Yaël Dillies]

And that is unhygienic because those names tend to change when lemmas are moved around.

[Mario Carneiro]

I said most

[Mario Carneiro]

lean 4 can do that too (variable names are officially part of the signature now)

[Mario Carneiro]

so you should not change the names of variables by moving them, that's a breaking change similar to changing the lemma statement

[James Gallicchio]

Mario Carneiro said:

what do you mean by lean4 funext requires it? Is it an error?

syntax error:

macro_rules
  | `(tactic|funext $x) => `(tactic| apply funext; intro $x:term)
  | `(tactic|funext $x $xs*) => `(tactic| apply funext; intro $x:term; funext $xs*)

It's a one-line fix :)

[Mario Carneiro]

well that was easy