[isabelle] Help defining a mutually recursive function

[Corey Richardson]

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.

[Lars Hupel]

Hi Corey,

Post by Corey Richardson
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.

Post by Corey Richardson
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

[Corey Richardson]

Post by Lars Hupel
Hi Corey,

Post by Corey Richardson
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!

Post by Lars Hupel

Post by Corey Richardson
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).

Post by Lars Hupel
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!