[opentheory-users] extending the standard library

[Joe Leslie-Hurd]

Hi Ramana,

Thanks for taking the time to synchronize the discussion.

> On creating theories in the HOL4 namespace, and depending on the hol-base
> package: I see these as interim measures, with my desired goal being that
> the
> theorems and additional constants eventually all make it into the standard
> namespace and depend on a nicely organised, unified, tree of packages. I
> think
> we probably agree on that goal, but I'm not sure. What do you say?

Yes, I agree. I see the HOL4 namespace and the hol-base package as a
convenient place to put HOL4-specific theories while we decide what
will be the highest value to port to the "nicely organised, unified,
tree of packages" depending only on the standard theory library.

> More generally, my goal is to put together OpenTheory packages that are so
> compelling in their organisation and coverage, having taken theorems from
> all
> the existing HOL provers, that everyone wants to use them. I want to move
> towards unification and away from fragmentation. I would be sad if
> OpenTheory
> simply becomes a mirror of the existing fragmentation and incompatibility
> between the various theorem prover libraries today. Do you agree with this
> more
> general goal?

Agreed also, which is somewhat motivating my resistance to including
totalized constants (see below).

> I would like to discuss how to achieve the HOL4-specific goal now, because I
> think we have enough information to make progress on such a discussion
> (enough
> HOL4 packages are already created). (This is in response to "When the HOL4
> theory packages are in place...".)

OK sure, let's now discuss moving HOL4 packages away from their
holding station in the HOL4 namespace depending on the hol-base
package.

> Now back to the questions from my previous email:
>
>  - Do you agree with the three pieces of my solution to issue (2)? How do
> you
>    think responsibility for those tasks should be divided between readers
> and
>    creators?

For issue (2) I was only considering the case where native and
OpenTheory constants have different but isomorphic types, such as zip
which might be defined as either of

A list * B list -> (A * B) list
A list -> B list -> (A * B) list

If this is the only difference we can provide an unconditional
equation between the OpenTheory and native variants of these
constants. I agree with your three pieces of the solution, and I would
hope that the theory creator could handle all of them so the reader
would not have to know about the native constant with the different
type.

Actually, this is not strictly true, since reading such a theory might
involve defining the HOL4 variant of the constant (just as reading the
real theory involves defining some symbols in the HOLLight namespace),
but I am ok with generating a bit of name pollution in logical kernels
that are not purely functional. [This can already happen when
auxiliary definitions are made to support definitions and proofs.]

>  - I guess your response "I'm loath to totalize any of the constants..." was
>    mainly to my suggested solution 0 to issue (3). That is a reasonable
>    objection to solution 0.
>    But:
>    What do you think of solution 1, namely, providing multiple versions of
>    constants that can be overspecified (in addition to the underspecified
>    version), together with theorems relating them?

I've thought a lot about this, and am still not sure about adding
totalized constants to OpenTheory theories that are intended to be
read into arbitrary environments. For a concrete case, let's consider
defining the HOL4 real inverse function:

|- !x. inv0 x = if x = 0 then 0 else inv 0

This makes it clear that when the argument can be proved to be
non-zero, then inv0 and inv are interchangeable.

The problem is that if I add inv0 to the real theory, then it has no
binding in an environment that doesn't contain that totalized
constant. And similarly the theorems about inv0, such as

|- inv0 0 = 0

don't have any equivalents in this environment. So we'd essentially be
asking this environment to define inv0 and prove these theorems,
because they'd be used in the proof of other theorems not involving
inv0.

In general each environment would have to define each variant of
totalized constants, and maintain them as visible symbols with
searchable theorems about them.

The alternative I'd prefer would be for the native symbols to be
hidden inside theories (HOL4.inv instead of inv0), just as in the case
of native symbols with different types, which would require their
properties to be proved each time inside theories that use them
instead of being proved once and exported (static linking instead of
dynamic linking).

This focus on minimizing the work of the reader admittedly maximizes
the burden on theory creators, but at least it avoids each environment
needing to define and maintain properties of constant variants from
other environments. In the extreme case of purely functional logical
kernels then variants of constants from other environments just exist
transiently to support proofs and are otherwise completely invisible.

Cheers,

Joe