This project provides a tool to translate HOL-Light proofs to Dedukti, Lambdapi and Coq.
HOL-Light is a proof assistant based on higher-order logic, aka simple type theory.
Dedukti is a proof format based on the λΠ-calculus modulo rewriting (λ-calculus + simple types + dependent types + implicit type equivalence modulo user-defined rewriting rules).
Lambdapi is a proof assistant based on the λΠ-calculus modulo rewriting that can read and generate Dedukti proofs.
Coq is a proof assistant based on the Calculus of Inductive Constructions.
The HOL-Light base library hol.ml and the libraries Arithmetic and
Logic formalizing the metatheory of first-order logic can be
exported and translated to Dedukti, Lambdapi and Coq in a few
minutes. The generated Dedukti files can be checked in a few minutes
as well, but it takes a much longer time for Coq and Lambdapi to check
the generated files (16 minutes for Coq for hol.ml).
For bigger libraries like Multivariate, it takes more time,
especially for Coq. For instance, the Multivariate library up to
topology.ml can be translated to Lambdapi in 18 minutes, then to Coq
in 18 more minutes, but the verification of the generated files by Coq
takes 8 hours.
While it is possible to translate any HOL-Light proof to Coq, the translated theorems may not be directly applicable by Coq users because not all HOL-Light types and functions are aligned with those of the Coq standard library yet. Currently, we only aligned the types of natural numbers and lists, and some functions on them in the file HOLLight.v. We gathered the resulting theorems in the Opam package coq-hol-light available in the Coq Opam repository released. We plan to add more mappings, especially on real numbers.
HOL-Light is based on classical higher-order logic with functional and propositional extensionality. We use the following Coq axioms to encode them:
Axiom classic : forall P:Prop, P \/ ~ P.
Axiom constructive_indefinite_description : forall (A : Type) (P : A->Prop), (exists x, P x) -> { x : A | P x }.
Axiom fun_ext : forall {A B : Type} {f g : A -> B}, (forall x, (f x) = (g x)) -> f = g.
Axiom prop_ext : forall {P Q : Prop}, (P -> Q) -> (Q -> P) -> P = Q.
Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
- Translating HOL-Light proofs to Coq, Frédéric Blanqui, 4 April 2024
Requirements:
- hol-light = ea45176 (07/02/24)
- ocaml = 4.14.2
- camlp5 = 8.02.01
- ocamlfind
- zarith, which may require pkg-config and libgmp-dev
- libipc-system-simple-perl
- libstring-shellquote
Find other potential working ocaml-camlp5 pairs on jrh13/hol-light#71 .
If you don't already have the HOL-Light sources somewhere, you can install them by using the following commands:
cd $HOME
sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl pkg-config libgmp-dev opam
opam init
opam switch create ocaml.4.14.2
eval `opam env`
opam install ocamlfind zarith camlp5.8.02.01
git clone https://github.com/jrh13/hol-light
git checkout ea45176
make -C hol-light
Requirements:
- ocaml >= 4.13
- dune >= 3.7
hol2dk is available on Opam. To install it, simply do:
opam install hol2dk
You can also install hol2dk from its sources as follows:
git clone https://github.com/Deducteam/hol2dk.git
cd hol2dk
dune build && dune install
For some commands to have access to files in hol2dk sources, you need to set the following environment variables:
export HOLLIGHT_DIR= # absolute path to hol-light source directory
export HOL2DK_DIR= # absolute path to hol2dk source directory
In case you installed hol2dk using opam, write:
export HOL2DK_DIR=$OPAM_SWITCH_PREFIX/share/hol2dk
Get it by running hol2dk | less.
By default, HOL-Light does not generate proofs that can be checked independently. Therefore, it must be patched so that proof steps are recorded:
hol2dk patch
This command slightly modifies a few HOL-Light files in order to dump proofs:
fusion.ml: the HOL-Light kernel file defining types, terms, theorems, proofs and proof rulesbool.ml: HOL-Light file defining basic tactics corresponding to introduction and elimination rules of connectivesequal.ml: HOL-Light file defining basic tactics on equality
The patch also adds a file xnames.ml.
Before applying the patch, a copy of these files is created in fusion-bak.ml, bool-bak.ml, etc.
To restore HOL-Light files, simply do:
hol2dk unpatch
For dumping the proofs of a HOL-Light file depending on hol.ml do:
cd $HOLLIGHT_DIR
hol2dk dump-simp [$path/]file.ml
This will generate the following files:
[$path/]file.sig: constants[$path/]file.prf: theorems (proof steps)[$path/]file.thm: named theorems[$path/]file.pos: positions of proof steps infile.prf[$path/]file.use: data about the use of theorems
WARNING: it is important to run the command in $HOLLIGHT_DIR so as to compute the list of named theorems properly.
For dumping (a subset of) hol.ml do:
cd $HOLLIGHT_DIR
hol2dk dump-simp-before-hol file.ml
where file.ml should at least contain the contents of hol.ml until the line loads "fusion.ml";;.
The command dump-simp (and similarly for dump-simp-before-hol) are actually the sequential composition of various lower level commands: dump, pos, use, rewrite and purge:
Simplifying dumped proofs. HOL-Light proofs have many detours that can be simplified following simple rewrite rules. For instance, s(u)=s(u) is sometimes proved by MK_COMB from s=s and u=u, while it can be directly proved by REFL.
The command rewrite implements the following simplification rules:
- SYM(REFL(t)) ⟶ REFL(t)
- SYM(SYM(p)) ⟶ p
- TRANS(REFL(t),p) ⟶ p
- TRANS(p,REFL(t)) ⟶ p
- CONJUNCT1(CONJ(p,_)) ⟶ p
- CONJUNCT2(CONJ(_,p)) ⟶ p
- MKCOMB(REFL(t),REFL(u)) ⟶ REFL(t(u))
- EQMP(REFL _,p) ⟶ p
Purging dumped proofs. Because HOL-Light tactics may fail, some theorems are generated but not used in the end, especially after simplification. Therefore, they do not need to be translated.
The command purge compute in file.use all the theorems that do not need to be translated. For instance, in the HOL-Light base library hol.ml, 60% of proof steps are useless after simplication.
The command simp is the sequential composition of rewrite and purge.
Requirements:
- lambdapi commit >= 31aef37c (25/11/24) > 2.5.1
- coq-hol-light-real
For not cluttering HOL-Light sources with the many generated files, we suggest to proceed as follows. For instance, for generating the proofs of the Logic library, do:
cd $HOLLIGHT_DIR/Logic
hol2dk dump-simp make.ml
mkdir -p ~/output-hol2dk/Logic
cd ~/output-hol2dk/Logic
hol2dk link Logic/make
This will create files and add links to files needed to generate, translate and check proofs.
You can then do in order:
maketo get the list of targets and variablesmake splitto generate a file for each theoremmake -j$jobs lpto translate HOL-Light proofs to Lambdapimake -j$jobs lpoto check Lambdapi files (optional)make -j$jobs vto translate Lambdapi files to Coq filesmake -j$jobs voto check Coq files
To speed up lp file generation for some theorems with very big proofs, you can write in a file called BIG_FILES a list of theorem names (lines starting with # are ignored). See for instance BIG_FILES. You can also change the default values of the options --max-proof-size and --max-abbrev-size as follows:
make -j$jobs MAX_PROOF=500_000 MAX_ABBREV=2_000_000 lp
Remark: for the checking of generated Coq files to not fail because of lack of RAM, we generate for each theorem ${thm}.lp one or several files for its proof, and a file ${thm}_spec.lp declaring this theorem as an axiom. Moreover, each other theorem proof using ${thm} requires ${thm}_spec instead of ${thm}.
On a machine with 32 processors i9-13950HX and 64G RAM, with OCaml 5.1.1, Camlp5 8.02.01, Lambdapi 2.5.0 and Coq 8.19.1:
| HOL-Light file | dump-simp | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo |
|---|---|---|---|---|---|---|---|---|
| hol.ml | 3m57s | 3 Gb | 5 M | 5679 | 51s | 55s | 1 Gb | 18m4s |
| Multivariate/make_upto_topology.ml | 48m | 52 Gb | 52 M | 18866 | 22m22s | 20m16s | 68 Gb | 8h (*) |
| Multivariate/make_complex.ml | 2h48m | 158 Gb | 220 M | 20200 | 52m26s | 31m39s | 240 Gb |
(*) with make -j32 vo; make -j8 vo
The Makefile commands above are not implemented for Dedukti yet. It is however possible to translate HOL-Light proofs to Dedukti in parallel by using the following older and less efficient commands:
hol2dk mk $nb_parts $base
make -f $base.mk -j$jobs dk
where $base is the base name of the library, e.g. make for $HOLLIGHT_DIR/Logic/make, which is also written in the file named BASE that is created when you do hol2dk link Logic/make.
It generates a single big Dedukti file $base.dk. To check it with dkcheck version >= 2.7, simply do:
dk check $base.dk
To check it with kocheck, simply do:
kocheck -j$jobs file-for-kocheck.dk
Performances: hol.dk can be checked by dkcheck in 4m11s.
While it is possible to translate any HOL-Light library to Coq, the obtained theorems may not be directly applicable by Coq users because HOL-Light types and functions may not be aligned with those of the Coq standard library yet. Currently, only the following types and functions have been aligned with those of Coq:
- unit type
- product type constructor
- type of natural numbers
- functions and predicates on natural numbers: addition, multiplication, order, power, maximum, minimum, substraction, factorial, division, division remainder, parity
- sum type constructor
- option type constructor
- type of lists
- functions on lists
- type of reals
- basic functions and predicates on reals
The part of HOL-Light that is aligned with Coq is gathered in the package coq-hol-light available in the Coq Opam repository released.
It is possible to get statistics on proofs by using the command stat. For instance, for hol.ml, after simplification, we get:
| rule | % |
|---|---|
| comb | 20 |
| term_subst | 17 |
| refl | 16 |
| eqmp | 12 |
| trans | 9 |
| conjunct1 | 6 |
| abs | 3 |
| beta | 3 |
| mp | 3 |
| sym | 2 |
| deduct | 2 |
| type_subst | 2 |
| assume | 1 |
| conjunct2 | 1 |
| disch | 1 |
| spec | 1 |
| disj_cases | 1 |
| conj | 1 |
Hol2dk instruments basic HOL-Light tactics corresponding to introduction and elimination rules of connectives to get smaller proofs and proofs closer to natural deduction proofs. It is however possible to generate full Q0 proofs by doing after patching:
cd $HOLLIGHT_DIR
sed -i -e 's/.*Q0.*//' -e 's/START_ND*)//' -e 's/(*END_ND//' fusion.ml bool.ml equal.ml
HOL-Light proof recording improves ProofTrace developed by Stanislas Polu in 2019.
Modified HOL-Light files:
lib.ml: provides functions on lists, etc. required byfusion.ml. A few lines are commented out so that it compiles with ocamlc.fusion.ml: defines types, terms, theorems, proofs and elementary proof rules.bool.ml: defines basic tactics corresponding to introduction and elimination rules of connectives.equal.ml: defines basic tactic(al)s on equality including alpha and beta-reduction. These files contain special comments that are removed to patch hol-light.
Additional files required for hol2dk:
main.ml: main program of Hol2dk.xprelude.ml: provides a few basic definitions.xlib.ml: functions on types, terms and other data structures.xproof.ml: functions for accessing proofs.xlp.ml: translation to Lambdapi of types, terms and proofs.xdk.ml: translation to Dedukti of types, terms and proofs.xfiles.ml: functions to compute dependencies and theorems of HOL-Light files.xnames.ml: functions for dumping the index of named theorems.xci.ml: slightly truncated version of the HOL-Light filehol.mlused for testing.
Note that all these files can be used in the OCaml toplevel as well by removing the open instructions and by adding unset_jrh_lexer;; and set_jrh_lexer;; at the beginning and at the end of the file.
Files necessary for the export to Coq: encoding.lp, erasing.lp, renaming.lp, HOLLight.v.
f.prf: proof steps
f.nbp: number of proof steps
f.sig: signature (types, constants, axioms, definitions)
f.thm: map from proof step index to theorem name (if any)
f.pos: array providing the position in f.prf of each proof step index
f.use: array lastuse such that lastuse.(i) = 0 if i is a named theorem, the highest proof step index using i if there is one, and -1 otherwise.
f.thp: map every useful theorem index to its name and position (similar to f.thm but with position)
n.sti: starting index (in f.prf) of theorem n
n.siz: estimation of the size of the proof of n
n_part_k.idx: min and max index (in n.prf) of part k proof steps
n.max: array of max proof step indexes of each part of n
n.typ: map from type expression strings to digests and number of type variables
n.sed: sed script to replace type expression digests by type abbreviations
n.brv: ordered list of pairs (term, term abbreviation number)
n.brp: array of positions in the file n.brv
n_term_abbrevs_part_i.min: min and max term abbreviation number of part i
f_types.lp: types
f_type_abbrevs.lp: type abbreviations
f_terms.lp: function symbols (i.e. signature)
f_axioms.lp: axioms
dump f.ml: generates an ml file and call ocaml on it to check f.ml and generates f.prf, f.nbp, f.sig and f.thm
dump-simp f.ml: calls the commands dump f.ml, pos f, use f, and simp f
pos f: reads f.nbp and f.prf, and generates f.pos
use f: reads f.nbp, f.thm and f.prf, and generates f.use
simp f: calls the commands rewrite f and purge f
rewrite f: reads f.pos, f.use and f.prf, and generates a new version of f.prf where proofs have been simplified
purge f: reads f.pos, f.prf, f.thm and f.use, and generates a new file f.use where useless proof steps are mapped to -1
split f: reads f.pos, f.use and f.thm, generates f.thp and, for each useful theorem n (if it has no user-defined name, we use its index as name), n.nbp, n.sti, n.pos, n.use
thmsize f n.lp: reads f.prf, n.use, n.pos, n.sti, and generates n.siz
thmsplit f n.lp: reads f.sig, f.thp, f.prf, n.use, n.sti, n.siz, n.pos, and generates the files n_part_k.idx, n.max and n.lp
thmpart f n_part_k.lp: reads f.sig, f.thp, f.prf, n.pos, n.use, n.sti, n.max, n_part_k.idx, and generates n_part_k.lp, n_part_k.brv, n_part_k.brp, n_part_k_term_abbrevs_part_i.min, n_part_k_subterms.lp
theorem f n.lp: reads f.sig, f.thp, f.prf, n.pos, n.use, n.sti, and generates the files n_part_k_proofs.lp, n_proofs.lp, n.typ, n_term_abbrevs.lp, n_subterm_abbrevs.lp, n_term_abbrevs.typ, n_part_k_deps.lp, n_part_k.lp.
abbrev f n_term_abbrevs_part_i.lp: reads f.sig, f.thp, n.brv, n.brp, n_term_abbrevs_part_i.min, and generates n_term_abbrevs_part_i.typ and n_term_abbrevs_part_i.lp
type_abbrevs f: for each file n.typ in the current directory, reads n.typ and generates n.sed and f_type_abbrevs.lp
split: calls hol2dk command split
lp:
- generates
f_types.lp,f_type_abbrevs.lp,f_terms.lp,f_axioms.lp - for every big file n.lp, calls hol2dk thmsize f n.lp (generates the file n.siz) and hol2dk thmsplit f n.lp (generates the files
n_part_k.idx, n.max and n.lp) - calls the Makefile target lp-proofs
- calls the Makefile target lp-abbrevs
- calls hol2dk type_abbrevs f
- calls the Makefile target rename-abbrevs
lp-proofs:
- for each file
n_part_k.idx(big file part), calls hol2dk thmpart fn_part_k.lp - for each file n.sti for which there is no file n.lp yet (small files), calls hol2dk theorem f n.lp
lp-abbrevs: for each file n.min, calls hol2dk abbrev f n.lp
rename-abbrevs: for each file n.sed, apply n.sed to n.lp