package hol2dk
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=e1d729676f01c0fdfcffaa06be212caa80316dcdccdea77fe3c0973c14fe641d
sha512=7be0c83ef0356ce18889f447a1183c4ec5373c2a47291ceb9c75d426fe159cd824db95b01285f8da805fbd002fdcb91cb59666e31535c3c84cac92075feefd63
README.md.html
Export HOL-Light proofs to Dedukti, Lambdapi and Coq
This project provides several things:
scripts
patch
andunpatch
to (un)patch HOL-Light to dump proofsa program
hol2dk
with commands for dumping proofs from HOL-Light, translate those proofs to Dedukti and Lambdapi, and generate Makefile's to translation those proofs to Coq using lambdapi.
HOL-Light is 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.
Installing HOL-Light sources
Requirements:
hol-light >= af186e9f3c685f5acab16097b05717c10ebb030d (28/01/23)
libipc-system-simple-perl
libstring-shellquote
ocaml 4.14.1
camlp5 8.00.05
ocamlfind
num
Find other potential working ocaml-camlp5 pairs on https://github.com/jrh13/hol-light/pull/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 opam
opam init
opam switch create ocaml.4.14.1
eval `opam env`
opam install ocamlfind num camlp5
git clone --depth 1 -b master https://github.com/jrh13/hol-light
make -C hol-light
Installing hol2dk
Requirements:
ocaml >= 4.13
dune >= 3.7
hol2dk is now available on Opam. To install it, simply do:
opam install hol2dk
For the moment, we however need hol2dk sources to run some commands (checking dk/lp files or translating them to coq).
You can also install hol2dk from its sources as follows:
git clone https://github.com/Deducteam/hol2dk.git
cd hol2dk
dune build && dune install
Setting the environment variable $HOL2DK_DIR
For some commands to have access to files in hol2dk sources, you need to set the following environment variable:
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
Patching HOL-Light sources
bash $HOL2DK_DIR/patch $HOL_LIGHT_DIR
where $HOL_LIGHT_DIR
is the directory where are the sources of HOL-Light.
This script 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:
bash $HOL2DK_DIR/unpatch $HOL_LIGHT_DIR
You can add the option -y
to force file restoration.
Summary of hol2dk commands
Get it by running hol2dk
without arguments.
Dumping HOL-Light proofs
cd $HOL_LIGHT_DIR
hol2dk dump file.ml
generates the files file.sig
, file.prf
and file.thm
.
file.ml
should at least require hol.ml
until the line loads "fusion.ml";;
.
WARNING: it is important to run hol2dk dump
in the HOL-Light directory so as to compute the list of named theorems properly.
Generating dk/lp files from dumped files
The base theory in which HOL-Light proofs are translated is described in the files theory_hol.lp and theory_hol.dk.
You first need to generate file.pos
and file.use
with:
hol2dk pos file
hol2dk use file
You can then generate file.dk
with:
hol2dk file.dk
And file.lp
with:
hol2dk file.lp
It is possible to get the proof of a single theorem by giving its number as additional argument (useful for debugging):
hol2dk file.lp $theorem_number
Generating dk/lp files in parallel
Dk/lp file generation is linear in the size of dumped files. For big dumped files, we provide a command to do file generation in parallel using make
.
First generate file.dg
and file.mk
with:
hol2dk dg $nb_parts file
hol2dk mk file
where $nb_parts
is the number of files in which you want to split the proofs.
Add links to hol2dk files:
ln -s $HOL2DK_DIR/theory_hol.dk
ln -s $HOL2DK_DIR/theory_hol.lp
ln -s $HOL2DK_DIR/lambdapi.pkg
ln -s $HOL2DK_DIR/coq.v
ln -s $HOL2DK_DIR/_CoqProject
Then generate file.dk
with:
make -j $jobs -f file.mk dk
And file.lp
with:
make -j $jobs -f file.mk lp
Checking the generated dk file
Requirement: lambdapi >= 2.3.0, dedukti >= 2.7 or kocheck
To check the generated dk file with dkcheck, do:
dk check file.dk
To check the generated dk file with the current version of kocheck, you need to slightly change the generated file:
sed -e 's/^injective /def /g' file.dk > file-for-kocheck.dk
kocheck -j 7 file-for-kocheck.dk
Checking the generated lp files
Requirement: lambdapi >= 2.3.0 for single-threaded generated files, lambdapi master branch for multi-threaded generated files
To check the generated lp files with lambdapi, do:
lambdapi check --map-dir hol-light:. file.lp
or create a file lambdapi.pkg
:
package_name = hol-light
root_path = hol-light
and simply do:
lambdapi check file.lp
Remark: In case hol-light and dkcheck/lambdapi do not use the same ocaml versions, it is convenient to use different switches in each directory:
Xterm 1 (for HOL-Light):
cd hol-light
opam switch link 4.02.3
eval `opam env`
Xterm 2 (for checking dk/lp files):
opam switch link 4.14.1
eval `opam env`
Translating lp files to Coq files
Requirement: lambdapi master branch
Once HOL-Light files have been translated to Lambdapi files, it is possible to translate Lambdapi files into Coq files using the Coq export feature of Lambdapi.
If your Lambdapi files have been generated using file.mk
, you can simply do:
make -j $jobs -f file.mk v # to generate Coq files
make -j $jobs -f file.mk vo # to check the generated Coq files
To indicate a specific lambdapi
command, do:
make -j $jobs -f file.mk LAMBAPI=$lambdapi v # to generate Coq files
Otherwise, you need to translate Lambdapi files one by one by hand or using a script:
lambdapi export -o stt_coq --encoding $HOL2DK_DIR/encoding.lp --erasing $HOL2DK_DIR/erasing.lp --renaming $HOL2DK_DIR/renaming.lp --requiring coq.v file.lp | sed -e 's/hol-light\.//g' > file.v
You can then check the generated Coq files as follows:
echo coq.v theory_hol.v file*.v > _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq
make -j $jobs -f Makefile.coq
Results
Dumping of hol.ml
:
checking time without proof dumping: 1m14s
checking time with proof dumping: 1m44s (+40%)
dumped files size: 3 Go
number of named theorems: 2834
number of proof steps: 8.5 M (8% unused)
rule | % |
---|---|
refl | 29 |
eqmp | 19 |
comb | 17 |
term_subst | 12 |
trans | 6 |
type_subst | 3 |
beta | 3 |
abs | 2 |
spec | 2 |
Results on a machine with 32 processors i9-13950HX and 64 Go RAM:
Multi-threaded translation to Lambdapi with dg 100
:
hol2dk dg: 14s
lp files generation time: 41s
lp files size: 1.9 Go
type abbrevs: 1.3 Mo
term abbrevs: 665 Mo (35%)
verification by lambdapi: 4h10 on 28 processors Intel Core Haswell @ 2.3 GHz with 16 Mo cache
translation to Coq: 30s 1.8 Go
verification by Coq: 2h29
Multi-threaded translation to Dedukti with dg 100
:
dk file generation time: 1m9s
dk file size: 2.8 Go
type abbrevs: 1.3 Mo
term abbrevs: 752 Mo (27%)
kocheck: 6m19s
dkcheck: 6m22s
Single-threaded translation to Lambdapi (data of 12 March 2023):
lp files generation time: 12m8s
lp files size: 2.5 Go
type abbreviations: 460 Ko
term abbreviations: 787 Mo (31%)
Single-threaded translation to Dedukti (data of 12 March 2023):
dk files generation time: 22m37s
dk files size: 3.6 Go
type abbreviations: 524 Ko
term abbreviations: 820 Mo (23%)
Results for hol.ml
up to arith.ml
(by commenting from loads "wf.ml"
to the end) with dg 7
:
proof dumping time: 12s 77 Mo
number of proof steps: 302 K (10% unused)
dk file generation: 3s 69 Mo
checking time with dk check: 9s
lp file generation: 2s 47 Mo
checking time with lambdapi: 1m15s
translation to Coq: 1s 45 Mo
checking time for Coq 8.18.0: 3m12s
Exporting pure Q0 proofs
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 $HOL_LIGHT_DIR
sed -i -e 's/.*Q0.*//' -e 's/START_ND*)//' -e 's/(*END_ND//' fusion.ml bool.ml equal.ml
Results on hol.ml
upto arith.ml
(by commenting from loads "wf.ml"
to the end):
ocaml proof dumping: 13.2s
number of proof steps: 564351
proof dumping: 1.4s 157 Mo
dk file generation: 45s 153 Mo
checking time with dk check: 26s
checking time with kocheck -j 7: 22s
lp file generation: 29s 107 Mo
checking time with lambdapi: 2m49s
Results on hol.ml
:
ocaml cheking without proof dumping: 1m14s
ocaml proof dumping: 2m9s (+74%)
proof size file: 5.5 Go
number of proof steps: 14.3 M
rule | % |
---|---|
refl | 26 |
eqmp | 21 |
term_subst | 15 |
trans | 11 |
comb | 10 |
deduct | 7 |
type_subst | 4 |
abs | 2 |
beta | 2 |
assume | 2 |
Source files
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.ml
used 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
, coq.v
.
Thanks
HOL-Light proof recording follows ProofTrace developed by Stanislas Polu in 2019.