Re: [isabelle] Common monadic programming idioms and termination



Dear Andreas,

Thanks!  That was obvious in hindsight.  I now have termination
conditions that look much more amenable.

Many thanks,
Dominic

On 27 October 2015 at 12:24, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
> Dear Dominic.
>
> The congruence rules must be declared as [fundef_cong] before the function
> definition takes place. In your example, they are declared between the
> definition and the termination proof.
>
> The theorems about set_error help to automate the termination proof. You can
> discover such lemmas when you try to do the proof manually.
>
> Best,
> Andreas
>
>
> On 27/10/15 12:41, Dominic Mulligan via Cl-isabelle-users wrote:
>>
>> Hi,
>>
>> Actually, after returning to this subject after unfortunately getting
>> distracted doing something else, I'm afraid that the lemmas that
>> Manuel suggested do not seem to work in transforming the termination
>> conditions generated by Isabelle into something that looks provable.
>> I've attached the same stripped down Isabelle theory file as last time
>> with the suggested lemmas added, marked as fundef_cong, and the issue
>> remains at the point marked XXX.  This persists after trying to use
>> some alternative congruence rules, also.
>>
>> Part of the issue is that I have no idea what the need for the rather
>> mysterious set_error_fail and set_error_return lemmas is in Manuel's
>> previous e-mail, or how I would even go about finding the need for
>> those lemmas.  From what I understand the "set_error" constant is
>> automatically generated by the new datatype machinery, but how this
>> interacts with termination is not clearly documented in either of the
>> Datatype or Function PDFs bundled with Isabelle.
>>
>> Lastly, is there any way to get Isabelle to spit out which congruence
>> rules it is trying to apply when constructing these proof obligations,
>> or which congruence rules it at least has knowledge of other than
>> grepping the Isabelle library source?
>>
>> Many thanks for any help,
>> Dominic
>>
>> On 23 October 2015 at 16:48, Manuel Eberl <eberlm at in.tum.de> wrote:
>>>
>>> The problem is that you have a recursive call in an argument of the
>>> âbindâ
>>> function, and the function package has no idea what kind of parameter
>>> this
>>> call will get.
>>>
>>> For instance, the âbindâ function could simply double the list it gets as
>>> the first input and call the function it gets as second input on it â
>>> then
>>> your function would never terminate.
>>>
>>> So, what you need to do is you need to tell the function package a little
>>> bit about what kinds of inputs the âbindâ function will give to its
>>> function
>>> parameter. You can do that with a congruence rule:
>>>
>>>
>>> lemma error_bind_cong [fundef_cong]:
>>>    "(map_error f x = map_error f' x') â error_bind x f = error_bind x'
>>> f'"
>>>    by (cases x; cases x') simp_all
>>>
>>> This essentially implies that bind only calls the function you give it
>>> with
>>> a value contained in the error object you give it. Once you have proven
>>> this
>>> lemma and declared it as [fundef_cong], your proof obligation in the
>>> termination proof will look a lot saner.
>>>
>>> Add two more simp lemmasâ
>>>
>>> lemma set_error_fail [simp]: "set_error (error_fail m) = {}"
>>>    by (simp add: error_fail_def)
>>>
>>> lemma set_error_return [simp]: "set_error (error_return s) = {s}"
>>>    by (simp add: error_return_def)
>>>
>>> âand everything works automagically.
>>>
>>>
>>> Cheers,
>>>
>>> Manuel
>>>
>>>
>>> the function package does not know anything about your âbindâ function.
>>>
>>>
>>> On 23/10/15 17:24, Dominic Mulligan via Cl-isabelle-users wrote:
>>>>
>>>>
>>>> Hi all,
>>>>
>>>> I have a problem with a development that I am working on (in Isabelle
>>>> 2015).  A slimmed down and simplified version of the problematic code
>>>> has been attached in a dedicated theory file to this e-mail with the
>>>> problem annotated with an (* XXX *) comment.
>>>>
>>>> The problem arises when trying to prove termination of recursive
>>>> functions that follow a fairly natural monadic programming style,
>>>> namely recursively calling your function on a decreasing argument that
>>>> is produced by earlier monadic code, hence lambda-bound following a
>>>> bind.  Here, the termination machinery seems to generate proof
>>>> obligations that are not solveable, demanding one prove that an
>>>> arbitrary list is shorter (according to the measure) than a non-empty
>>>> list, like so:
>>>>
>>>> âxs xa. xs â [] â length xa < length xs
>>>>
>>>> Interestingly, HOL4's termination machinery also seems to behave
>>>> similarly, and with the help of Anthony Fox the issue has been
>>>> reported to Konrad Slind.
>>>>
>>>> Does anybody have any suggestions on how to proceed other than
>>>> completely rewriting all of my monadic code?  The problematic code is
>>>> automatically generated, and comes from a rather large model, so I'd
>>>> rather not have to rewrite everything.
>>>>
>>>> Many thanks for any help proffered,
>>>> Dominic
>>>>
>>>
>




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