Niels Mündler (Apr 11 2021 at 23:38): Niels Mündler (Apr 11 2021 at 23:38):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?
Simon Roßkopf (Apr 11 2021 at 23:45):There is thin_tac. However its use is not really encouraged(See also ).
Mathias Fleury (Apr 12 2021 at 05:37):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.
Manuel Eberl (Apr 12 2021 at 11:00):Generally a good idea to give everything with a ‘tac’ in its name a wide birth. :wink:
Last updated: Dec 21 2024 at 16:20 UTC