Email Gateway (Aug 18 2022 at 15:54): Email Gateway (Aug 18 2022 at 15:54):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I’m trying to work with two mutual recursive, partially defined and
not-always terminating functions (It evaluates a program, the code is at
http://git.nomeata.de/?p=funcCF.git;a=blob;f=CFGraph/Eval.thy;hb=HEAD
if anyone is curious). The functions happen to be tail-recursive, so I’d
like to use the function package’s support for that.
Unfortunately, it fails when using both tailrec and sequential. But
already the following simple example fails, so don’t bother looking at
my code :-):
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
theory Tmp imports Main
begin
function (sequential,tailrec) f where "f True = 0"
apply pat_completeness
apply auto
done
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
gives me:
*** Tactic failed.
*** The error(s) above occurred for the goal statement:
*** f_sumC False = undefined
*** At command "done".
Is that easily fixable, or is there a work-around?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 15:54):From: Alexander Krauss <krauss@in.tum.de>
Hi Joachim,
These problems with "tailrec" are starting to become embarrasing for me. :-}
I just pushed a quick fix, which seems to help here, and also makes your
real example go through:
http://isabelle.in.tum.de/repos/isabelle/rev/39db63c45683
The patch also works for the Isabelle2009-2 release.
Hope this helps...
Alex
Email Gateway (Aug 18 2022 at 15:54):From: Joachim Breitner <mail@joachim-breitner.de>
HI,
thanks. Now a beginner question: Do you have to rebuild Isabelle to have
this fix, or can I just patch the file and it will work?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 15:54):From: Alexander Krauss <krauss@in.tum.de>
Joachim Breitner wrote:
thanks. Now a beginner question: Do you have to rebuild Isabelle to have
this fix, or can I just patch the file and it will work?
You have to rebuild, by running the "build" script at the root of the
Isabelle tree.
Alex
Email Gateway (Aug 18 2022 at 15:54):From: Joachim Breitner <mail@joachim-breitner.de>
Dear Alex,
thanks. I applied the fix, and it worked so far. But when I tried to
reduce the number of equations generated by sequential by simplifying
the pattern matches, I get an error message that does not occur without
tailrec. I could not cook up a simple example though.
This change worked:
http://git.nomeata.de/?p=funcCF.git;a=commitdiff;h=e9a10e7b004fbb1eb6f71a4195c39d6366338302
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/CFGraph/Eval.thy b/CFGraph/Eval.thy
index ee507b5..4e75111 100644
--- a/CFGraph/Eval.thy
+++ b/CFGraph/Eval.thy
@@ -39,8 +39,8 @@ function (sequential,tailrec,domintros)
= ( let b' = Suc b
in if v \<noteq> 0 then evalF contt [] ve b'
else evalF contt [] ve b')"
= (case as of [DI i] \<Rightarrow> i)"
| "evalC (App lab f vs) \<beta> ve b
= (let f' = evalV f \<beta> ve;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
while this change of the (seemingly) same kind fails:
http://git.nomeata.de/?p=funcCF.git;a=commitdiff;h=04c9da1123e3dc8aec3212a0a7bfaf8f9d66849d
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/CFGraph/Eval.thy b/CFGraph/Eval.thy
index 4e75111..c71295f 100644
--- a/CFGraph/Eval.thy
+++ b/CFGraph/Eval.thy
@@ -35,8 +35,9 @@ function (sequential,tailrec,domintros)
| "evalF (DP (Plus c)) [DI a1, DI a2, cont] ve b
= (let b' = Suc b
in evalF cont [DI (a1 + a2)] ve b')"
The error message I get is:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*** Proof failed.
*** accp evalF_evalC_rel x
*** 1. ⋀evalF_evalC_sum ct cf as ve b y cta cfa asa vea ba a list int aa lista
*** ab listb x.
*** ⟦⋀a list inta aaa lista aba listb x.
*** ⟦int = inta ∧ aa = aaa ∧ ab = aba; a = DI inta;
*** list = [aaa, aba]; lista = [aba]; listb = []; x = Suc ba⟧
*** ⟹ evalF_evalC_graph (Inl (aaa, [], vea, Suc ba))
*** (evalF_evalC_sum (Inl (aaa, [], vea, Suc ba)));
*** ⋀a list inta aaa lista aba listb x.
*** ⟦int = inta ∧ aa = aaa ∧ ab = aba; a = DI inta;
*** list = [aaa, aba]; lista = [aba]; listb = []; x = Suc ba⟧
*** ⟹ accp evalF_evalC_rel (Inl (aaa, [], vea, Suc ba));
*** ⋀a list int aa lista ab listb x.
*** ⟦False; a = DI 0; list = [aa, ab]; lista = [ab]; listb = [];
*** x = Suc ba; int = 0⟧
*** ⟹ evalF_evalC_graph (Inl (aa, [], vea, Suc ba))
*** (evalF_evalC_sum (Inl (aa, [], vea, Suc ba)));
*** ⋀a list int aa lista ab listb x.
*** ⟦False; a = DI 0; list = [aa, ab]; lista = [ab]; listb = [];
*** x = Suc ba; int = 0⟧
*** ⟹ accp evalF_evalC_rel (Inl (aa, [], vea, Suc ba));
*** y = Inl (aa, [], vea, Suc ba);
*** ct = cta ∧ cf = cfa ∧ as = [DI int, aa, ab] ∧ ve = vea ∧ b = ba;
*** asa = [DI int, aa, ab]; a = DI int; list = [aa, ab]; lista = [ab];
*** listb = []; x = Suc ba; int ≠ 0⟧
*** ⟹ accp evalF_evalC_rel (Inl (aa, [], vea, Suc ba))
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** evalF_evalC_graph x y ⟹ accp evalF_evalC_rel x
*** At command "done".
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
TIA for helping me out here,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 15:59):From: Alexander Krauss <krauss@in.tum.de>
Dear Joachim,
thanks. I applied the fix, and it worked so far. But when I tried to
reduce the number of equations generated by sequential by simplifying
the pattern matches, I get an error message that does not occur without
tailrec.
[...]
The error message I get is:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*** Proof failed.
*** accp evalF_evalC_rel x
*** 1. ⋀evalF_evalC_sum ct cf as ve b y cta cfa asa vea ba a list int aa lista
*** ab listb x.
*** ⟦⋀a list inta aaa lista aba listb x.
*** ⟦int = inta ∧ aa = aaa ∧ ab = aba; a = DI inta;
*** list = [aaa, aba]; lista = [aba]; listb = []; x = Suc ba⟧
*** ⟹ evalF_evalC_graph (Inl (aaa, [], vea, Suc ba))
*** (evalF_evalC_sum (Inl (aaa, [], vea, Suc ba)));
[...]
Tailrec performs some very ugly proofs internally, and unfortunately it
relies on the simplifier to do certain case splits automatically, which
does not seem to work in general in the presence of "case". There is no
fix at the moment, and I won't try to find one, since I am working on a
new package for certain classes of partial functions, which will subsume
and replace tailrec in its current form.
For the moment, if all else fails, you must fall back to the good old
while combinator (HOL/Library/While_Combinator".
Alex
Last updated: Nov 21 2024 at 12:39 UTC