Tactic to clear unneeded hypotheses

Stream: Is there code for X?

[Bolton Bailey]

I may have asked this a few years ago but: Is there a tactic that will try to identify hypotheses that aren't necessary to prove the goal and remove them? For example, if I have h : a = b and this is the only place where a appears, then this hypothesis can be removed.

[Joachim Breitner]

clear h?

ah, you mean it identifies the unhelpful ones for you?

There is https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/Cleanup.html#Lean.MVarId.cleanup but I don’t see it exposed as a tactic.

[Mario Carneiro]

if you have a have in your proof, clearly that hypothesis is redundant and can be removed :P

[Damiano Testa]

Joachim Breitner said:

clear h?

ah, you mean it identifies the unhelpful ones for you?

There is https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/Cleanup.html#Lean.MVarId.cleanup but I don’t see it exposed as a tactic.

There was some talk of getting prune to do that, but it is something I have not gotten around to. The initial PR is #5062.

[Mario Carneiro]

Even the example you gave is not definitely a useless hypothesis, it is generated by generalize and you can observe that there are lots of uses of it in the wild

[Mario Carneiro]

also removing hypotheses about equality to the original value generated by match can cause termination proofs to fail