Re: [isabelle] Common monadic programming idioms and termination



Hi Manuel,

Thanks for your help.  The fundef_cong attribute is what I had been missing!

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.