Release notes for HOL4, Kananaskis-14
(Released: 3 February 2021)
We are pleased to announce the Kananaskis-14 release of HOL4.
Contents
* New
features<file:///Users/nor190/k14-release/kananaskis-14.release.html#new-features>
* Bugs
fixed<file:///Users/nor190/k14-release/kananaskis-14.release.html#bugs-fixed>
* New
theories<file:///Users/nor190/k14-release/kananaskis-14.release.html#new-theories>
* New
tools<file:///Users/nor190/k14-release/kananaskis-14.release.html#new-tools>
* New
Examples<file:///Users/nor190/k14-release/kananaskis-14.release.html#new-examples>
*
Incompatibilities<file:///Users/nor190/k14-release/kananaskis-14.release.html#incompatibilities>
New features:
* The special Type syntax for making type abbreviations can now map to
temp_type_abbrev (or temp_type_abbrev_pp) by adding the local attribute to the
name of the abbreviation.
For example
Type foo[local] = “:num -> bool # num”
or
Type foo[local,pp] = “:num -> bool # num”
Thanks to Magnus Myreen for the feature suggestion.
* We have added a special syntactic form Overload to replace various
flavours of overload_on calls. The core syntax is exemplified by
Overload foo = “myterm”
Attributes can be added after the name. Possible attributes are local (for
overloads that won’t be exported) and inferior to cause a call
inferior_overload_on (which makes the overload the pretty-printer’s last
choice).
Thanks to Magnus Myreen for the feature suggestion.
* The Holmake tool will now build multiple targets across multiple
directories in parallel. Previously, directories were attacked one at a time,
and parallelisation only happened within those directories. Now everything is
done at once. The existing -r option takes on a new meaning as part of this
change: it now causes Holmake to build all targets in all directories
accessible through INCLUDESdirectives. Without -r, Holmake will build just
those dependencies necessary for the current set of targets (likely
files/theories in the current directory).
* It is now possible to write let-expressions more smoothly inside monadic
do-od blocks. Rather than have to write something like
do
x <- M1;
let y = E
in
do
z <- M2 x y;
return (f z);
od
od
one can replace the let-bindings with uses of the <<- arrow:
do
x <- M1;
y <<- E;
z <- M2 x y;
return (f z)
od
(The <<- line above is semantically identical to writing y <- return E, but is
nonetheless syntactic sugar for a let-expression.)
The pretty-printer reverses this transformation.
Thanks to Hrutvik Kanabar for the implementation of this feature.
* There is (yet) another high-level simplification entry-point: gs
(standing for “global simplification”). Like the others in this family this has
type
thm list -> tactic
and interprets theorems as rewrites as with the others. This tactic simplifies
all of a goal by repeatedly simplifying goal assumptions in turn (assuming all
other assumptions as it goes) until no change happens, and then finishes by
simplifying the goal conclusion, assuming all of the (transformed) assumptions
as it does so.
There are three variants on this base (with the same type): gns, gvs and gnvs.
The presence of the vindicates a tactic that eliminates variables (as is done
by rw and some others), and the presence of the n causes assumptions to not be
stripped as they are added back into the goal. Stripping (turned on by default)
is the effect behind strip_assume_tac (and strip_tac) when these tactics add to
the assumptions. It causes, for example, case-splits when disjunctions are
added.
We believe that gs will often be a better choice than the existing fs and rfs
tactics.
* Automatic simplification of multiplicative terms over the real numbers is
more aggressive and capable. Multiplicative terms are normalised, with
coefficients being gathered, and variables sorted and grouped (e.g., z * 2 * x
* 3 turns into 6 * (x * z)). In addition, common factors are eliminated on
either side of relation symbols (<, ≤, and =), and occurrences of inv (⁻¹) and
division are rearranged as much as possible (e.g., z * x pow 2 * 4 = x⁻¹ * 6
turns into x = 0 ∨ 2 * (x pow 3 * z) = 3). To turn off normalisation over
relations within a file, use
val _ = diminish_srw_ss [“RMULRELNORM_ss”]
To additionally stop normalisation, use
val _ = diminish_srw_ss [“RMULCANON_ss”]
These behaviours can also be turned off in a more fine-grained way by using
Excl invocations.
* The Induct_on tactic is now more generous in the goals it will work on
when inducting on an inductively defined relation. For example, if one’s goal
was
∀s t. FINITE (s ∪ t) ∧ s ⊆ t ⇒ some-concl
and the aim was to do an induction using the principle associated with
finite-ness’s inductive characterisation, one had to manually turn the goal
into something like
∀s0. FINITE s0 ==> ∀s t. s0 = s ∪ t ∧ s ⊆ t ⇒ some-concl
before applying Induct_on ‘FINITE’.
Now, Induct_on does the necessary transformations first itself.
* The Inductive and CoInductive syntaxes now support labelling of specific
rules. The supported syntax involves names in square brackets in column 0, as
per the following:
Inductive dbeta:
[~redex:]
(∀s t. dbeta (dAPP (dABS s) t) (nsub t 0 s)) ∧
[~appL:]
(∀s t u. dbeta s t ⇒ dbeta (dAPP s u) (dAPP t u)) ∧
[~appR:]
(∀s t u. dbeta s t ⇒ dbeta (dAPP u s) (dAPP u t)) ∧
[~abs:]
(∀s t. dbeta s t ⇒ dbeta (dABS s) (dABS t))
End
The use of the leading tilde (~) character causes the substitution of the
“stem” name (here dbeta) and an underscore into the name. Thus in this case,
there will be four theorems saved, the first of which will be called
dbeta_redex, corresponding to the first conjunct. If there is no tilde, the
name is taken exactly as given. Theorem attributes such as simp, compute etc.
can be given in square brackets after the name and before the colon. For
example, [~redex[simp]:].
The given names are both saved into the theory (available for future users of
the theory) and into the Poly/ML REPL.
* There is a new using infix available in the tactic language. It is an SML
function of type tactic * thm -> tactic, and allows user-specification of
theorems to use instead of the defaults. Currently, it works with the
Induct_on, Induct, Cases_on and Cases tactics. All of these tactics consult
global information in order to apply specific induction and cases theorems. If
the using infix is used, they will attempt to use the provided theorem instead.
Thus one can do a “backwards” list induction by writing
Induct_on ‘mylist’ using listTheory.SNOC_INDUCT
The using infix has tighter precedence than the various THEN operators so no
extra parentheses are required.
Bugs fixed:
* In extrealTheory: the old definition of extreal_add wrongly allowed
PosInf + NegInf = PosInf, while the definition of extreal_sub wrongly allowed
PosInf - PosInf = PosInf and NegInf - NegInf = PosInf. Now these cases are
unspecified, as is division-by-zero (which is indeed allowed for reals in
realTheory). As a consequence, now all EXTREAL_SUM_IAMGE- related theorems
require that there must be no mixing of PosInf and NegInf in the sum elements.
A bug in ext_suminf with non-positive functions is also fixed.
There is a minor backwards-incompatibility: the above changes may lead to more
complicated proofs when using extreals, while better alignment with textbook
proofs is achieved, on the other hand.
* Fix soundness bug in the HolyHammer translations to first-order.
Lambda-lifting definitions were stated as local hypothesis but were printed in
the TPTP format as global definitions. In a few cases, the global definition
captured some type variables causing a soundness issue. Now, local hypothesis
are printed locally under the quantification of type variables in the
translated formula.
New theories:
* Univariate differential and integral calculus (based on Henstock-Kurzweil
Integral, or gauge integral) in derivativeTheory and integrationTheory. Ported
by Muhammad Qasim and Osman Hasan from HOL Light (up to 2015).
* Measure and probability theories based on extended real numbers, i.e.,
the type of measure (probability) is α set -> extreal. The following new (or
updated) theories are provided:
sigma_algebraTheory
Sigma-algebra and other system of sets
measureTheory
Measure Theory defined on extended reals
real_borelTheory
Borel-measurable sets generated from reals
borelTheory
Borel sets (on extended reals) and Borel-measurable functions
lebesgueTheory
Lebesgue integration theory
martingaleTheory
Martingales based on sigma-finite filtered measure space
probabilityTheory
Probability theory based on extended reals
Notable theorems include: Carathéodory's Extension Theorem (for semirings), the
construction of 1-dimensional Borel and Lebesgue measure spaces, Radon-Nikodym
theorem, Tonelli and Fubini's theorems (product measures), Bayes' Rule
(Conditional Probability), Kolmogorov 0-1 Law, Borel-Cantelli Lemma,
Markov/Chebyshev's inequalities, convergence concepts of random sequences, and
simple versions of the Law(s) of Large Numbers.
There is a major backwards-incompatibility: old proof scripts based on
real-valued measure and probability theories should now open the following
legacy theories instead: sigma_algebraTheory, real_measureTheory,
real_borelTheory, real_lebesgueTheory and real_probabilityTheory. These legacy
theories are stil maintained to support examples/miller and
examples/diningcryptos, etc.
Thanks to Muhammad Qasim, Osman Hasan, Liya Liu and Waqar Ahmad et al. for the
original work, and Chun Tian for the integration and further extension.
New tools:
* holwrap.py: a simple python script that ‘wraps’ hol in a similar fashion
to rlwrap. Features include multiline input, history and basic StandardML
syntax highlighting. See the comments at the head of the script for usage
instructions.
New examples:
* algebra: an abstract algebra library for HOL4. The algebraic types are
generic, so the library is useful in general. The algebraic structures consist
of monoidTheory for monoids with identity, groupTheory for groups, ringTheory
for commutative rings, fieldTheory for fields, polynomialTheory for polynomials
with coefficients from rings or fields, linearTheory for vector spaces,
including linear independence, and finitefieldTheory for finite fields,
including existence and uniqueness.
* simple_complexity: a simple theory of recurrence loops to assist the
computational complexity analysis of algorithms. The ingredients are
bitsizeTheory for the complexity measure using binary bits, complexityTheory
for the big-O complexity class, and loopTheory for various recurrence loop
patterns of iteration steps.
* AKS: a mechanisation of the AKS algorithm, contributed by Hing Lun Chan
from his PhD work.
The theory behind the AKS algorithm is delivered in AKS/theories, starting with
AKSintroTheory, the introspective relation, culminating in AKSimprovedTheory,
proving that the AKS algorithm is a primality test. The underlying theories are
based on finite fields, hence making use of finitefieldTheory in algebra.
An implementation of the AKS algorithm is shown to execute in polynomial-time:
the pseudo-code of subroutines is given in AKS/compute, and the corresponding
implementations in monadic style are given in AKS/machine, which includes a
simple machine model outlined in countMonadTheory and countMacroTheory.
Run-time analysis of subroutines is based on loopTheory in simple_complexity.
The AKS main theorems and proofs have been cleaned up in AKScleanTheory. For
details, please refer to his PhD thesis<http://hdl.handle.net/1885/177195>.
* The code for training tree neural networks using mlTreeNeuralNetwork on
datasets of arithmetical and propositional formulas is located in AI_TNN.
* A demonstration of the reinforcement learning algorithm mlReinforce on
the tasks of synthesizing combinators and Diophantine equations can be found in
AI_tasks.
* bootstrap: a minimalistic verified bootstrapped compiler. By
bootstrapped, we mean that the compiler is applied to itself inside the logic.
We evaluate (using EVAL) this self-application to arrive at an x86-64 assembly
implementation of the compiler function.
* Hoare-for-divergence: a Hoare logic for proving properties of (the output
behaviour of) diverging programs. This Hoare logic has been proved sound and
complete. The same directory also includes soundness and completeness proofs
for a standard total-correctness Hoare logic.
* Lassie: a tool for developing tactic languages by example. A tutorial
using Lassie is included in the manual, and more details about the technique
can be found in the corresponding paper<https://arxiv.org/abs/2101.00930>.
Incompatibilities:
* Two new rewrites to do with disjunctions have been introduced into the
automatic simplifier (and also other simpsets that derive from the fundamental
bool_ss value). The rewrites are
[lift_disj_eq]
⊢ (x ≠ y ∨ P ⇔ x = y ⇒ P) ∧
(P ∨ x ≠ y ⇔ x = y ⇒ P)
[lift_imp_disj]
⊢ ((P ⇒ Q) ∨ R ⇔ P ⇒ Q ∨ R) ∧
(R ∨ (P ⇒ Q) ⇔ P ⇒ R ∨ Q)
These can be removed with Excl directives, the -* operator or {temp_,}delsimps.
* The treatment of abbreviations (introduced with qabbrev_tac for example),
has changed slightly. The system tries harder to prevent abbreviation
assumptions from changing in form; they should stay as Abbrev(v = e), with v a
variable, for longer. Further, the tactic VAR_EQ_TAC which eliminates
equalities in assumptions and does some other forms of cleanup, and which is
called as part of the action of rw, SRW_TAC and others, now eliminates
“malformed” abbreviations. To restore the old behaviours, two steps are
required:
val _ = diminish_srw_ss ["ABBREV"]
val _ = set_trace "BasicProvers.var_eq_old" 1
which invocation can be made at the head of script files.
* The theorem rich_listTheory.REVERSE (alias of
listTheory.REVERSE_SNOC_DEF) has been removed because REVERSE is also a
tactical (Tactical.REVERSE).
* listTheory and rich_listTheory: Some theorems have been generalized.
For example, EVERY_{TAKE, DROP, BUTLASTN, LASTN} had unnecessary preconditions.
As a result of some theorems being generalized, some _IMP versions of the same
theorems have been dropped, as they are now special cases of the non-_IMP
versions.
Also, DROP_NIL has been renamed to DROP_EQ_NIL, to avoid having both DROP_nil
and DROP_NIL around. Furthermore, >= in the theorem statement has been replaced
with <=.
* Renamed theorems in pred_setTheory: SUBSET_SUBSET_EQ became
SUBSET_ANTISYM_EQ (compatible with HOL Light).
* The theorem SORTED_APPEND_trans_IFF has been moved from alist_treeTheory
into sortingTheory. The moved theorem is now available as SORTED_APPEND, and
the old SORTED_APPEND is now available as SORTED_APPEND_IMP. To avoid
confusion, as SORTED_APPEND is now an (conditional) equality, SORTED_APPEND_IFF
has been renamed to SORTED_APPEND_GEN.
* The definition SORTED_DEF is now an automatic rewrite, meaning that terms
of the form SORTED R (h1::h2::t) will now rewrite to R h1 h2 /\ SORTED (h2::t)
(in addition to the existing automatic rewrites for SORTED R [] and SORTED R
[x]). To restore the old behaviour it is necessary to exclude SORTED_DEF(use
temp_delsimps), and reinstate SORTED_NIL and SORTED_SING (use augment_srw_ss
[rewrites [thmnames]]).
* The syntax for greater than in intSyntax and realSyntax is consistently
named as in numSyntax: The functions great_tm,dest_great and mk_great become
greater_tm, dest_greater and mk_greater, respectively. Additionally,
int_arithTheory.add_to_great is renamed to int_arithTheory.add_to_greater.
* Two theorems about list$nub (the constant that removes duplicates in a
list), have been made automatic: listTheory.nub_NIL (⊢ nub [] = []) and
listTheory.all_distinct_nub (⊢ ∀l. ALL_DISTINCT (nub l)). Calls to
temp_delsimps can be used to remove automatic rewrites as necessary.
* The SML API for ThmSetData has changed; user-provided call-backs that
apply set-changes (additions and removals of theorems) are only ever called
with single changes at once rather than lists, so the required types for these
call-backs has changed to reflect this.
* Parsing of ~x has been changed so that this is always preferentially
interpreted as being a boolean operation. This may break proofs over types with
a numeric negation that use expressions such as
SPEC “~x” some_theorem
It is much better style to use Q.SPEC ‘~x’ some_theorem; and indeed one can
also use - as a unary operator, so that Q.SPEC ‘-x’ some_theorem will also work.
If a big script is broken by this, one can reinstate the old behaviour by
changing the grammar locally with
Overload "~"[local] = “numeric_negation_operator”
where the appropriate negation operator might be, e.g., “$real_neg”.
* Two theorems about TAKE and DROP have been added to the stateful
simplifier:
TAKE_LENGTH_ID_rwt2
⊢ ∀l m. TAKE m l = l ⇔ LENGTH l ≤ m
DROP_EQ_NIL
⊢ ∀l m. DROP m l = [] ⇔ LENGTH l ≤ m
The former is a new theorem; the latter is an existing theorem that has been
promoted to “automatic” status. Use Excl or {temp_,}delsimps to remove these
theorems from the simplifier as necessary.
* The BIGINTER_SUBSET theorem in pred_setTheory has changed from
⊢ ∀sp s. (∀t. t ∈ s ⇒ t ⊆ sp) ∧ s ≠ ∅ ⇒ BIGINTER s ⊆ sp
to
⊢ ∀sp s t. t ∈ s ∧ t ⊆ sp ⇒ BIGINTER s ⊆ sp
________________________________
HOL4, Kananaskis-14<http://hol-theorem-prover.org/>
Release notes for the previous
version<file:///Users/nor190/k14-release/kananaskis-13.release.html>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
