RFC: `rcases`/`obtain` should always clear a variable

Stream: lean4

[Jovan Gerbscheid]

I'm working on making by_contra! work with rcases patterns. A natural implementation as a macro would be as follows: by_contra! $pat => by_contra h; push_neg at h; obtain $pat := h. However, when pat is just a variable, then obtain $pat := h doesn't do anything, and leaves the hypothesis as this inaccessible h. So instead, I need to replace obtain $pat := h with revert h; rintro $pat, which I think is quite awkward.

Is there a reason why obtain h' := h doesn't rename h to h'?

[Aaron Liu]

what the

[Aaron Liu]

I definitely expected it to do something

[Aaron Liu]

is it just a noop

[Aaron Liu]

maybe this is a bug?

[Joachim Breitner]

Jovan Gerbscheid schrieb:

revert h; rintro $pat, which I think is quite awkward.

What’s the downside of this?

[Jovan Gerbscheid]

It is less efficient and gives a more verbose/confusing tactic implementation.