clean-upon-use

Stream: general

[Joachim Breitner]

Often when proving I am referring to some local hypothes, knowing that this is the last, or even only, use of this fact in this proof. I can make that explicit writing clean foo as the next tactic, and I think this is good style: it communicates that further down, this fact should not be used, makes the proof goal easier to read, and automatic tactics that look at the context might be faster.

But repeating the the name in a separate tactic is kinda verbose and extra work.

I wonder if it would be possible to have a convenient syntax to mark a use of a hypothesis as final (maybe something like foo- or -foo), causing that hypothesis to be cleared at the end of the current tactic.

Is it just me who would use such a device? Is that implementable? And is there some good space left in the always tight space of possible syntaxes?

[Yaël Dillies]

-h is already syntax in simp. Namely, it explicitly disables h as a simp lemma (so h wil often be a lemma rather than a local hypothesis, but still).

[Yaël Dillies]

It might be a nice educational tool but I wouldn't want this to become the standard for mathlib because it's more bookkeeping and syntax to learn with virtually no benefit.

[Yaël Dillies]

Another thing to take into account is that we value tactic modularity. We don't like overloading tactics (except tauto and other kitchen sink tactics because that's what they do).

[Kevin Buzzard]

I do tend to clear hypotheses and I typically put the clear tactic on the same line as the other tactic.

[Sebastian Ullrich]

Joachim Breitner said:

Is it just me who would use such a device?

I've pondered basically the same feature before fwiw, especially in involved program verification proofs. Implementing it could be a bit tricky, but should be possible (in Lean 4, more realistically) by adjusting the tactic interpreter. More problematic in tactics that contain other tactics though.