Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help defining a mutually recursive function

Email Gateway (Aug 22 2022 at 14:17):

From: Corey Richardson <corey@octayn.net>
Greetings,

In a theory I'm working on, I'm having challenges defining a mutually
recursive function.

Here's the repository and the particular function:

https://gitlab.com/cmr/rust-semantics/blob/unsigned/MIR_SimpleEvals.thy#L38

I think I need to prove that read_array does not make a larger "t" for
the higher-order function passed in. I'm not sure how to do this either.

pat_completeness auto also doesn't show completeness of the pattern
matches, which I do not understand. They seem complete to me at least!

I also suspect I'll need some congruence rule for read_array, but even
after studying examples of congruence rules from the functions.pdf and
the Isabelle libraries, I'm not sure what it should be.

Thanks for any help.
signature.asc

Email Gateway (Aug 22 2022 at 14:18):

From: Lars Hupel <hupel@in.tum.de>
Hi Corey,

let's start with the simple question:

pat_completeness auto also doesn't show completeness of the pattern
matches, which I do not understand. They seem complete to me at least!

They are overlapping as you have written them down. As opposed to "fun",
"function" by default does not consider pattern matches to be
sequential. That is, your sixth equation matches everything the others
matched, too. The fix is easy: use "function (sequential)" instead, and
"pat_completeness auto" will solve it.

I think I need to prove that read_array does not make a larger "t" for
the higher-order function passed in. I'm not sure how to do this either.

I also suspect I'll need some congruence rule for read_array, but even
after studying examples of congruence rules from the functions.pdf and
the Isabelle libraries, I'm not sure what it should be.

"read_array" looks complicated, because the calls of the callback
function look quite irregular. Have you tried inlining the definition of
"read_array", i.e. remove the callback and define it as part of the
mutual bundle?

(In my personal experience, while this complicates some proofs because
of the now three-way-mutual definition, it greatly simplifies some others.)

Also, the "Option.bind ... (Some o ValArray)" looks suspicious. Why are
you "bind"ing if you're always feeding in a "Some"?

Cheers
Lars

Email Gateway (Aug 22 2022 at 14:19):

From: Corey Richardson <corey@octayn.net>
On 2016-10-06 5:29, Lars Hupel wrote:

Hi Corey,

let's start with the simple question:

pat_completeness auto also doesn't show completeness of the pattern
matches, which I do not understand. They seem complete to me at least!

They are overlapping as you have written them down. As opposed to "fun",
"function" by default does not consider pattern matches to be
sequential. That is, your sixth equation matches everything the others
matched, too. The fix is easy: use "function (sequential)" instead, and
"pat_completeness auto" will solve it.

Ah, that's simple. Thanks!

I think I need to prove that read_array does not make a larger "t" for
the higher-order function passed in. I'm not sure how to do this either.

I also suspect I'll need some congruence rule for read_array, but even
after studying examples of congruence rules from the functions.pdf and
the Isabelle libraries, I'm not sure what it should be.

"read_array" looks complicated, because the calls of the callback
function look quite irregular. Have you tried inlining the definition of
"read_array", i.e. remove the callback and define it as part of the
mutual bundle?

(In my personal experience, while this complicates some proofs because
of the now three-way-mutual definition, it greatly simplifies some others.)

I was avoiding it for the complication you mention. Adding it as another
mutually recursive function indeed makes all my problems go away (for now).

Also, the "Option.bind ... (Some o ValArray)" looks suspicious. Why are
you "bind"ing if you're always feeding in a "Some"?

I was using it as a poor-man's map_option, before I noticed that
map_option existed! I was looking for Option.map and my search for
constants used "'a option => ('a => 'b) => 'b option" instead of the
other way around for the arguments.

Thanks Lars!
signature.asc

Last updated: Apr 26 2024 at 01:06 UTC