hol-theorem-prover/hol

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

This is the distribution directory for the Kananaskis release of HOL4. See http://hol-theorem-prover.org for online resources.

The following is a brief listing of what's available in the distribution.

 INSTALL        * Installation instructions
 COPYRIGHT      * Copyright notice
 std.prelude    * File loaded at the beginning of each HOL session

 bin/           * Executables
 doc/           * Some documentation, including release notes
 examples/      * Some examples
 help/          * Help support
 src/           * The system sources
 tools/         * Support for building the system
 sigobj/        * Collection of all signatures and compiled code

hol's Issues

undocumented conversions

RESORT_FORALL_CONV, RESORT_EXISTS_CONV

MP treats negations as implications

Either MP shouldn't do that or it should be documented more clearly (I haven't found any documentation about it, e.g. in Thm.MP.doc).

Add a ‘while’ constant to state_transformer theory

There is a natural notion of while loop for state monads. With our do notation, you'd like to have it satisfy the following theorem:

while guard body = 
  do 
     gval <- guard;
     if gval then 
        do 
          body;
          while guard body
        od
     else return ()
  od

I think it should be possible to define this in terms of our existing WHILE combinator. Something like

mwhile g b = SND (g (WHILE (FST o g) (SND o b o SND o g)))

#include directive for build-sequence files

This would give us a way to modularise build-sequences into components that could be included or not at a higher level. This would allow us to do away with the special handling of the expk and stdknl options, simply replacing them with appropriate build sequences.

Allow 'raw' option to LaTeX munger commands

This raw option would cause it to print stuff like

!x. P x ==> Q x

rather than the pretty, Unicoded

∀x. P x ⇒ Q x

that would current appear.

This would be useful for documentation purposes.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

More aggressive, mutual simplification of assumptions

FULL_SIMP_TAC only simplifies assumptions with respect to each in one order. It should be possible to simplify all assumptions with respect to all others. Could call this ALL_SIMP_TAC or similar.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Rename READ-ME, Readme etc. to README

[HOL]$ find . -name README|wc -l
82
[HOL]$ find . -name READ-ME|wc -l
18
[HOL]$ find . -name Readme|wc -l
1

For sake of uniformity, alternative spellings of README should be eliminated where possible.

Allow specification of grammar to LaTeX munger commands

E.g., something like

\HOLtm[g=bool]{x + y}

would cause the printing of a term like

arithmetic$+ x y

as the bool grammar has no knowledge of the + constant.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Link to the built-in Poly/ML pretty-printer better

This is currently done in a hackish way, which results in sub-optimal printing of values when embedded in the Poly/ML printing of things like lists. The PPBackEnd technology may make this easy to do.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Thm.GEN_ABS undocumented

STRIP_QUANT_CONV unexpected behaviour

> val c = let open Canon in NNF_CONV NO_CONV true THENC PROP_CNF_CONV end;

> t';
val it =
   ``∀y. ∃x. ∀x'. x ∧ y ∨ (y ⇒ x')``:
   term

> (STRIP_QUANT_CONV c) t';
val it =
   |- (∀y. ∃x. ∀x'. x ∧ y ∨ (y ⇒ x')) ⇔ ∀y. ∃x. ∀x'. x ∧ y ∨ x' ∨ ¬y:
   thm

> t'';
val it =
   ``x ∧ y ∨ (y ⇒ x')``:
   term

> c t'';
val it =
   |- x ∧ y ∨ (y ⇒ x') ⇔ (x ∨ x' ∨ ¬y) ∧ (y ∨ x' ∨ ¬y):
   thm

Shouldn't the rhs above be the same as the body in the result of STRIP_QUANT_CONV?

Testing Framework

An automated regression testing framework for HOL4, with a decent (web) interface and report generation.

Daily build reports by e-mail are nice, but (e.g.) Isabelle's Mira testing framework (http://isabelle.in.tum.de/reports/Isabelle/) is nicer.

Implement Coq-style goal-matching tactic

An “ltac” is perhaps of the form

([hyppat1, hyppat2, ...], goalpat, 
 (fn ([matchvar1, matchvar2, ...], [hypth1, hypth2, ...], goalterm) => tactic))

where the hyppat and goalpat are terms that are matched against the goal. The instantiation is obviously kept from one match to the next. If a goal matches the provided function is called, and passed the instantiations for the matches (in the order they appear) as well as theorems corresponding to the matched hypotheses. (Should the matched hypotheses be removed from the hypotheses? Maybe; the user can always put them back.)

E.g.,

([`P ==> Q`, `P`], `goal`, (fn (_, [imp, a], _) => ASSUME_TAC (MP imp a)))

would be a bit like a RES_TAC, but which only eliminated one literal pair.

WIth a bit of care over the matching, a matching version would also work:

([`!x. P x ==> Q x`, `P v`], `goal`, (fn (_, [imp, a], _) => ASSUME_TAC (MATCH_MP imp a)))

(The code would have to instantiate subsequent patterns and β-reduce them.)

There are clearly all sorts of usability tweaks that might be added to this.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Implement “smart quotes” for docfiles

Currently we have to use back-quotes for “ and double-apostrophes for ” in order to make the LaTeX manuals work. Thus we get stuff like

This is a sentence with ``scare quotes''.

This results in ugly text in non-LaTeX places. Better would be to use normal quotes, and to then convert them as appropriate depending on the destination format. In fact, everywhere except LaTeX could use the Unicode characters. I don’t know if LaTeX supports Unicode quotation characters, though it might.

Allow non-constructor constants as function arguments

It would be nice if the following worked:

Define x = 1;
Definition has been stored under "x_def"
val it = |- x = 1: thm
Define f x = x;

Exception raised at TotalDefn.Define:
on line 2, characters 8-14:
at Defn.prim_mk_defn:
at Functional.mk_case:
Some patterns are not constants or variables
Exception-
HOL_ERR
{message =
"on line 2, characters 8-14:\nat Defn.prim_mk_defn:\nat Functional.mk_case:\nSome patterns are not constants or variables",
origin_function = "Define", origin_structure = "TotalDefn"} raised

Move web-site pages onto github

As per the subject line.

normalForms.CNF_CONV broken

Surely it shouldn't be introducing variables of types higher than bool?

> t;
val it =
   ``∃(x :bool). ∀(y :bool). ∃(z :bool). x ∧ y ∨ x ∧ ¬z ∨ y ∧ z``:
   term
> normalForms.CNF_CONV t;
val it =
   |- (∃(x :bool). ∀(y :bool). ∃(z :bool). x ∧ y ∨ x ∧ ¬z ∨ y ∧ z) ⇔
   ∃(x :bool) (z :bool -> bool).
     ∀(y :bool).
       (y ∨ ¬z y) ∧ (x ∨ ¬z y ∨ y) ∧ (x ∨ y) ∧ (y ∨ x) ∧ (x ∨ z y) ∧
       (y ∨ x ∨ z y):
   thm

Let and case parsing precedence

The following doesn't type check:

case x of [] -> let y = 1 in y || a::b -> 2

but this one does:

case x of [] -> (let y = 1 in y) || a::b -> 2

A quick look at the term grammar made me think that the precedences could be tweaked to make the top example work without harming anything else by moving "let" from to between "||" and "and", but I'm far from expert in this part of the system.

Help documentation should be “opt out”

From Tjark @ Sourceforge:

Currently, help/src-sml/Keepers.sml contains "a list of the signatures that we think users will be interested in." In my humble opinion, the current list is too restrictive. It would be much easier to skim over some uninteresting entries in the documentation than it is to find (or even become aware of) things that are not documented at all. Personally, I found a hacked Keepers.sml that simply documents all signatures much more useful than the current one.

In any case, the current implementation by default does NOT include signatures unless they are explicitly added to Keepers.sml. I think this can be surprising to new developers (it certainly was to me), and it means that additional work (namely editing Keepers.sml) is necessary to have your signatures included in the documentation. Given that most signatures should be interesting to some users, and that there usually tends to be too little rather than too much documentation, I think this is probably not a very wise choice. I would prefer an approach that documents all signatures unless they are mentioned in some blacklist - i.e., an opt-out approach rather than the current opt-in one.

Document CONJ_ASM{1,2}_TAC

As per subject-line.

bin/build silently does nothing if called from wrong dir

If it is trying to use a build-sequence file from an earlier build command, but the path given for the build sequence was relative, then it does nothing if you don't call from the same place. More generally, should it at least say something when the build-sequence file is missing?

Tutorial chapter 3 needs cleanup

Attempting to run through the code in the session boxes reveals places where things need open-ing before they will actually work. No doubt this is a throwback to HOL88 which would have just auto-loaded many identifiers as necessary.

HOL munger should not translate inside LaTeX comments

The built-in lexer should know when it has just passed over a %... On the other hand, having to spot that it's inside a verbatim type environment is a very hard prospect.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Build generates too many warnings

From Tjark @ Sourceforge

Building HOL4 generates a number (25, to be precise) of warnings on my machine. These are related to the parsing of numerals (22), overloading resolution (1), and EmitML's type info (2):

<<HOL warning: parse_term.term_parser:
 0 treated specially and allowed - no other numerals permitted>>
<<HOL warning: Preterm.remove_overloading: many overloaded symbols in term: overloading resolution might take a long time.>>
<<HOL warning: EmitML.datatype_silent_defs: No info in the TypeBase for "int">>

In my opinion, a warning (in contrast to a message) should alert the user to a potential problem. So if there is a potential problem with the calls that generate these warnings, the code should be fixed; if there isn't, the warnings should be disabled explicitly.

In any case, a default build of HOL4 in my humble opinion should not produce any warnings if everything goes according to plan.

PairCases_on is undocumented

There is not even a helpful comment in the sig file (which is what you get from help "PairCases_on").

Tutorial refers to non-existent files

The tutorial claims that there are solutions to the parity example's exercises in

hol/examples/parity/RESET_{REG,PARITY}.sml .

These files do not exist.

Better error messages on Poly/ML faults

From Tjark @ Sourceforge

When building HOL4 with Poly/ML, messages generated by the Poly/ML compiler refer to temporary files (see the output below for an example). It would be more helpful to see the original filename (in this example, src/integer/integerScript.sml).

Building directory src/integer [29 Sep, 18:53:46]
Linking integerScript.uo to produce theory-builder executable
Poly/ML 5.4 Release
> Warning- in '/tmp/MLTEMPvP9QkE', line 101.
Pattern is not exhaustive.
Found near val [eqop, binop] = map (... o ... o concl) [hd lcthms, sym]

Nice hierarchical record update syntax.

It would be nice to be able to write

r1 with r2.fld := 3

where the thing following with is a field-name path. (Suggested by Konrad.)

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

pp_overloads_on etc. undocumented

There are about 20 entry points in Parse to do with abbrevs and overloads that are undocumented. They're in 1 or 2 families, though, so it's probably best to write just a couple of document files and then heavily cross-reference... I guess there's not much support for that apart from \SEEALSO.

case pretty-printing bug

case x of (a,b) => 1;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = case x of | (a,b) => 1: term

but a leading | isn't allowed in the input (although I think it should be).

Allow word_or to be overloaded with "||"

Paper reviewers scoff at our use of "!!" for bitwise-or. "|" causes problems with set-comprehensions and "||" causes problems with case-statmements. Smarter case-split magic could possibly free up "||"? At the moment we get:

overload_on ("||", word_or);

a || b && c : word32;
<<HOL message: inventing new type variable names: 'a, 'b>>

Type inference failure: unable to infer a type for the application of

case_split__magic (a :α -> β)

roughly on line 3, characters 2-14

which has type

:(α -> β) -> α -> β

to

(b :bool[32]) && (c :bool[32])

roughly on line 3, characters 7-14

which has type

:bool[32]

unification failure message: unify failed

New syntax for function-valued fields

From Steve Brackin @ Sourceforge:

Translate

<| fld1 x y := E1(x,y); fld2 z := E2(z) |>

to

fldl_fupdate (K (λx y. E1(x,y))) (fld2_fupdate (K (λz. E2(z))) ARB)

The idea is to save the user from having to think in terms of lambda expressions and beta reductions.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

ARITH_CONV performance on natural number subtraction

The performance can be very bad because of unnecessary case-splitting.

x - PRE i - SUC (PRE i - PRE i) = 0.

Here, for example, there should be just one split on (i = 0), not three. (This is not a statement the system should be proving, incidentally, but it still takes inordinately long to fail.)

Allow pattern-overloading to work with paired abstractions

When parsing, the system doesn't do a paired β-reduction, and when printing, it doesn't recognise the term as an abstraction, and so fails to do any useful pattern-matching.

Organise traces hierarchically

Now there are so many traces, the output provided by traces() is confusing. I think it would be an improvement to group traces into related areas.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Handle paired-abstractions better

In particular, if there is a quantifier over a variable of pair type, and that same variable is an argument to a paired abstraction, then the quantifier should be rewritten to pick up the abstraction's names, and the abstraction should be β-reduced.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Check crypto/serpent/reference on poly5.3

Apparently this directory builds OK with Poly5.4. I should check that it really continues to fail with 5.3. If it does we may need to enrich the syntax of the build-sequence file so that we can specify multiple ML implementations and ML+specific version information.

Add wildcard function to Holmake

Documented at http://www.gnu.org/s/hello/manual/make/Wildcard-Function.html

Replace link to SourceForge tracker with GitHub tracker in file INSTALL

As per the subject line.

Allow Holmake's default target to just be the first target in a makefile

At the moment, if you just type a bare Holmake it tries to do all of its built-in automatic things, as well as the first target in the makefile. It might be useful to turn this off so that the bare command only attempts to build the first target.

I guess an extra string in the OPTIONS = line could enable this.

Holmake to build LaTeX (with HOL inclusions)

Holmake should be able to build latex files into PDFs. It should handle "easy" cases well (single source file with embedded images and bibliographies), and should certainly support .htex files that need passing through a munger of some sort.

Fix Induct_on for mutually/nested recursive types

Example problem:

val _ = Hol_datatype `ptree = Leaf of 'ts | Node of 'nts => ptree list`
val ptsize_def = Define`
   (ptsize (Leaf t) = 1) /\
   (ptsize (Node nt ps) = ptsizel ps + 1) /\
   (ptsizel [] = 0) /\
   (ptsizel (p::ps) = ptsize p + ptsizel ps)
`
val ptsize_gt0 = prove(
   ``!t. 0 < ptsize t``,
   Induct_on `t` (* raises exception *)
);

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

ifdef/ifndef/ifeq for Holmakefiles

This facility would allow for things like:

ifdef POLY
heap: heap_deps
             $(protect $(HOLDIR)/bin/buildheap) -o $@ thy1 thy2...
endif

Currently, so that mosml doesn't get all confused, you have to do vaguely horrible things with nested variable references (see the Holmakefile in examples/computability/lambda).

HolQbf Library Documentation Needs Update

The description of the HolQbf library (in HOL/Manual/Description/HolQbf.tex) is outdated. In particular, Ramana's recent work on conversion of QBF into prenex normal form is not documented yet.

Provide good indication of all constants’ real names and types

show_types works tolerably well for indicating the types of variables and some constants. But when a constant is involved in a special syntactic form (typically an infix) or is overloaded polymorphically, the user gets nothing back at all. For example,

- load "integerTheory";
- show_types := true;
- ``x + y``;
> val it = ``(x: int) + (y:int)`` : term

No indication that + is really int$+, though it's easy enough (given knowledge about the theories) to see that this is so. With show_types on,

- ``LENGTH``;
> val it = ``(LENGTH : α list -> num)`` : term

(good). But also:

- Define`SUC (n:int) = n + 1`;
> val it = |- ∀(n :int). SUC n = n + (1 :int) : thm

(bad) and

- ``SUC``;
<<HOL message: more than one resolution of overloading was possible>>
> val it = ``SUC`` : term

(also bad).

For the last example, I'd like to see

``SUC : int -> int``

as this case isn't.

Worse, I'm not sure what the output should be in the following scenario. Just annotating the SUC with its type is not sufficient:

- Define`SUC (n:num) = n - 1`;
Definition has been stored under "SUC_def"
> val it =
   |- ∀(n :num). SUC n = n − (1 :num) : thm

- ``SUC x``;
<<HOL message: more than one resolution of overloading was possible>>
> val it = ``SUC (x :num)`` : term

- dest_term (rator it);
> val it =
   CONST
    {Ty = ``:num -> num``,
     Thy = "scratch", Name = "SUC"} : lambda

Syntax for list comprehensions

Support syntax for list comprehensions along the lines of

[ x + 1 | x <- somelist, x < 10]

which would draw x values from list somelist, throw out those not less than 10, and then add one to the result.

The code should be generic enough to allow similar syntax (perhaps with [[ and ]]) for lazy lists.

The above would translate to

MAP (λx. x + 1) (FILTER (λx. x < 10) somelist)

and the pretty-printer would have to spot terms like the above and print the list-comprehension form. Note that even

MAP (λx. x + 1) list

is shorter (count the characters) when you write it as a list comprehension:

[ x + 1 | x <- list ]

(Note that the pretty-printer wouldn't attack something like MAP f list because there isn't an abstraction as the first argument to MAP.)

If two lists are drawn from, then you need some sort of MAP_FLAT constant, of type :(α -> β list) -> α list -> β list. This would then allow

[ x + y | x <- list1, y <- list2, x < 10, y <> x ]

to turn into

MAP_FLAT (λx. MAP (λy. x + y) (FILTER (λy. x < 10) (FILTER (λy. y <> x) list2))) list1

Note the weirdness of the FILTER (λy. x < 10); this will filter the list list2 by something that is either true or false in the context of a particular x.

If list1 = [11;2;5;6] and list2 = [2;3;4] the result of the above is [5; 6; 7; 8; 9; 8; 9; 10].

The similar comprehension

[ x + y | x <- list1, x < 10, y <- list2, y <> x ]

gives the translation

MAP_FLAT (λx. MAP (λy. x + y) (FILTER (λy. y <> x) list2)) (FILTER (λx. x < 10) list1)

which has the same semantics.

(See the Scala book (Odersky, Spoon and Venners) for discussion of this translation.)

As Scott pointed out in Nijmegen, it would be nice to be able have patterns on the lhs of the binding <-. This would allow something like

[ f x | SOME x <- list ]

so that only particular types of values need to be considered. I'm not so sure how this should be translated.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Provide in-system documentation for traces

When getting a list of traces, the user should also get short descriptions of what each trace is for. The name of the trace shouldn't attempt to be this description. Developers setting up traces can provide the docstring as part of the call to register_trace.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

printing of 'if' still not ideal

This doesn't print as nicely as I'd like. In particular, the leaves get put onto new lines of their own.

if i < lim then n2s i
else if i <= n then n2s (i + 1)
else if i = n + 1 then n2s lim
else n2s i

Reinstate Reference Manual's list of theorems

The Reference manual used to include a big list of the core system's theorems. I found this useful when I was learning HOL, so perhaps we should try to do this again. It's not clear if we'd really want to list all theorems, even for just the core theories, but I guess a tool that included all theorems from specified theories except for ones that a developer somehow flagged as 'uninteresting' would be the way to go.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

Update web pages to mention/link to GitHub instead of SourceForge

As per the subject line.