Hypothesis renaming — mathlib4#1658

Stream: mathlib4

[Alistair Tucker]

For this PR the question seems to be whether it is OK to revise hypothesis names in mathlib4 defs and lemmas while the port is ongoing. As I understand it, once a function has been ported its existing mathlib3 hypothesis names cease to appear in mathlibport output and become basically irrelevant to the port effort generally. If that is so, I can’t see any reason to keep them sacrosanct in mathlib4.

[Alistair Tucker]

The reason the question arises is perhaps of interest in its own right. As they work in Lean 4 the cases using and induction using tactics label the case split with the names of hypotheses used in the relevant "custom recursor". Current mathlib3 hypothesis names have been chosen without view to this.

In this PR mathlib4#1658, I have experimentally changed hypothesis names in just three of these recursors so that, for example,

induction s using cons_induction with
| h₁ => …
| @h₂ c s hc ih => …

becomes

induction s using cons_induction with
| base => …
| @ind c t hc ih => …

[Alistair Tucker]

In fact this might be better

induction s using cons_induction with
| empty => …
| @cons c t hc ih => …

but to implement it one needs to introduce a hypothesis named cons into the body of Finset.cons_induction. I shied away from that initially but I guess it’s fine? The name clash can be resolved easily enough with the appropriate qualifiers.

[Eric Wieser]

Arguably this consideration was present in mathlib3 too

[Eric Wieser]

If you use induction combined with tactic#case, those names are accessible

[Eric Wieser]

I don't know if mathport supports the case tactic, but if it does then anything using the case tactic in mathilb3 is going to be relying on the old hypothesis names, and the mathport output will end up wrong.

[Alistair Tucker]

Good point! If I ever knew about tactic#case I had forgotten.

[Eric Wieser]

In the immediate term, it would be totally reasonable to change all the hypothesis names in unported files in mathlib 3

[Eric Wieser]

That way when those files get ported, they'll automatically get sensible names

[Eric Wieser]

You can find places to change by searching for elab_as_eliminator

[Johan Commelin]

I think it won't be a big problem, because we try to be pretty strict about unnamed hypotheses in mathlib 3.

[Johan Commelin]

But I agree that it doesn't hurt to work on this change in ml3.