Latest release

Kananaskis 11

@mn200 mn200 released this Mar 3, 2017 · 1602 commits to master since this release

Kananaskis-11

(Released: 3 March 2017)

We are pleased to announce the Kananaskis-11 release of HOL 4.

New features:

  • We have ported HOL Light’s PAT_CONV and PATH_CONV “conversionals”, providing nice machinery for applying conversions to specific sub-terms.

  • The tactic PAT_ABBREV_TAC (also available in the Q module) can now use patterns that are more polymorphic than the sub-term in the goal that is ultimately matched. (Github issue)

  • We have implemented the rule for constant specification described by Rob Arthan in HOL Constant Definition Done Right.
    The new primitive gen_prim_specification in the kernel is used to implement the new rule, gen_new_specification, and is also used to re-implement new_definition and new_specification.
    We removed prim_constant_definition from the kernel, but kept prim_specification because the new derivation of new_specification uses pairs.
    (Github pull-req)

  • Various commands for moving over and selecting HOL tactics in the emacs mode have been improved.
    We have also added a new command hol-find-eval-next-tactic (bound to M-h M-e by default), which selects and highlights the next tactic in the source text, and then applies it to the current goal in the *HOL* buffer.
    This shortcuts the current idiom, which requires the tactic to be highlighted manually, and then applied via M-h e.
    (The advantage of the latter is that one can select specific tactic sequences to be applied all at once.)

  • Record updates can now be more polymorphic. For example, if one defined

       Datatype`rcd = <| myset : α -> bool ; size : num |>`
    

    one used to get back an update constant for the myset field:

       rcd_myset_fupd : ((α -> bool) -> (α -> bool)) -> α rcd -> α rcd
    

    Now, the same constant is

       rcd_myset_fupd : ((α -> bool) -> (β -> bool)) -> α rcd -> β rcd
    

    One might use this to define

       Define`img (f:α->β) r = r with myset updated_by IMAGE f`
    

    This definition would have previously been rejected. (Github issue)

    This change can cause incompatibilities.
    If one wants the old behaviour, it should suffice to overload the record update syntax to use a more specific type.
    For example:

       val _ = gen_remove_ovl_mapping
                 (GrammarSpecials.recfupd_special ^ "myset")
                 ``λf x. rcd_myset_fupd f x``
    
       val _ = Parse.add_record_fupdate(
             "myset", Term.inst[beta |-> alpha] ``rcd_myset_fupd``);
    
  • PolyML “heaps” are now implemented with its SaveState technology, used hierarchically.
    This should make heaps smaller as they now only save deltas over the last used heap.

Bugs fixed:

  • An embarrassing infinite loop bug in the integration of the integer decision procedures (the Omega test, Cooper’s algorithm) into the simplifier was fixed.

  • Theorems can now have names that are the same as SML constructor names (e.g., Empty). (Github issue)

  • Holmake will now follow INCLUDES specifications from Holmakefiles when given “phony” targets to build on the command-line. (A typical phony target is all.) As in the past, it will still act only locally if given just a clean target (clean, cleanDeps or cleanAll). To clean recursively, you must also pass the -r flag to Holmake. (Github issue)

  • We fixed three problems with Datatype. Thanks to Ramana Kumar for the reports.
    First, Datatype will no longer create a recursive type if the recursive instance is qualified with a theory name other than the current one.
    In other words,

        Datatype`num = C1 num$num | C2`
    

    won’t create a recursive type (assuming this is not called in theory num).
    (Hol_datatype had the same problem.)

    Second, Datatype will handle antiquotations in its input properly (Hol_datatype already did).

    Third, Datatype (and Hol_datatype) allows the definition of identical record types in different theories.

  • Attempts to define constants or types with invalid names are now caught much earlier.
    An invalid name is one that contains “non-graphical” characters (as per SML’s Char.isGraph) or parentheses.
    This means that Unicode cannot be used in the kernel’s name for a constant, but certainly doesn’t prevent Unicode being used in overloaded notation.
    Functions such as overload_on, add_rule and set_mapped_fixity can still be used to create pretty notation with as many Unicode characters included as desired.

  • Loading theories under Poly/ML would fail unnecessarily if the current directory was unwritable.
    Working in such directories will likely cause problems when and if an export_theory call is made, so there is a warning emitted in this situation, but the load now succeeds.
    Thanks to Narges Khakpour for the bug report.

  • The function thm_to_string was creating ugly strings full of special codes (encoding type information) rather than using the “raw” backend.

  • Bare record operations (e.g., rcdtype_field, the function that accesses field of type rcdtype) would occasionally pretty-print badly. (Github issue)

New tools:

  • Holyhammer: A method for automatically finding relevant theorems for Metis.
    Given a term, the procedure selects a large number of lemmas through different predictors such as KNN or Mepo.
    These lemmas are given to the external provers E-prover (1.9), Vampire (2.6) or Z3 (4.0).
    The necessary lemmas in the provers' proofs are then returned to the user.
    Modifications to the kernels to track dependencies between theorems allow predictors to learn from the induced relation improving future predictions.
    The build of the source directory src/holyhammer needs ocaml (> 3.12.1) installed as well as a recent version of g++ that supports the C++11 standard.
    The three ATPs have to be installed independently.
    At least one of them should be present, preferably E-prover (1.9).

    Thanks to Thibault Gauthier for this tool.

  • A principle for making coinductive definitions, Hol_coreln.
    The input syntax is the same as for Hol_reln, that is: a conjunction of introduction rules.
    For example, if one is representing coalgebraic lists as a subset of the type :num → α option, the coinductive predicate specifying the subset would be given as

       val (lrep_ok_rules, lrep_ok_coind, lrep_ok_cases) = Hol_coreln`
         lrep_ok (λn. NONE)
             ∧
         ∀h t.
           lrep_ok t
               ⇒
           lrep_ok (λn. if n = 0 then SOME h else t(n - 1))
       `;
    

    as is now done in src/llist/llistScript.sml.

    Thanks to Andrea Condoluci for this tool.

New examples:

  • A theory of balanced binary trees (examples/balanced_bst), based on Haskell code by Leijen and Palamarchuk, and mechanised by Scott Owens. The type supports operations such as insert, union, delete, filters and folds. Operations are parameterised by comparison operators for comparing keys. Balanced trees can themselves be compared.

  • A formalisation of pattern matches (examples/pattern_matches).
    Pattern matching is not directly supported by higher-order logic.
    HOL4’s parser therefore compiles case-expressions (case x of ...) to decision trees based on case constants.
    For non-trivial case expressions, there is a big discrepancy between the user’s view and this internal representation.
    The pattern_matches example defines a new general-purpose representation for case expressions that mirrors the input syntax in the internal representation closely.
    Because of this close connection, the new representation is more intuitive and often much more compact.
    Complicated parsers and pretty-printers are no longer required.
    Proofs can more closely follow the user’s intentions, and code generators (like CakeML) can produce better code.
    Moreover, the new representation is strictly more general than the currently used representation.
    The new representation allows for guards, patterns with multiple occurrences of the same bound variable, unbound variables, arithmetic expressions in patterns, and more.
    The example provides the definitions as well as tools to work with the new case-expressions.
    These tools include support for evaluating and simplifying them, a highly configurable pattern compilation algorithm inside the logic, and optimisations like detecting redundant rows and eliminating them.

Incompatibilities:

  • The function optionSyntax.dest_none will now unwrap the type of its result, e.g., returning rather than :α option when applied to NONE : α option. This brings it into line with the behaviour of listSyntax.dest_nil. See this github issue.

  • The functions Q.MATCH_RENAME_TAC and Q.MATCH_ASSUM_RENAME_TAC have been adjusted to lose their second arguments (the list of variable names that are not to be bound). For example, applying Q.MATCH_RENAME_TAC `(f x = Pair c1 c2) ⇒ X` ["X"] to the goal

         ?- (f x = Pair C'' C0') ⇒ (f C'' = f C0')
    

    used to result in the renamed goal

         ?- (f x = Pair c1 c2) ⇒ (f c1 = f c2)
    

    where the X in the pattern was ignored.
    The interface now achieves the same end by simply allowing the user to write underscores in the pattern.
    Thus, the tactic would become Q.MATCH_RENAME_TAC `(f x = Pair c1 c2) ⇒ _`.
    Multiple underscores can be used to ignore multiple sub-terms.

    Of course, the qmatch_rename_tac and qmatch_assum_rename_tac names for these tactics in bossLib have changed types as well.
    The new Q.MATCH_GOALSUB_RENAME_TAC and Q.MATCH_ASMSUB_RENAME_TAC (and their lower-case versions) have similar types, without explicit lists of variable names to ignore.

  • The theory state_option was removed.
    The better-developed errorStateMonad theory should be used instead.


Downloads

Kananaskis-10

@mn200 mn200 released this Nov 10, 2014 · 2364 commits to master since this release

Release notes for HOL4, Kananaskis-10

(Released: 10 November 2014)

We are pleased to announce the Kananaskis-10 release of HOL 4.

Contents

New features:

  • Our TUTORIAL and LOGIC manuals are now available in Italian translations. Work on the DESCRIPTION manual is also far advanced. Many, many thanks to Domenico Masini for doing this work.

  • The abbreviation tactics (Q.ABBREV_TAC and others) now handle abstractions as abbreviations better. In particular, if one sets up an abstraction as an abbreviation (e.g., Q.ABBREV_TACf = (λn. 2 * n + 10)``), then the simplifier will find and replace instances not just of the abstraction itself (the old behaviour), but also instances of applications of the abstraction to arguments. For example, given the abbreviation for f above, the simplifier would turn a goal such as `2 * (z + 1) + 10 < 100` into `f (z + 1) < 100`.

  • The MAX_SET function in pred_setTheory is now defined (to have value 0) on the empty set.

  • There is an alternative syntax for specifying datatypes. Instead of the Hol_datatype entry-point, one can also use Datatype, which takes a slightly different syntax, inspired by Haskell. This does away with the use of the (somewhat confusing) of and => tokens.

    For example, one would define a simple type of binary tree with

       Datatype`tree = Lf num | Node tree tree`
    

    If the arguments to a constructor are not just simple types (expressible as single tokens), then they need to be enclosed in parentheses. For example:

       Datatype`mytype = Constr mytype ('a -> bool) | BaseCase`
    

    The Hol_datatype entry-point can continue to be used. However, the LaTeX output of EmitTeX uses the new format, and the various DATATYPE constructors used in the EmitML module take quotations in the new format, rather than the old.

  • The arithmetic decision procedure for natural numbers will now prove slightly more goals by doing case-splits on boolean sub-terms that are not in the Presburger subset. This means that goals such as

       0 < y ⇒ x < x + (if P then y else y + 1)
    

    are now provable.

  • The Vim mode for HOL now supports multiple simultaneous sessions. See its README for details.

  • Many of the standard libraries now provide an add_X_compset : compset -> unit (e.g., add_pred_set_compset) to ease building of custom call-by-name evaluation conversions that don't, like EVAL, include everything in the_compset().

  • Holmake has a new function, wildcard which allows expansion of “glob” patterns (e.g., *Script.sml) into lists of matching filenames.

  • The standard pretty-printer now annotates constants with their types as well as variables. (Note that these annotations are typically only visible by using mouse-over tooltips in the emacs mode.) The annotation also includes the constant’s real name, in the form thy$name, making overloads easier to tell apart.

    For example, this means that it is possible to have integers, reals and numbers all in scope, to write something like MAP (+), and to then see what constants are involved by using the mouse. (See Github issue #39.)

  • Unicode is handled slightly better on Windows systems. By default, the pretty-printer avoids printing with Unicode characters there, but can still parse Unicode input successfully. This is important because many of the examples distributed with HOL use Unicode characters in their scripts (nothing in src/ does). This behaviour can be adjusted by toggling the PP.avoid_unicode trace. On Windows this trace is initialised to true; elsewhere it is initialised to false.

Bugs fixed:

  • Holmake was unnecessarily quiet when it compiled certain SML files.
  • The “munging” code for turning HOL into LaTeX now does a better job of rendering data type definition theorems. (This change is independent of the new underlying syntax described earlier.)
  • Pretty-printers added to the system with add_user_printer weren’t having terms-to-be-printed tested against the supplied patterns (except by the gross approximation provided by the built-in term-net structure). Thanks to Ramana Kumar for the bug report.
  • Character literals weren’t pretty-printing to LaTeX. We also improved the handling of string literals. Thanks to Ramana Kumar for the bug reports.
  • Piotr Trojanek found and fixed many documentation bugs in our various manuals.
  • The remove_rules_for_term and temp_remove_rules_for_term functions tended to remove rules for binders as well as the desired rules.

New theories:

  • A theory of “list ranges” (listRangeTheory). A range is a term written [ lo ..< hi ], meaning the list consisting of the (natural) numbers from lo up to, but not including, hi. The theory comes with some basic and obvious theorems, such as

       MEM i [lo ..< hi] ⇔ lo ≤ i ∧ i < hi
    

    and

       LENGTH [lo ..< hi] = hi - lo
    
  • A new development in src/floating-point, which is a reworking of the theories in src/float. Key differences are listed below.

    1. The data representation:
      • The old ieeeTheory uses a pair :num # numto represent the exponent and fraction widths and a triple:num # num # num to represent sign, exponent and fraction values.

      • The new binary_ieeeTheory makes use of HOL records and bit-vectors. The floating-point type :(α, β) float has values of the form

          <| Sign : word1; Exponent : β word; Significand : α word |>
        

        The fraction and exponent widths are now constrained by the type, which facilitates type-checking and avoids having to pass size arguments to operations.

    2. The new development now supports standard bit-vector encoding schemes. The theory machine_ieeeTheory defines floating-point operations over 16-bit, 32-bit and 64-bit values. For example, the 16-bit floating point operations are defined by mapping to and from the type :(10, 5) float, which is given the type abbreviation :half. Theories for other sizes can be built using machine_ieeeLib.mk_fp_encoding.
    3. There is now syntax support via the structures binary_ieeeSyntax and machine_ieeeSyntax.
    4. Ground term evaluation is now supported for most operations. This can be enabled by loading binary_ieeeLib.
    5. The full development does not build under Moscow ML 2.01, as it makes use of the IEEEReal and PackRealBig basis structures.
  • A theory of “simple Patricia trees” (sptreeTheory). This theory implements a type α sptree, which is a finite map from natural numbers to values of type α. (This type is not really a Patricia tree at all; for those, see the other theories in src/patricia.) Values of type α sptree feature efficient lookup, insertion, deletion and union (efficient when evaluated with EVAL or simplified). Though there is a efficient (linear-time) fold operation, it does not iterate over the key-value pairs in key-order.

New tools:

  • New libraries enumLib and fmapalLib provide representations in pred_set and finite map types of enumerated constant sets and maps as minimum-depth binary search trees. A suitable total order on the set elements (map arguments) must be supplied, with a conversion for evaluating it; assistance with this is provided. The primary objective has been an IN_CONV, and a similar FAPPLY_CONV, operating with a logarithmic number of comparisons, but additional operations such as UNION_CONV, INTER_CONV, and FUPDATE_CONV are included and have reasonable asymptotic running times. A conversion TC_CONV implements Warshall’s algorithm for transitive closure of a binary relation (treated as a set-valued finite map).

Examples:

  • The miniml example has been removed. This work has evolved into the CakeML project. That project’s git repository contains all of the material that was once in the HOL distribution, and, given its continuing evolution, much more besides.

Incompatibilities:

  • In relationTheory, the theorems TC_CASES1 and TC_CASES2 have been renamed to TC_CASES1_E and TC_CASES2_E respectively, where the _E suffix indicates that these are elimination rules. In other words, these theorems are of the form TC R x y ⇒ .... This has been done so that new equivalences can be introduced under the old names. For example, TC_CASES1 now states

       TC R x z ⇔ R x z ∨ ∃y. R x y ∧ TC R y z
    

    This change makes the naming consistent with similar theorems RTC_CASES1 and RTC_CASES2 about the reflexive and transitive closure.

  • A theorem stating

       ⊢ ¬(0 < n) ⇔ (n = 0)
    

    (for n a natural number) has been added to the automatic rewrites used by SRW_TAC and srw_ss().

  • Some new automatic rewrites from pred_setTheory:

    • ⊢ DISJOINT (x INSERT s) t ⇔ DISJOINT s t ∧ x ∉ t (and the version of this with DISJOINT s (x INSERT t) as the l.h.s.)
    • ⊢ ∀f s. INJ f ∅ s
    • ⊢ ∀f s. INJ f s ∅ ⇔ (s = ∅)
  • The add_binder and temp_add_binder entry-points in Parse have been removed. They are subsumed by set_fixity <name> Binder and temp_set_fixity <name> Binder respectively. In addition, add_binder was broken, creating an unloadable theory on export.

  • There is a new automatic rewrite from oneTheory:

       ⊢ ∀v:one. v = ()
    

    stating that every value in the type one (analogue of SML’s unit type) is equal to the designated value ().

  • Constants that print to the TeX backend as symbolic identifiers (e.g., non-alphanumeric tokens like +, **) are now annotated there with the \HOLSymConst command rather than \HOLConst. The default behaviour of \HOLSymConst (defined in holtexbasic.sty) is to do nothing.

  • If

  • Holmake is called in a directory with a Holmakefile, and

  • that Holmakefile has at least one explicit target, and

  • Holmake is called with no command-line targets,

then: Holmake will attempt to build only the first target in that Holmakefile. We believe that this will cause problems in only a relatively small number of scenarios. The advantage of this change is that it makes Holmake easier to control from a Holmakefile. It also makes Holmake’s behaviour rather more like that of normal make.

One scenario, among others, where this change may cause problems is where Poly/ML users have set up a rule to create a HOL heap. The fix is to prepend something like the following to your Holmakefile:

   THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
   TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))

   all: $(TARGETS) ...
   .PHONY: all

so that all becomes the first target of the Holmakefile. Any previous targets, such as HOL heaps, should be inserted where the ... occurs above.

Note that Holmakefiles that only include variable declarations such as OPTIONS = ..., INCLUDES = ..., and HOLHEAP = ... don’t have any targets at all, so that Holmake’s behaviour in such files’ directories will not change.


HOL4, Kananaskis-10

Downloads

Kananaskis 9

@mn200 mn200 released this Dec 9, 2013 · 2901 commits to master since this release

Notes on HOL 4, Kananaskis-9 release

We are pleased to announce the Kananaskis-9 release of HOL 4.

Contents

New features:

  • The Define function for making function definitions now treats each clause (each conjunct) of the definition as independent when assessing the types of the new functions’ parameters. For example, the following now works as a definition (termination still has to be proved manually):
   (f x = x + 1 + g (x > 4)) ∧
   (g x = if x then f 0 else 1)

In earlier releases, the parser would have rejected this because the two x parameters would have been required to have the same types (in the clause for f, the author wants x to have type :num, and in the clause for g, type :bool).

This feature is most useful when dealing with algebraic types with numerous constructors, where it can be a pain to keep the names of parameters under constructors apart.

Thanks to Scott Owens for the feature suggestion.

  • The compilation of pattern-matching in function definitions now attempts to be cleverer about organising its nested case-splits. This should result in less complicated definitions (and accompanying induction principles).

Thanks to Thomas Türk for the implementation of this feature.

Bugs fixed:

  • Type abbreviations involving array types (of the form ty1[ty2]) weren’t being pretty-printed. Thanks to Hamed Nemati for the bug report. (GitHub issue)
  • It was possible to prove a theorem which caused an unexportable theory. Thanks to Joseph Chan for the bug report. (GitHub issue)
  • The error messages printed by, and the documentation for, new_type_definition have been improved. Thanks to Rob Arthan for
    the bug report. (GitHub issue)
  • Holmake’s parsing of nested conditional directives (ifdef, ifeq, ifndef etc.) was incorrect.
  • Evaluation and simplification were not correctly handling (real valued) terms such as 0 * 1/2 and 1/2 * 0.
  • Parsing code for tracking the way overloaded constants should be printed stored information in a data structure that grew unreasonably when theories were loaded. Thanks to Scott Owens for the bug report.
  • The emacs mode got confused when called on to open a theory whose name included the substring _fun_. Thanks to Magnus Myreen for the bug report.

New tools:

  • There is a new tactic HINT_EXISTS_TAC designed to instantiate existential goals. If the goal is of the form
   ∃x. P(x) ∧ Q(x) ∧ R(x)

and there is an assumption of the form Q(t) (say), then HINT_EXISTS_TAC applied to this goal will instantiate the existential with the term t.

Thanks to Vincent Aravantinos for the implementation of this tactic.

  • A new tactic, suffices_by, an infix, taking two arguments, a quotation and a tactic. When ``some termsuffices_by tac is executed, the system attempts to prove that `some term` implies the current goal by applying `tac`. The sub-goal(s) resulting from the application of `tac` will be presented to the user, along with `some term`. (GitHub issue)

New examples:

  • Theories in examples/parsing to do with context-free languages, their properties and Parsing Expression Grammars. The material not to do with PEGs is derived from Aditi Barthwal’s PhD thesis, with more still to be updated and brought across.
  • Theories in examples/ARM_security_properties provide proofs of several security lemmas for the ARM Instruction Set Architecture. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. A proof tool is included, which assists the verification of relational state predicates semi-automatically.

The work has been done as part of the PROSPER project by members from KTH Royal Institute of Technology and SICS Swedish ICT. Some of the obtained theorems are tied to that project (but can be adopted for others), while some guarantees are generally applicable.

Incompatibilities:

  • The MEM constant has been replaced with an abbreviation that maps that string to λe l. e ∈ set l. In other words, if you enter MEM x mylist, the underlying term would be x ∈ set mylist (recall also that set is another name for LIST_TO_SET). The pretty-printer will reverse this transformation so that the same term will print as MEM e l. The entry-points for making MEM-terms in listSyntax do the right thing. Similarly, exporting code with EmitML will continue to work.

Thus, SML code that takes MEM-terms apart using functions like rand and rator will likely need to be adjusted. If the SML code uses listSyntax.{dest,mk,is}_mem, it will be fine. (GitHub issue)

  • The case-constants generated for algebraic data types now have different types. The value that is “switched on” is now the first argument of the constant rather than the last. The names of these constants have also changed, emphasising the change. For example, the old constant for natural numbers, num_case had type
   α → (num → α) → num → α

Now the case constant for the natural numbers is called num_CASE and has type

   num → α → (num → α) → α

This change is invisible if the “case-of” syntax is used.

This change makes more efficient evaluation (with EVAL) of expressions with case constants possible.

In addition, the bool_case constant has been deleted entirely: when the arguments are flipped as above it becomes identical to COND (if-then-else). This means that simple case-expressions over booleans will print as if-then-else forms. Thus

   > ``case b of T => 1 | F => 3``;
   val it = ``if b then 1 else 3``: term

More complicated case expressions involving booleans will still print with the case form:

   > ``case p of (x,T) => 3 | (y,F) => y``;
   val it =
     ``case p of (x,T) => 3 | (x,F) => x``: term

At the ML level, we have tried to retain a degree of backwards compatibility. For example, the automatically defined case constants for algebraic types will still be saved in their home-theories with the name “type_case_def”. In addition, case terms for the core types of the system (options, lists, numbers, pairs, sums, etc) can still be constructed and destructed through functions in the relevant typeSyntax modules in the same way. For example, numSyntax.mk_num_case still has the type

   term * term * term -> term

and the returned term-triple still corresponds to the 0-case, the successor-case and the number-argument (in that order), as before. This is despite the fact that the underlying term has those sub-terms in a different order (the number-argument comes first). (GitHub issue)

  • The various printing traces in the Goalstack module have been renamed to all be of the form "Goalstack.<some_name>". For example, what was the trace "goalstack print goal at top" is now "Goalstack.print_goal_at_top". This change collects all the goalstack-related traces together when the traces are listed (e.g., with the traces() command). There is also a new trace, "Goalstack.show_stack_subgoal_count", which, if true (the default), includes the number of sub-goals currently under consideration when a goalstack is printed.
  • The -r command-line option to Holmake now forces recursive behaviour (even with cleaning targets, which is a new feature), rather than being a shorter form of the --rebuild_deps flag.

HOL 4, Kananaskis-9

Downloads