add hol.ml up to lists.ml (#2)

.github/workflows/main.yml

@@ -19,6 +19,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'

AUTHORS.md

@@ -1 +1,2 @@
 - [Frédéric Blanqui](https://blanqui.gitlabpages.inria.fr/)
+- [Anthony Bordg](https://sites.google.com/site/anthonybordg/)

CHANGES.md

@@ -3,6 +3,10 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
+## 0.0.1 (2024-02-24)
+
+Contains HOL-Light up to lists.ml.
+
 ## 0.0.0 (2023-11-06)
 
 First release. Contains HOL-Light up to arith.ml only.

README.md

@@ -10,15 +10,16 @@ Axiom classic : forall P:Prop, P \/ ~ P.
 Axiom constructive_indefinite_description : forall (A : Type) (P : A->Prop), (exists x, P x) -> { x : A | P x }.
 Axiom fun_ext : forall {A B : Type} {f g : A -> B}, (forall x, (f x) = (g x)) -> f = g.
 Axiom prop_ext : forall {P Q : Prop}, (P -> Q) -> (Q -> P) -> P = Q.
+Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
 ```
 
-For the moment, it only contains the HOL-Light base library up to [arith.ml](https://github.com/jrh13/hol-light/blob/master/arith.ml), that is, basic theorems on first-order logic and on natural numbers arithmetic on the Coq functions pred, add, mul, pow, div, modulo, max, min, and the Coq predicates le, lt, ge, gt, Even, Odd.
+For the moment, it only contains the HOL-Light base library up to [lists.ml](https://github.com/jrh13/hol-light/blob/master/lists.ml), that is, basic theorems on first-order logic, on natural numbers arithmetic on the Coq functions pred, add, mul, pow, div, modulo, max, min, and the Coq predicates le, lt, ge, gt, Even, Odd, and on basic functions on lists.
 
-We can translate to Coq much bigger parts of the HOL-Light library (at least all the base library [hol.ml](https://github.com/jrh13/hol-light/blob/master/hol.ml)). However, to get a library that is directly usable in Coq, we need to align HOL-Light functions and predicates to the ones defined in Coq standard library. This requires to (for the moment) manually prove that the HOL-Light definitions are equal to the corresponding Coq definitions. This has been done for the above functions and predicates but remains to be done for more functions and predicates on lists, real numbers, etc.
+We can translate to Coq much bigger parts of the HOL-Light library (at least all the base library [hol.ml](https://github.com/jrh13/hol-light/blob/master/hol.ml)). However, to get a library that is directly usable in Coq, we need to align HOL-Light functions and predicates to the ones defined in Coq standard library. This requires to manually prove that the HOL-Light definitions are equal to the corresponding Coq definitions. This has been done for the above functions and predicates but remains to be done for other types like real numbers.
 
-The translated theorems are (for the moment) provided as axioms in order to have fast Require's in Coq because the proofs currently extracted from HOL-Light are very big and not very informative for they are low level (the translation is done at the kernel level, not at the source level). If you are skeptical, you can however generate and check them again by using [hol2dk](https://github.com/Deducteam/hol2dk).
+The translated theorems are provided as axioms in order to have fast Require's in Coq because the proofs currently extracted from HOL-Light are very big and not very informative for they are low level (the translation is done at the kernel level, not at the source level). If you are skeptical, you can however generate and check them again by using [hol2dk](https://github.com/Deducteam/hol2dk).
 
-The current library contains 448 lemmas. The corresponding Coq proof files have a size of 49 Mo and take about 4m25s to check. The whole HOL-Light base library `hol.ml` has 2834 theorems. The corresponding Coq proof files have a size of 1.9 Go and take about 6 hours to check (with 64 Go RAM). The full HOL-Light library has 36471 theorems.
+The current library contains 667 lemmas. The corresponding Coq proof files have a size of 86 Mo and take about 4m to check. The whole HOL-Light base library `hol.ml` has 2834 theorems. The corresponding Coq proof files have a size of 1.1 Go and take about 31m to check (with 32 processors and 64 Go RAM). The full HOL-Light library has 36471 theorems.
 
 **Installation using [opam](https://opam.ocaml.org/)**
 
@@ -36,32 +37,4 @@ Check thm_DIV_DIV.
 
 **Reproducibility**
 
-First, install HOL-Light and hol2dk as described in [README.md](https://github.com/Deducteam/hol2dk/blob/main/README.md). Then, do:
-
-```
-mkdir reproduce
-cd reproduce
-git clone https://github.com/jrh13/hol-light.git
-export HOL_LIGHT_DIR=`pwd`/hol-light
-git clone https://github.com/Deducteam/hol2dk.git
-export HOL2DK_DIR=`pwd`/hol2dk
-cd $HOL2DK_DIR
-git checkout 983fc82
-dune build && dune install
-./patch $HOL_LIGHT_DIR
-cd $HOL_LIGHT_DIR
-git checkout 9c07c4f
-make
-cp hol.ml hol_upto_arith.ml
-emacs hol_upto_arith.ml # edit hol_upto_arith.ml by removing every thing after ``loads "arith.ml";;''
-hol2dk dump hol_upto_arith.ml
-hol2dk pos hol_upto_arith
-hol2dk use hol_upto_arith
-ln -s $HOL2DK_DIR/lambdapi.pkg
-ln -s $HOL2DK_DIR/theory_hol.lp
-ln -s $HOL2DK_DIR/_CoqProject
-ln -s $HOL2DK_DIR/coq.v
-hol2dk dg 7 hol_upto_arith
-hol2dk mk-part hol_upto_arith
-make -j7 -f hol_upto_arith.mk vo
-```
+First, install HOL-Light and hol2dk as described in [README.md](https://github.com/Deducteam/hol2dk/blob/main/README.md). Then, do run [reproduce.sh](https://github.com/Deducteam/hol2dk/blob/main/reproduce.sh). If every thing works well, the proofs will be in the directory `reproduce/output`.

axioms.v

@@ -0,0 +1,4 @@
+Require Import coq.
+Require Import theory_hol.
+Require Import types.
+Require Import terms.

coq-hol-light.opam

@@ -11,7 +11,7 @@ doc: "https://github.com/Deducteam/coq-hol-light"
 maintainer: "[email protected]"
 authors: ["Frédéric Blanqui"]
 license: "CeCILL-2.1"
-depends: [ "coq" {>= "8.16"} ]
+depends: [ "coq" {>= "8.19"} ]
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 tags: [