HOLLIGHTCOQ
HOLLIGHTCOQ is a communication tool between two interactive theorem
provers: HOL-Light
and Coq. It mainly automatically
imports HOL-Light's theorems into Coq in order to check and use them in
Coq. It pays a particular attention to restore theorems intelligibility
in Coq.
Sources
The source code is available under the same license as HOL-Light. It
includes a distribution of HOL-Light with its standard library.
Download:
-
Development
version, snapshot
of 1/18/10.
Software requirements
For Coq:
For HOL-Light:
Top of the page
Usage
Basic usage of HOLLIGHTCOQ
After unpacking the sources:
-
- Compile the Coq files:
- cd coq
- make
-
- Define a new environment variable $HOLPROOFEXPORTDIR pointing
the directory in which the HOL-Light proofs will be exported;
for instance:
- export HOLPROOFEXPORTDIR=/tmp
-
- Compile the HOL-Light framework:
- cd ../hol_light
- make
-
- The command above creates an OCaml top-level in which
HOL-Light can be launched:
- ./top
- #use "hol.ml";;
-
- Export the proofs:
- export_saved_proofs ();;
-
- Exit the OCaml top-level, copy the Coq files compiled in 1. in
the exportation directory:
- cp ../coq/*.vo $HOLPROOFEXPORTDIR/hollight/hollight/
- cd $HOLPROOFEXPORTDIR/hollight/hollight
-
- Compile the Coq theorems that were generated:
- make
Using particular theorems in Coq
To use some particular theorems T1,..., TN in Coq, you can proceed as
follows:
-
- Change step 5. into:
- export_list ["T1";...;"TN"];;
- (If N = 1, you can also use:
- export_one_proof "T1";;
- .)
-
- Change step 7. into:
- make thms
- This creates a file theorems.vo containing the Coq version of
the theorems T1,...,TN.
For instance, you can try
- export_one_proof "MOD_EQ_0";;
to get the corresponding theorem into Coq.
By default, facilities allow to export lemmas about natural integers.
You can change or complement it by editing the file
hol_light/interpretation.txt. It contains a set of couple of lines:
- HOL-Light definition
- Coq's counterpart
. Be careful that the Coq terms must be correct and well typed;
otherwise, compilation will fail.
We intend to facilitate and make robust the way a user can interpret
HOL-Light's definitions.
Top of the page
Suggestions and bug report
Do not hesitate to make any suggestion or to report bugs to
Chantal
Keller (remove the anti-spam dots and at).
Top of the page
Related work
Exportation of HOL-Light's theorems is based on Steven
Obua's proof recording
tool for HOL-Light.
Top of the page
Last update: 03/01/10