*To*: Mathieu Giorgino <mathieu.giorgino at irit.fr>*Subject*: Re: [isabelle] Termination of function with let-binding on left-nested tuples*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 29 Jul 2011 09:08:32 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1375594.JkJhBao4WR@leh>*References*: <1375594.JkJhBao4WR@leh>*Sender*: huffman.brian.c at gmail.com

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 >

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

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

- Previous by Date: [isabelle] Termination of function with let-binding on left-nested tuples
- Next by Date: Re: [isabelle] Termination of function with let-binding on left-nested tuples
- Previous by Thread: [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