[opentheory-users] Questions about the standard library packages

[Joe Hurd]

Hi Ali,

> I am working on a translation from OpenTheory to Dedukti
> (http://www.lix.polytechnique.fr/dedukti/), a proof system close to the LF
> and Coq family. I have some questions regarding the packaging of some
> theories in the standard library.

Sounds cool - I'd be happy to see an interchange of theories between
the HOL family and Dedukti.

> 1. Our biggest obstacle right now is inductive type definitions. It turns
> out it is very expensive to type-check the complex machanisms of inductive
> type definitions the way they are currently implemented in HOL (and hence in
> OpenTheory). However, these mechanisms are hidden in the packages that use
> them (e.g. in list-def, option-def, sum-def) and therefore reappear in each
> of them, resulting in bloated packages. Is there any reason why inductive
> type definitions have not been formalized in a separate package, on which
> the theories using them (list, option, sum, etc.) depend on?

This is the difference between "static linking" of one theory within
another (as is currently the case in these theories) and "dynamic
linking" (carving out a common theory that they depend on). Just as
with software, there are advantages and disadvantages to both methods
of linking:

Static linking: fewer dependencies to manage; no re-use possible.

Dynamic linking: must construct out a clean common theory that lives
in the standard namespace; can re-use to create more compact theories
that depend on it.

Right now no one has expended the effort to carve out a clean theory
of inductive definitions, so it is in the default state of being
statically linked into any theory that uses them.

> 2. Why are some constant definitions hidden (e.g. the empty list [] and the
> list constructor (::)) while others are not (e.g. boolean connectives)?

There is no special significance of a definition theorem in a theory
export - it is up to the theory author to choose what theorems to
export that refer to constants and type operators defined in a theory.
Since there is very little machinery available to clean up the
definitions made in bool-def, the definition theorems are exported
"as-is". In later theories forms such as

|- !x. c x = tm[x]

are exported rather than the primitive definition form

|- c = \x. tm[x]

for aesthetic reasons.

> 3. The packaging of real numbers is a bit odd. It is only split in two, very
> unbalanced packages, real-def and real-thm, and most of the theory is
> squeezed into the first one, resulting in a huge monolithic package (compare
> this to the theory of natural numbers). Is this intended or is it still a
> work in progress?

This is most definitely a work in progress. real-thm currently just
has a couple of trivial theorems in it, while real-def contains the
entire HOL Light construction of the real numbers from the natural
numbers, resulting in quite a big theory:

$ opentheory info --inference real-def
Primitive inferences:
eqMp ............ 11,710
subst ............ 9,691
appThm ........... 8,985
deductAntisym .... 5,501
refl ............. 3,469
absThm ........... 1,829
betaConv ......... 1,596
assume ............. 428
axiom .............. 151
defineConst ......... 36
defineTypeOp ......... 3
Total ........... 43,399

Cheers,

Joe