[opentheory-users] standard library requests

[Joe Hurd]

Hi Ramana,

I'm afraid to say that the theorems currently in the standard theory
library are rather random. I actually have a more recent version of
the standard library where the situation is slightly improved, but
before making changes I would definitely appreciate hearing the
opinions of people on this list about their preferred style of
theorems. I'm sure there will be many dissenting voices, but it would
be good to make use of whatever consensus currently exists.

For example, your first request rang a warning bell for me:

> |- ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)

I make extensive use of MATCH_MP_TAC when I am theorem proving, and so
have a strong preference for theorems of the form

|- !x_1 ... x_m. P_1 /\ ... /\ P_n ==> Q

rather than the nested implications in your example. Being consistent
about such stylistic matters will also help promote composibility of
theories.

Another point I'm unsure about: is it good style to avoid top-level
conjunctions in theorems, like so?

|- C1 /\ ... /\ Cn

Packing theorems together like this definitely makes it harder to work
with the individual conjuncts, but this is a common style for "AC
theorems"

|- (!x y. x + y = y + x) /\ (!x y z. x + (y + z) = (x + y) + z)

or definitions

|- length [] = 0 /\ (!h t. length (h :: t) = suc (length t))

> The first of these I think should simply be in the bool package. Is it
> there already? It's hard to search the list of theorems.

You're quite right that it's hard to search through the theorems. One
day I'd love to see a "hoogle"

http://www.haskell.org/hoogle/

for higher order logic theorems (thoogle?).

> Arguably I
> ought to make a new version of the bool package that proves that
> theorem and .. submit it somewhere? Doing so would be a good test of
> the tool chain. What do you imagine would be the easiest way to do
> that, anyway?

Submitting a new theory involves the following steps:

1. Exporting a HOL4 theory to OpenTheory format.

2. Installing the new theory:

opentheory install THEORY.thy

3. Uploading the theory to the repo:

opentheory upload THEORY-1.0

However, you can't simply "take over maintenance" of a theory by
uploading a new version (you need the permission of the current
maintainer). It might be best to start by uploading a new theory that
doesn't already exist.

> |- TYPE_DEFINITION =
>   (λP rep.
>      (∀x' x''. (rep x' = rep x'') ⇒ (x' = x'')) ∧
>      ∀x. P x ⇔ ∃x'. x = rep x')
>
> The second theorem I wouldn't expect to go into the standard library
> because it's basically an ad hoc constant definition to package up
> type definitions in HOL4. However, it is the kind of theorem I imagine
> being present in a "compatibility package" sitting between HOL4
> theories and the standard library. Apart from a compatibility package,
> or from simply defining TYPE_DEFINITION at the start of every HOL4
> theory package, what other options are there for this theorem (and
> others like it)?

When exporting from HOL Light I was faced with the problem of what to
do with similar auxiliary definitions. To start with I made a
"compatibility layer" theory that contained these definitions and also
the auxiliary theorems, but it was too big and ugly to maintain. So
now I simply redefine and reprove the auxiliary constants and theorems
inside each theory that uses them.

Cheers,

Joe