rename_i during porting

Stream: mathlib4

[Eric Wieser]

I've noticed a few cases now where rename_i has been added in the port to deal with an autogenerated name. Are we happy with this during porting, or should we be adding the explicit names to the tactics using autogenerated names?

[Eric Wieser]

In favor of just using rename_i is that this is something that's very easy to clean up later by just burninating all uses of rename_i post-port.

[Mario Carneiro]

rename_i is fine-ish. It's a code smell, but not terrible. Not all tactics allow you to control the new names, and even if they do if it's like induction' with a long list of names you might prefer to not do that and introduce the names in the cases instead (let's assume that the equivalent of induction didn't exist in this example). I've taken to using next a b => instead of rename_i though when used in this way

[Mario Carneiro]

It is the sort of thing a linter can find and possibly fix in the future though, so keep that in mind

[Arien Malec]

Each should be marked by a porting note.

[Shreyas Srinivas]

Arien Malec said:

Each should be marked by a porting note.

If a linter can find them then what purpose does the porting note serve?

[Arien Malec]

Searching through the codebase, marker to reviewers. Also there isn’t yet a lint.

[Eric Wieser]

I think a porting note is uneccessary, you can just search through the codebase for rename_i since it's pretty much always a code smell

[Arien Malec]

Just searching through the codebase, I'd say ~90% of the rename_i would be trivial to remove, and the other 10% are tactic bugs, missing features, which makes it really had to do what I'm suggesting for a porting note, to document why a rename_i was necessary...

[Shreyas Srinivas]

Arien Malec said:

Just searching through the codebase, I'd say ~90% of the rename_i would be trivial to remove, and the other 10% are tactic bugs, missing features, which makes it really had to do what I'm suggesting for a porting note, to document why a rename_i was necessary...

One would have to be an expert porter to find this out. Or alternatively ask experts. This would either slow down the port or use up the time of experts or both. If the linter does the job, then a diagnosis of why rename_I was used is not only consuming too much time, but also pointless. The linter could always be applied later to check for rename_I and the respective proofs improved.

[Eric Wieser]

Shreyas Srinivas said:

One would have to be an expert porter to find this out. Or alternatively ask experts.

This certainly isn't the case for the 90% of the rename_i that are trivial to remove, a quick look at the tactic documentation that introduced the inaccessible name is all that's needed

[Eric Wieser]

And that's probably less effort than having this discussion :)

[Arien Malec]

I'm preparing a refactor PR as we write.

[Shreyas Srinivas]

I replaced rename_i usage in my PR, by using induction' instead of induction. It only seems to make the proof more messy, and all just for preserving an identifier name.

[Yury G. Kudryashov]

You can use induction with case/case.

[Shreyas Srinivas]

is there an example for this?

[Arien Malec]

inductive Sum' (α : Type u) (β : Type v) where
  | inl (val: α) : Sum' α β
  | inr (val: β) : Sum' α β

theorem foo (s₁ : Sum' α β ) : Sum'.inl s₁ = a := by
  induction s₁
  case inl a => sorry
  case inr b => sorry

[Eric Wieser]

I think this works too?

  induction s₁ with
  | inl a => sorry
  | inr b => sorry

[Eric Wieser]

I don't know which is preferred

[Arien Malec]

!4#2429

What's left are:

• split and split_ifs
• nontriviality
• one case in Data.LazyList.Basic where intros eats a variable number after an apply (the rename_i here could be avoided by moving the intro and ext into each case but that would be...worse).
• some particularly ugly cases in Data.PFunctor.Univariate.M where there's some shadowing going on after an induction, and rename_i is used to reclaim the shadowed original hypotheses.

[Mario Carneiro]

Eric Wieser said:

I don't know which is preferred

You should prefer induction x with | foo x => over induction x; case foo x =>, because it has a more rigid structure. The case form should only be used when you are deliberately relaxing that structure, e.g. by proving only some of the cases and then using a different kind of automation