Proof hygiene

Stream: new members

[Jacob Weightman]

I have a relatively long proof where I find myself using the have tactic and let a lot. As I keep going, I find the environment is getting quite cluttered with definitions that I no longer need. This leads me to two questions:

1. Is there a tactic that allows me to remove or hide things from the context in the Lean Infoview?
2. Are there "best practices" to avoid this problem, or perhaps tactics I'm not aware of?

[Notification Bot]

A message was moved here from #new members > RealWorld in the IO Monad by Vlad Tsyrklevich.

[Vlad Tsyrklevich]

If you no longer need them, is it possible that the definitions actually belonged in a previous have/let, and should not have been top-level definitions?

[suhr]

The natural way to manage this is scoping:

let bigResult1 =
  let small1 = ...
  let small2 = ...
  ...
-- `small1` and `small2` are not in the scope anymore
let bigResult2 =
  ...
...

[Daniel Weber]

You could also use clear to remove hypotheses, i.e. clear small1 small2

[Winston Yin (尹維晨)]

Sometimes having lots of haves and lets is inevitable, but this is “forward” thinking, where you manipulate and combine assumptions until they look like the goal. Instead, the more idiomatic style in Lean is “backward” thinking, manipulating and splitting the goal until it looks like the assumptions. Both are mathematically equivalent, but the latter results in less clutter. If you find that you must introduce a special term using have or let, you can often abstract it out into a separate lemma which can be invoked within the current proof.

Perhaps we can help you golf your proof if you provide a #mwe.

[Ruben Van de Velde]

I would disagree that "backwards" reasoning is the only idiomatic style in lean.

[Ruben Van de Velde]

Instead, many haves might indicate that your proof can be split into multiple lemmas

[Shreyas Srinivas]

Sometimes when you are performing forward reasoning, the replace and specialize tactics are handy

[Eric Wieser]

Perhaps it's not possible, but one thing I'd like is a have bar := some_lemma (clear% foo) which has roughly the same effect as have bar := some_lemma foo; clear foo

[Jacob Weightman]

Awesome. I didn't want to bog down the question with the full context of what I'm working on, but every single one of these answers was helpful in tidying up my proof. Thanks everyone!