The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

    Dear Coq users,

I am pleased to announce the availability on Opam of new versions of hol2dk and coq-hol-light:

- Hol2dk (https://github.com/Deducteam/hol2dk) is a tool to extract proofs from HOL-Light and translate them to Dedukti, Lambdapi and Coq (using the Coq export function of Lambdapi). This new version provides a lot of improvements wrt the previous version:
    . simplification of HOL-Light proofs
    . elimination of useless proof steps
    . new command split to generate a file for each named theorem
      and translate and check them in parallel using make
    . more efficient implementation of abbreviation recording
    . a new option --sharing for handling some big proofs in the Multivariate library (> several Go)
    . many other useful commands
    . improvement of the command line interface
    . more alignments between HOL-Light and Coq (sum, option and list types) thanks to Anthony Bordg

The HOL-Light base library hol.ml can now be translated to Lambdapi in less than 1 minute, to Coq in less than 1 minute, and checked by Coq in about 30 minutes.

- Coq-hol-light (https://github.com/Deducteam/coq-hol-light) is a Coq library on Coq's types of natural numbers and lists mainly, which has been automatically generated from HOL-Light by using hol2dk, and a mapping of HOL-Light types and functions to Coq types and functions. It currently contains 667 theorems. Much more theorems will be made available as soon as we will have a mapping of HOL-Light reals to Coq reals.

Best regards,

Frédéric Blanqui,

chair of https://europroofnet.github.io/.