## Stream: General

### Topic: Translate terminal proof to single method

#### 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)+)
``````

#### 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.

#### 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: Aug 15 2022 at 02:13 UTC