Use kernel compute feature in HOL4 simplifier, decision procedures, and EVAL

[myreen]

I’m planning to make the HOL4 simplifier, decision procedure, and default EVAL set up use the new compute primitive for (at least) any computations over constant natural numbers. This way users will benefit from the new compute primitive (e.g. faster arithmetic decision procedures) without doing anything.

Background: HOL4’s kernel now includes a compute primitive (see merged PR and this ITP’23 paper). The new primitive can do fast computation over natural numbers and Lisp-like first-order functional programs. Note that the primitive does not extend the HOL logic in any way. The compute primitive has been proved to follow the inference rules of higher-order logic (as formalised for Candle). More specifically: @oskarabrahamsson has proved in HOL4 that, for every theorem produced by the new compute primitive, there is some syntactic derivation of that theorem in HOL.

We should discuss a conflict between HOL4's new compute primitive and proof export with OpenTheory. More specifically: What should we do about the OpenTheory exporter? Just to be clear: once simp (and friends) use the new compute under the hood it will part of every development, but the OpenTheory exporter won’t know how to record its computation as OpenTheory primitive inferences.

Here are some options: (1) have a global flag that turns on or off the use of compute in simp, EVAL, DECIDE, or (2) use “ifdef” like hackery to remove all calls to the new compute primitive when building for the OpenTheory kernel (there is already some such hackery going on in Makefiles/Holmakefiles).

[oskarabrahamsson]

This code will run very often. Maybe it would be worth the effort to go with (2)?

[xrchz]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

[xrchz]

An option to record a standard HOL proof (either of your 1 or 2) is probably good to have too though.

[myreen]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

This is a very good point! An importer could then either try to prove these equations with its evaluation mechanism or just take them as assumptions.

[oskarabrahamsson]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

This is a nice suggestion. There's this thing: https://www.gilith.com/opentheory/article.html#axiomCommand

[binghe]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

This is a nice suggestion. There's this thing: https://www.gilith.com/opentheory/article.html#axiomCommand

A well-shaped exported OT article, when combined all together, should only have 3 very axioms corresponding to the standard HOL theory. The extra assumptions (as axioms) that OpenTheory importers have to prove, if they are too many (e.g. case-by-case arithmetics equations), I feel this will render the entire OT exporting facility less useful. Thus I think simply disabling the new computation primitives for OT kernel, is still the best option.