Dear community,

I am working a lot with apply style proofs using the Separation Refinement Framework. In the course of these proofs, many assumptions build up and tend to slow down proofs significantly. However many assumptions are not really required at that point of the proof, so I would like to discard them for further steps. Is there a canonical way (proof pattern, proof method) for this? Or does anyone have a suggestion on how to build such a method?

There is `thin_tac`

. However its use is not really encouraged(See also ).

In such cases I convert the proof to Isar (I have a tool that converts such goals to have or lemma or context+lemma). In my experience, the apply-version of the proofs is too fragile to be useful.

Generally a good idea to give everything with a ‘tac’ in its name a wide birth. :wink:

Last updated: Aug 10 2022 at 19:17 UTC