Re: [isabelle] Termination of function with let-binding on left-nested tuples
function (sequential) f2 :: "((nat * nat) * nat) \<Rightarrow> unit"
"f2 ((_, _), 0) = ()"
| "f2 n = (let ((a1, a2), a3) = n in f2 ((a2+2,a1+1), a3 - 1))"
by pat_completeness auto
Then it seems impossible to prove the termination of f2 (and "fun f2'" fails).
In the termination proof, we can see there is no equality relation for the
second component of the outermost pair.
It seems to be related to congruence rules in some way but I couldn't figure
out the exact problem.
Thanks for reporting this issue. The root of the problem lies in the way
the function package extracts recursive calls from the definition. This
information is then used in the construction of pretty much everything:
the function itself, the graph, the domain, the rules etc.
The extraction process, guided by congruence rules, is necessarily
heuristic in nature and known to be imprecise in some cases, which can
then lead to unprovable termination conditions. This is also the case
here (the code behaves exactly as specified), but the example is
especially disturbing, since the problem is so easy and completely
Here is a different instance of the same problem, which is a bit clearer:
function f3 :: "bool => nat => nat"
"f3 _ 0 = 0"
| "f3 b (Suc n) = (case b of True => f3 True | False => id) n"
Note that he branches of the case are functions, and one is a recursive
call. But the argument to the call sits at the other end of the term. A
similar thing happens in your example.
It seems that, unlike in most other situations, this cannot be solved
(in general) by adding some cong rules. Since I'd like the process to be
complete for situations like this one, I am considering adding special
treatment for tuple patterns, but this is not trivial...
This archive was generated by a fusion of
Pipermail (Mailman edition) and