fallible rename_i

Stream: lean4

[Jad Ghalayini]

Right now, when I call rename_i I, it either gives an error if there are no more inaccessible variables, or binds the inaccessible variable to the name I. I can't do try rename_i I if there are no inaccessible variables, which is making my automation quite difficult. Is there a version where this is possible, or even better, a version which either binds I to the first inaccessible variable or does something else and/or binds I to something else?

[Mario Carneiro]

Here's a tactic idea: access a b renames all inaccessible variables that are variants of a or b to have accessible names with subscripts if necessary. access * does the same but for all inaccessible variables. access * => A B C names the variables A, B, C in order of occurrence in the local context

[Mario Carneiro]

it never fails; excess names are ignored, and _ or missing names in the => list use the default "subscript the variable" naming convention

[Arthur Paulino]

What if you provide a name that's already in use?

[Arthur Paulino]

I think this tactic is nice but I also think people would end up needing it due to some sort of "accident". So maybe it's worth taking a few steps back and rewriting the proofs in a way that the variables references aren't lost

[Jad Ghalayini]

The reason why I need it is because I want to uniformly handle each case of an induction which has different numbers of inductive hypotheses.

[Mario Carneiro]

Arthur Paulino said:

What if you provide a name that's already in use?

In the proposed access tactic, if you give a name that is already in use the newly renamed variable will shadow the old one. I don't see any other reasonable behavior.

[Mario Carneiro]

Arthur Paulino said:

I think this tactic is nice but I also think people would end up needing it due to some sort of "accident", such that it would be worth taking a few steps back and rewriting the proof in a way that the variables references by name aren't lost

Sure, but this happens sometimes. Especially if you are using the same tactic script on 10 very slightly different goals, you want tactics that can handle a little sloppiness.