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



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.