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.


The source code is available under the same license as HOL-Light. It includes a distribution of HOL-Light with its standard library.

Software requirements

For Coq: For HOL-Light:

Top of the page


Basic usage of HOLLIGHTCOQ

After unpacking the sources:
  1. Compile the Coq files:
    cd coq
  2. Define a new environment variable $HOLPROOFEXPORTDIR pointing the directory in which the HOL-Light proofs will be exported; for instance:
  3. Compile the HOL-Light framework:
    cd ../hol_light
  4. The command above creates an OCaml top-level in which HOL-Light can be launched:
    #use "hol.ml";;
  5. Export the proofs:
    export_saved_proofs ();;
  6. 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
  7. Compile the Coq theorems that were generated:

Using particular theorems in Coq

To use some particular theorems T1,..., TN in Coq, you can proceed as follows: 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

Home Research Studies Teaching Miscellaneous

Last update: 03/01/10