Stream: Beginner Questions

Topic: Removing assumptions in apply style proofs


view this post on Zulip 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?

view this post on Zulip Simon Roßkopf (Apr 11 2021 at 23:45):

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

view this post on Zulip 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.

view this post on Zulip 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: Sep 25 2021 at 08:21 UTC