HOLLIGHTCOQ
HOLLIGHTCOQ is a communication tool between two interactive theorem
provers: HOLLight
and Coq. It mainly automatically
imports HOLLight'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 HOLLight. It
includes a distribution of HOLLight with its standard library.
Download:

Development
version, snapshot
of 1/18/10.
Software requirements
For Coq:
For HOLLight:
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 HOLLight proofs will be exported;
for instance:
 export HOLPROOFEXPORTDIR=/tmp

 Compile the HOLLight framework:
 cd ../hol_light
 make

 The command above creates an OCaml toplevel in which
HOLLight can be launched:
 ./top
 #use "hol.ml";;

 Export the proofs:
 export_saved_proofs ();;

 Exit the OCaml toplevel, 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:
 HOLLight 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
HOLLight'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 antispam dots and at).
Top of the page
Related work
Exportation of HOLLight's theorems is based on Steven
Obua's proof recording
tool for HOLLight.
Top of the page
Last update: 03/01/10