[isabelle] Common monadic programming idioms and termination

Discussion:

(too old to reply)

Manuel Eberl

2015-10-23 15:55:31 UTC

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.

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
⋀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

Dominic Mulligan via Cl-isabelle-users

2015-10-23 15:56:33 UTC

Permalink

Hi Manuel,

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

Dominic

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
"(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.

Andreas Lochbihler

2015-10-27 12:28:01 UTC

Permalink

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

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

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
"(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.

Dominic Mulligan via Cl-isabelle-users

2015-10-27 12:45:57 UTC

Permalink

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

Post by Andreas Lochbihler
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

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
"(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.