*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Termination of function with let-binding on left-nested tuples*From*: Mathieu Giorgino <mathieu.giorgino at irit.fr>*Date*: Fri, 29 Jul 2011 18:26:31 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CAAMXsibRVsb-S1-bTHup-Tfc=y6A+UA7svF8fpfRvrLk8veBvw@mail.gmail.com>*Organization*: IRIT*References*: <1375594.JkJhBao4WR@leh> <CAAMXsibRVsb-S1-bTHup-Tfc=y6A+UA7svF8fpfRvrLk8veBvw@mail.gmail.com>*User-agent*: KMail/4.6.1 (Linux/2.6.39-ARCH; KDE/4.6.5; x86_64; ; )

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

**References**:**[isabelle] Termination of function with let-binding on left-nested tuples***From:*Mathieu Giorgino

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

- Previous by Date: Re: [isabelle] Termination of function with let-binding on left-nested tuples
- Next by Date: Re: [isabelle] the state of the lattice theories
- Previous by Thread: Re: [isabelle] Termination of function with let-binding on left-nested tuples
- Next by Thread: Re: [isabelle] Termination of function with let-binding on left-nested tuples
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list