Email Gateway (Aug 19 2022 at 10:31): Email Gateway (Aug 19 2022 at 10:31):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Alex,
Thanks for looking into this. Your rule is more or less the
contrapositive to mine (in terms of "= undefined" and P). I proved your
rule and it works for showing undefinedness in case of non-termination
(there an introductory contrapos_np step, but that's all). Do you think
this should be the default induction rule for (tailrec)? Currently,
partial_function (tailrec) generates no induction rule at all. If so, I
can adapt Partial_Function.thy accordingly.
Andreas
Email Gateway (Aug 19 2022 at 10:31):From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,
Yes, go ahead! This rule should be the default.
Alex
Email Gateway (Aug 19 2022 at 10:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Every now and then, I want to prove that a function that I have defined
with partial_function (tailrec) is undefined when the recursion does not
terminate. Unfortunately, partial_function (tailrec) does not generate
an induction theorem for the functions. So I set out to prove my own
generic induction rule (fixp_induct_tailrec_undefined in the attachment)
similar to fixp_induct_option in Partial_Function.thy. If I manually
instantiate it with the ..._def theorem of the partial function ...,
everything works fine. However, when I register it as the induction
theorem to be used for tailrec (like it is done for fixp_induct_option
and option in Partial_Function.thy), I only get exceptions when using
partial_function.
What's wrong with my induction theorem? How can I change it such that it
works with partial_function?
Andreas
Scratch.thy
Email Gateway (Aug 19 2022 at 10:47):From: Alexander Krauss <krauss@in.tum.de>
Hi Andreas,
partial_function currently expects induction rules whose conclusion is
of the form "... ==> P x y" where ... intuitively means "f x terminates
and evaluates to y". In the option monad, this is simply "f x = Some y
==> P x y", but in the degenerate tailrec monad you would get something
like "f x = y ==> y ~= undefined ==> P x y".
I just tried this and got the following rule accepted by partial_function.
lemma fixp_induct_tailrec_undefined:
fixes F :: "'c ⇒ 'c" and
U :: "'c ⇒ 'b ⇒ 'a" and
C :: "('b ⇒ 'a) ⇒ 'c" and
P :: "'b ⇒ 'a ⇒ bool" and
x :: "'b"
assumes mono: "⋀x. mono_tailrec (λf. U (F (C f)) x)"
assumes eq: "f ≡ C (ccpo.fixp (fun_lub (flat_lub undefined)) (fun_ord
tailrec_ord) (λf. U (F (C f))))"
assumes inverse2: "⋀f. U (C f) = f"
assumes step: "⋀f x y. (⋀x y. U f x = y ⟹ y ≠ undefined ⟹ P x y) ⟹ U
(F f) x = y ⟹ y ≠ undefined ⟹ P x y"
assumes result: "U f x = y"
assumes defined: "y ≠ undefined"
shows "P x y"
sorry
I believe this rule should be provable and sufficient for what you want.
I cannot say on the spot whether partial_function could be modified to
accept rules like yours. The problem is the curry/uncurry translation,
which must do some explicit instantiations and assumes a certain
syntactic form.
Let me know when you make progress (or run into more problems).
Alex
Last updated: Apr 25 2024 at 20:15 UTC