Defining multiple independent functions in the same definition block.

[Eric-C-Hall]

It would be good to be able to tell HOL to allow you to define multiple independent functions in one definition block without it complaining, because this would make it easier to debug when you are defining mutually recursive functions, if, for example, you want to write it one part at a time instead of all at once, or if you want to comment out parts of it to see which parts of the definition are broken. It will mean you will not have to correctly define the entire set of possibly many functions correctly all at once.

The default should be for HOL to complain, because this will avoid bugs where recursion is not happening where recursion is expected, but it would be good to disable HOL's complaints.

Maybe use the attribute [multi] to indicate that it is ok to define multiple functions in the same block.

[konrad-slind]

Hi Eric,

There is multiDefine, invoked as follows:

TotalDefn.multiDefine f x = x+1 /\ g y = y + 2;

Definition has been stored under "g_def"

Definition has been stored under "f_def"

val it = [⊢ ∀y. g y = y + 2, ⊢ ∀x. f x = x + 1]: thm list

This hasn't yet been incorporated into the Definition ... End syntax. Note that multiDefine is intended to handle a collection of independent definitions. It is allowed to have some of the definitions be recursive, and even mutually recursive, but termination will have to be auto-proved for all of them.

Re: how to develop complex mutually recursing functions. I often resort to replacing parts of the definitions with ARB in order to get the typechecking sorted out, then go back and replace the ARBs one by one with the intended recursive calls.

Konrad.

On Wed, Oct 16, 2024 at 10:22 PM Eric Hall @.***> wrote:

It would be good to be able to tell HOL to allow you to define multiple independent functions in one definition block without it complaining, because this would make it easier to debug when you are defining mutually recursive functions, if, for example, you want to write it one part at a time instead of all at once, or if you want to comment out parts of it to see which parts of the definition are broken. It will mean you will not have to correctly define the entire set of possibly many functions correctly all at once.

The default should be for HOL to complain, because this will avoid bugs where recursion is not happening where recursion is expected, but it would be good to disable HOL's complaints.

Maybe use the attribute [multi] to indicate that it is ok to define multiple functions in the same block.

— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1324, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD34ZOOR7TSYBJ3PX5TZ34UO7AVCNFSM6AAAAABQCYUK4GVHI2DSMVQWIX3LMV43ASLTON2WKOZSGU4TGNJQGI4DIMY . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[Eric-C-Hall]

That sounds good! I'll have to check it out next time I need to write a recursive function. Would be good to have it incorporated into the Definition ... End syntax.

[Eric-C-Hall]

I, too, like to replace parts of my definition with ARB to ensure that the rest of the definition is being type-checked correctly, and then fill in the ARBs later. However, when attempting to do this in mutually recursive functions, if you replace the mutually recursive call with an ARB, then the function becomes no-longer-mutually-recursive, and HOL complains because you can't have multiple definitions in a non-mutually-recursive definition block.

Now that I think about it, though, in the case that this happens, it is possible to split the definition up into multiple single definitions, and work with those. However, this is needlessly labour-intensive, if you're going to have to combine the definitions again when they become mutually recursive, anyway.

[konrad-slind]

Good point. IMO, a logic environment should almost have a separate interface for constructing well-formed (and typed) terms. Right now, comprehending type errors, fixing them, and re-submitting can be onerous on large definitions and terms.

Konrad.

On Wed, Oct 16, 2024 at 11:39 PM Eric Hall @.***> wrote:

I, too, like to replace parts of my definition with ARB to ensure that the rest of the definition is being type-checked correctly, and then fill in the ARBs later. However, when attempting to do this in mutually recursive functions, if you replace the mutually recursive call with an ARB, then the function becomes no-longer-mutually-recursive, and HOL complains because you can't have multiple definitions in a non-mutually-recursive definition block.

Now that I think about it, though, in the case that this happens, it is possible to split the definition up into multiple single definitions, and work with those. However, this is needlessly labour-intensive, if you're going to have to combine the definitions again when they become mutually recursive, anyway.

— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1324#issuecomment-2418482100, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOADZE6KJP7MQISOZOHSTZ345PRAVCNFSM6AAAAABQCYUK4GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMJYGQ4DEMJQGA . You are receiving this because you commented.Message ID: @.***>