rcases modifies assumptions

Stream: mathlib4

[David Ang]

I feel like Lean is sometimes too eager to include redundant assumptions. For instance, is this intended behaviour?

import Mathlib.Tactic
variable (n : Nat) (h : n = n)
lemma one : n = n := by rcases n <;> rfl
#check one -- (n : ℕat) (h : n = n) : n = n
lemma two : n = n := by clear h; rcases n <;> rfl
#check two -- (n : ℕat) : n = n

Here rcases n modifies h, so Lean thinks one needs h. I can hide h by doing clear as in two.

[Yury G. Kudryashov]

How could rcases guess that it shouldn't touch h?

[Yury G. Kudryashov]

David Ang said:

I feel like Lean is sometimes too eager to include redundant assumptions. For instance, is this intended behaviour?

As far as I understand, if you come up with a solution to this problem that doesn't slow down Lean too much, it would be very nice. In the meantime, don't have extra assumptions in variables.

[Kyle Miller]

That's to say, there have been a number of long discussions about this problem on the Zulip already. If not intended, it's definitely a known behavior.

[David Ang]

Yury G. Kudryashov said:

How could rcases guess that it shouldn't touch h?

I think it’s fine that rcases touches h, but once the lemma proof ends Lean can perhaps find out exactly which assumptions are actually used (and not just modified) and delete the rest. I don’t know whether this is the way it’s currently handled or whether it’s feasible to do it this way though.

[David Ang]

Kyle Miller said:

That's to say, there have been a number of long discussions about this problem on the Zulip already. If not intended, it's definitely a know behavior.

Could you link me to a topic? I searched for rcases and none of the existing topics I found talked about this exact problem.

[Yaël Dillies]

See eg https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Lean.204.20adds.20variable.20to.20args.20for.20no.20reason

[Yaël Dillies]

This is not specific to rcases at all.

[Kyle Miller]

David Ang said:

Yury G. Kudryashov said:
I think it’s fine that rcases touches h, but once the lemma proof ends Lean can perhaps find out exactly which assumptions are actually used (and not just modified) and delete the rest.

I've had this thought too, but it seems like it would be complicated to implement and probably not possible with the current tactic architecture. rcases (and cases and induction and ...) works by reverting all the local hypotheses that depend on the given variable, computing a motive from that, and applying the variable's type's recursor, and then intro-ing variables in the resulting goals to make them look like the obvious results of a case analysis. Remember that tactics are constructing partial proof terms -- reverting variables causes them to be used, even if they're not "used". To eliminate these used but "unused" variables, you'd need to go back and change the proof terms. It doesn't seem impossible, but I don't think you can do it without re-engineering much more than just individual tactics.

[Kyle Miller]

Another thread https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60induction.60.20tactic.20changes.20type.20signature.3F/near/338448701

[Kyle Miller]

And another https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Auto.20include.20variables/near/366740413

[Damiano Testa]

Also, regardless of whether the removal of "unnecessary" hypothesis can be easily implemented or not, my preference would be that, once you begin the proof, everything in the infoview survives the final term.

[Damiano Testa]

I prefer to remove by hand "unused" hypotheses, than to leave it to an automated process. Of course, I would also very much welcome an "unused hypotheses" linter that would highlight these hypotheses automatically!

[Eric Wieser]

#6594 is another example of this coming up

[Eric Wieser]

Do we have a tracking issue for this?