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



Thanks Brian, that's what I thought.

Of course, an easy workaround is to use a case-expression or to split the let-
binding:

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

But a bug in still hidden somewhere.

Mathieu

Le vendredi 29 juillet 2011 09:08:32 Brian Huffman a écrit :
> Hi Mathieu,
> 
> I'm pretty sure that this is a bug in the function package.
> 
> If I do a theorem search for "f2_dom" during the termination proof, I
> see the following rule, which is apparently derived from f2.pinduct:
> 
> local.termination:
>   ⟦wf ?R;
>    ⋀v vb x xa y xb ya xc.
>       ⟦x = (v, Suc vb); (xa, y) = x; (xb, ya) = xa⟧
>       ⟹ (((ya + 2, xb + 1), xc - 1), v, Suc vb) ∈ ?R⟧
>   ⟹ All f2_dom
> 
> This rule is completely useless, because it does not let you assume
> anything about the variable xc. The correct form of this rule should
> have "xc" replaced with "y".
> 
> Compare this with the similar rule we get for the termination proof of f1:
> 
> local.termination:
>   ⟦wf ?R;
>    ⋀v vb vd x xa y xb ya.
>       ⟦x = (v, vb, Suc vd); (xa, y) = x; (xb, ya) = y⟧
>       ⟹ ((xb + 2, xa + 1, ya - 1), v, vb, Suc vd) ∈ ?R⟧
>   ⟹ All f1_dom
> 
> Here, the local assumptions imply that (v, vb, Suc vd) = (xa, xb, ya),
> making the rule possible to use in practice.
> 
> Unfortunately I can't think of a good workaround for this problem,
> unless you want to manually prove a corrected form of f2.pinduct and
> the termination rule, based on unfolding the definition of f2_dom. You
> will probably just have to wait for a bug fix from the developers.
> 
> - Brian
> 
> 
> On Fri, Jul 29, 2011 at 7:45 AM, Mathieu Giorgino
> 
> <mathieu.giorgino at irit.fr> wrote:
> > 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.