Assumption renaming in large context?

Stream: lean4

[Jason Yu]

Hi! I'm wondering what are the options for renaming assumptions in a large context. There's rename but it doesn't work if I want to rename multiple hidden assumptions of the same type. There's rename_i but when the context is large and the assumption I want to rename is far away, I have to put loads of _ as placeholders. case is basically the same as rename_i. I could turn off the hygienic option but that would make the proof more brittle.

I feel the following options would be nice if they exist:

• rename but only for hidden assumptions
• rename but allows renaming multiple assumptions of the specified type
• rename_i but allows specifying an offset index, with the index shown in infoview next to each assumption
• Combination rename and rename_i
• Perhaps support for some more general form of "assumption selector" that combines things like type patterns, indices, hidden or not etc

I'm fairly new to Lean btw. I hope I'm not misunderstanding certain things. Any comments or suggestions are welcome.

[Ruben Van de Velde]

Is "give them names before you get this far" an acceptable answer?

[Jason Yu]

If you are suggesting always naming all assumptions, I find doing that a bit too cumbersome. Most of the time I only want to use selected few of them. But thanks for the suggestions!

[Christian Merten]

I think there is no stable way to refer to anonymous hypothesis, so relying on rename or expose_names is typically code smell, because it can easily break.

Jason Yu said:

If you are suggesting always naming all assumptions, I find doing that a bit too cumbersome. Most of the time I only want to use selected few of them. But thanks for the suggestions!

Note that you can do

intro x _ _ y _ hx _ _ hy

to only name a subset of the variables.

[Jason Yu]

Christian Merten said:

I think there is no stable way to refer to anonymous hypothesis, so relying on rename or expose_names is typically code smell, because it can easily break.

Isn't case foo => rename_i a b c d basically the same as case foo a b c d => though?

I think it's just the autogenerated names that are unstable (thus turning off the hygienic option is not good). The order in which the assumptions are arranged should be stable. Otherwise how do we name them through intros or case? The types should be stable too as they are user specified.

Christian Merten said:

Note that you can do

intro x _ _ y _ hx _ _ hy

to only name a subset of the variables.

When I have lots of assumptions (say 30+) I would need to put lots of _ placeholders. Hence I'm looking for something like these:

Jason Yu said:

I feel the following options would be nice if they exist:

• rename but only for hidden assumptions
• rename but allows renaming multiple assumptions of the specified type
• rename_i but allows specifying an offset index, with the index shown in infoview next to each assumption
• Combination rename and rename_i
• Perhaps support for some more general form of "assumption selector" that combines things like type patterns, indices, hidden or not etc

[Christian Merten]

Jason Yu said:

When I have lots of assumptions (say 30+) I would need to put lots of `_` placeholders.

If you are really introducing 30+ hypothesis in a intro or case, you should consider bundling some of the assumptions in custom structures.

[Jason Yu]

Christian Merten said:

If you are really introducing 30+ hypothesis in a intro or case, you should consider bundling some of the assumptions in custom structures.

I should try that indeed. Thanks!