Email Gateway (Aug 18 2022 at 17:05): Email Gateway (Aug 18 2022 at 17:05):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Hi all,
the following definition (a simplified version of what i need) of a
tail recursive function produces two subgoals, that can be proved, for
instance, by "apply auto". Nevertheless, the proof cannot be completed
(as can be seen by trying "by auto"). A goal seems to remain
unsolvable:
function (tailrec) remove :: "'a set => (nat => 'a) => 'a set"
where "remove A f = (if A = {} then A
else remove (A - {f 1}) (%k. if k < (1::nat)
then f k else f (Suc k)))"
Are there any problems with the definition? Which additional facts
have to be proved? (I am using Isabelle 2009-2).
Thanks in advance for any help,
Jesus
Email Gateway (Aug 18 2022 at 17:06):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Jesus,
If you try "apply auto", you should see the reassuring message "No subgoals!". Things go sour only when you enter "done", and then the error says "Proof failed". This indicates than an internal proof obligation couldn't be discharged by "function".
When such a thing happens with a definitional package (e.g., "datatype", "inductive", "function"), it usually indicates a bug in the package. The "tailrec" option is seldom used or tested; a bug there wouldn't be so surprising.
Alex will hopefully be able to help you here...
Cheers,
Jasmin
Email Gateway (Aug 18 2022 at 17:06):From: Alexander Krauss <krauss@in.tum.de>
Hi Jesus,
That's a very polite way of expressing it :-). "function (tailrec)" is
very buggy and currently the top thing on my kill list. It is a funny
coincidence that just today I eliminated the remaining uses from the
AFP, (cf. http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/cfeb14dc4509 ,
in particular, SatSolverCode.thy).
My recommendation is to move to Isabelle2011 and use the new
"partial_function (tailrec)" command. There is an example in
HOL/ex/Fundefs.thy, and you should be able to see from the changeset
above how to port things. Note that currently no pattern matching is
supported, but you can easily work around this by using "case" on the
right-hand side.
Hope this helps.
Alex
Last updated: Nov 21 2024 at 12:39 UTC