# [isabelle] Termination of function with let-binding on left-nested tuples

• To: isabelle-users at cl.cam.ac.uk
• Subject: [isabelle] Termination of function with let-binding on left-nested tuples
• From: Mathieu Giorgino <mathieu.giorgino at IRIT.FR>
• Date: Fri, 29 Jul 2011 16:45:29 +0200
• Organization: IRIT
• User-agent: KMail/4.6.1 (Linux/2.6.39-ARCH; KDE/4.6.5; x86_64; ; )

```Hi all,

I just noticed a problem with "let" bindings on left-nested tuples in function
definitions.

For example, these 2 functions -- each written with "function" and "fun" --
are exactly the same, excepted for the nesting of tuples.

-----------
theory Scratch imports Main
begin

function (sequential) f1 :: "(nat * nat * nat) \<Rightarrow> unit"
where
"f1 (_, _, 0) = ()"
| "f1 n = (let (a1, a2, a3) = n in f1 (a2+2, a1+1, a3 - 1))"
by pat_completeness auto
termination
apply (relation "measure (snd o snd)")
apply (auto simp del:in_measure)
by auto

fun f1' :: "(nat * nat * nat) \<Rightarrow> unit"
where
"f1' (_, _, 0) = ()"
| "f1' n = (let (a1, a2, a3) = n in f1' (a2+2, a1+1, a3 - 1))"

function (sequential) f2 :: "((nat * nat) * nat) \<Rightarrow> unit"
where
"f2 ((_, _), 0) = ()"
| "f2 n = (let ((a1, a2), a3) = n in f2 ((a2+2,a1+1), a3 - 1))"
by pat_completeness auto
termination
apply (relation "measure snd")
apply (auto simp del:in_measures)
oops

fun f2' :: "((nat * nat) * nat) \<Rightarrow> unit"
where
"f2' ((_, _), 0) = ()"
| "f2' n = (let ((a1, a2), a3) = n in f2' ((a2+2, a1+1), a3 - 1))"
-----------

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.

In these examples, the let could be replaced by the function pattern matching
but this problem also prevents those let-bindings in more complicated
functions.

An idea on what is going wrong ?

Thanks,

Mathieu

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.