Florian Sextl (Nov 23 2021 at 13:26): 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?
Lukas Stevens (Nov 23 2021 at 13:35):To clarify:
proof(induction _)
qed (cases; auto)
does not work?
Florian Sextl (Nov 23 2021 at 13:36):No, unfortunately not.
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)+)
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.
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
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!
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: Dec 21 2024 at 16:20 UTC