Stream: General

Topic: Translate terminal proof to single method


view this post on Zulip Florian Sextl (Nov 23 2021 at 13:26):

I have a proof by structural induction where several (28 of 29) cases can be proved directly with a terminal backward proof:

by cases auto (* which is just syntactic sugar for: proof cases qed auto *)

Now I'd like to omit these cases and just use a single method after the top level qed. Is there a way to translate this simple terminal proof into a single method that does all the goal refinement normally done by by and which can be used directly with qed?

view this post on Zulip Lukas Stevens (Nov 23 2021 at 13:35):

To clarify:

proof(induction _)
qed (cases; auto)

does not work?

view this post on Zulip Florian Sextl (Nov 23 2021 at 13:36):

No, unfortunately not.

view this post on Zulip Lukas Stevens (Nov 23 2021 at 14:01):

Ah, of course that does not work. What about

proof(induction _; cases)
qed auto

or

proof(induction _)
qed ((cases; auto)+)

view this post on Zulip Florian Sextl (Nov 23 2021 at 14:41):

I was able to change the setup of a few elimination rules in the meantime and now at least some of the subgoals can be proven with auto. Yet, there are still some which require cases auto and together with these your other suggestions also don't work.

view this post on Zulip Alexander Taepper (Nov 23 2021 at 15:22):

While it would be very helpful to see the lemma you are trying to prove, I could suggest trying

proof(induction _; cases)
qed (auto | assumption)+

as by makes implicit calls to assumption after applying the proof method

view this post on Zulip Alexander Taepper (Nov 23 2021 at 15:27):

Well, nevermind what I wrote above.. assumption are of course being resolved in the simplification process of auto.. my bad!

view this post on Zulip Florian Sextl (Nov 23 2021 at 15:33):

Thanks for the input. Unfortunately, by putting cases after induction, Isabelle only splits the value of some undefined predicate instead of splitting the correct data.

The formalization I'm working on is a bit too involved to post in one piece and not yet published to a public repository, but it's a rather direct port of the Iris framework's HeapLang formalization and the corresponding Coq lemma can be found here.

I just published the first draft of the port and the corresponding lemma can now be found here.


Last updated: Aug 15 2022 at 02:13 UTC