Stream: Beginner Questions

Topic: Unfinished termination proof allows to finish proof


view this post on Zulip Robert Soeldner (Jun 23 2021 at 13:21):

Hi,

I have a mutual recursive function defined using
function (sequential) ... by pat_completeness auto termination by lexicographic_order
where by the termination proof fails with unfinished subgoals. With this definition (incl. the unfinished proof goals), I'm able to proof a lemma using the simplifier, without the termination proof it fails. Is this an expected behavior?

view this post on Zulip Mathias Fleury (Jun 23 2021 at 13:23):

without termination, all simp rules are of the form "x in the terminating domain ==> f x = ..."

view this post on Zulip Mathias Fleury (Jun 23 2021 at 13:23):

With termination, the "termination domain" covers all values.

view this post on Zulip Mathias Fleury (Jun 23 2021 at 13:23):

So: yes this is expected.

view this post on Zulip Mathias Fleury (Jun 23 2021 at 13:25):

For the sake of an example:
f x = (if x >= 0 then x * (f (x-1)) else f x + 1

This is terminating for x >= 0, but you cannot use the simplification rule because the definition is not looping for x < 0

view this post on Zulip Manuel Eberl (Jun 23 2021 at 13:26):

Also, in the interactive mode in Isabelle/jEdit, proofs are checked in parallel and you can use a result before its proof has been checked. In particular, you can use a result even if the proof failed.

view this post on Zulip Robert Soeldner (Jun 23 2021 at 13:34):

Mathias Fleury said:

without termination, all simp rules are of the form "x in the terminating domain ==> f x = ..."

Does this mean, the unfinished subgoals will be excluded from the simp rules but I'm able to use the proven ones?

view this post on Zulip Mathias Fleury (Jun 23 2021 at 13:36):

termination has to prove all goals.

view this post on Zulip Robert Soeldner (Jun 23 2021 at 13:42):

Thank you, I will re-read few sections in https://isabelle.in.tum.de/doc/functions.pdf . Is there a way of showing, which steps the simplifier has used?

view this post on Zulip Jakub Kądziołka (Jun 23 2021 at 13:43):

you can do using [[simp_trace_new]] by simp


Last updated: Sep 25 2022 at 23:25 UTC