Rename should not rewrite assumptions multiple times

[dnezam]

Imagine a proof state along the lines:

1. P x
2. P x'
---------
F

If I use rename [‘P x₁’, ‘P x₂’] on this state, the behavior is to keep renaming the one at the bottom, resulting in:

1. P x
2. P x₂
---------
F

I would argue a much more intuitive and useful behavior is to get a proof state along the following lines:

1. P x₂
2. P x₁
---------
F

I think this is related to #❓ Support > try applying a thm_tactic to all assumptions. @ 💬, which talks about rpt (drule th):

From @mn200

I want to support this so that you can write something like rpt (drule th) and have it do the right thing. Currently the semantics of that actual tactic are wrong, but it might turn into

  rpt (dmrule th) >> clearmarks

where dmrule “marks” the assumptions its used, so that each iteration finds a different one to drule against. Of course, the above might then get encapsulated into rpt_drule or similar.

[mn200]

Thanks for the issue. I agree that this would be nice. Note that it is reasonable to have rename list elements targeting separate parts of the same assumption, but this could be made a special case, and your behaviour could be the default. Alternatively, one approach might be to add functionality to the existing comments-in-quotations "tech", so that for example, one could write

rename [`P x1 (* x *)`, `P x2`]

where the x (as in first_x_assum and others) indicated that the corresponding assumption should be removed from consideration where the following matches are concerned. There could also be (* sx *) which would look for a sub-term within an assumption and then not consider that assumption again.