add the translation of Multivariate

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/).
 
+## Unreleased
+
+Add HOL-Light library Multivariate/make_complex.ml (~20,000 theorems).
+
 ## 2.0.0 (2024-12-17)
 
 All HOL-Light base library lib_hol.ml with alignement of real numbers.

CONFIG

@@ -0,0 +1,2 @@
+#!/bin/sh
+hol2dk config Multivariate/make_complex.ml HOLLight HOLLight_Real_With_N.mappings With_N.v Coq.NArith.BinNat Coq.Reals.Rbase Coq.Reals.Rdefinitions Coq.Reals.Rbasic_fun With_N.lp With_N.mk

Makefile

@@ -1,3 +1,5 @@
+LIBNAME=HOLLight
+
 .SUFFIXES:
 
 .PHONY: default
@@ -8,7 +10,7 @@ Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o $@
 
 _CoqProject:
-	echo -R . HOLLight `ls *.v` > $@
+	echo "-R . $(LIBNAME) `ls *.v`" > $@
 
 .PHONY: clean
 clean: Makefile.coq

README.md

@@ -1,11 +1,15 @@
 HOL-Light libraries in Coq
 --------------------------
 
-This Coq library contains an automatic translation in [Coq](https://coq.inria.fr/) of the [HOL-Light](https://github.com/jrh13/hol-light) base library [hol_lib.ml](https://github.com/jrh13/hol-light/blob/master/hol_lib.ml) with HOL-Light types and functions mapped to the corresponding types and functions in the Coq standard library so that, for instance, a HOL-Light theorem on HOL-Light real numbers is translated into a Coq theorem on Coq real numbers. The provided theorems can therefore be readily reused and combined with other Coq developments based on the Coq standard library.
+This Coq library contains an automatic translation in [Coq](https://coq.inria.fr/) of the [HOL-Light](https://github.com/jrh13/hol-light) library [Multivariate/make_complex.ml](https://github.com/jrh13/hol-light/blob/master/Multivariate/make_complex.ml) with various HOL-Light types and functions mapped to the corresponding types and functions of the Coq standard library so that, for instance, a HOL-Light theorem on HOL-Light real numbers is translated into a Coq theorem on Coq real numbers. The provided theorems can therefore be readily reused and combined with other Coq developments based on the Coq standard library.
 
-It contains 2897 theorems including theorems on arithmetic,
-wellfounded relations, lists, real numbers, integers, basic set
-theory, etc.
+It contains 17500 theorems on arithmetic, wellfounded relations,
+lists, real numbers, integers, basic set theory, permutations, group
+theory, matroids, metric spaces, homology, vectors, determinants,
+topology, convex sets and functions, paths, polytopes, Brouwer degree,
+derivatives, Clifford algebra, integration, measure theory, complex
+numbers and analysis, transcendental numbers, real analysis, complex
+line integrals, etc. See HOL-Light files for more details.
 
 As HOL-Light is based on classical higher-order logic with choice, this library uses the following standard set of axioms in Coq:
 
@@ -21,7 +25,7 @@ The translated theorems are provided as axioms in order to have fast Require's b
 
 **Installation using [opam](https://opam.ocaml.org/)**
 
-dependencies: [coq-hol-light-real](https://github.com/Deducteam/coq-hol-light-real/), [coq-fourcolor-reals](https://github.com/coq-community/fourcolor)
+dependencies: [coq-hol-light-real-with-N](https://github.com/Deducteam/coq-hol-light-real-with-N/), [coq-fourcolor-reals](https://github.com/coq-community/fourcolor)
 
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -37,4 +41,4 @@ Check thm_DIV_DIV.
 
 **Reproducibility**
 
-Run [reproduce](https://github.com/Deducteam/hol2dk/blob/main/reproduce). It takes 70 minutes with 32 processors Intel Core i9-13950HX and 64 Gb RAM. If every thing works well, the proofs will be in the directory `tmp/output`.
+Run [reproduce](https://github.com/Deducteam/hol2dk/blob/main/reproduce). It takes 35 hours with 32 processors Intel Core i9-13950HX and 128 Gb RAM. If every thing works well, the proofs will be in the directory `tmp/output`.

erasing.lp → With_N.lp

@@ -29,17 +29,17 @@ builtin "ex_def" ≔ ∃_def;
 builtin "not" ≔ ¬;
 builtin "not_def" ≔ ¬_def;
 
-builtin "True" ≔ T;
-builtin "T_def" ≔ T_def;
+builtin "True" ≔ ⊤;
+builtin "T_def" ≔ ⊤_def;
 
-builtin "False" ≔ F;
-builtin "F_def" ≔ F_def;
+builtin "False" ≔ ⊥;
+builtin "F_def" ≔ ⊥_def;
 
 builtin "ex1" ≔ ∃₁;
 builtin "ex1_def" ≔ ∃₁_def;
 
 // natural deduction rules
-builtin "Logic.I" ≔ Tᵢ;
+builtin "Logic.I" ≔ ⊤ᵢ;
 builtin "conj" ≔ ∧ᵢ;
 builtin "proj1" ≔ ∧ₑ₁;
 builtin "proj2" ≔ ∧ₑ₂;
@@ -93,9 +93,9 @@ builtin "IND_SUC" ≔ IND_SUC;
 builtin "IND_0" ≔ IND_0;
 
 // type of natural numbers
-builtin "nat" ≔ num;
-builtin "0" ≔ _0;
-builtin "S" ≔ SUC;
+builtin "N" ≔ num;
+builtin "0%N" ≔ _0;
+builtin "N.succ" ≔ SUC;
 builtin "mk_num" ≔ mk_num;
 builtin "dest_num" ≔ dest_num;
 builtin "NUM_REP" ≔ NUM_REP;
@@ -108,39 +108,39 @@ builtin "axiom_8" ≔ axiom_8;
 builtin "BIT0" ≔ BIT0;
 builtin "BIT0_def" ≔ BIT0_def;
 builtin "BIT1" ≔ BIT1;
-builtin "Nat.pred" ≔ PRE;
+builtin "N.pred" ≔ PRE;
 builtin "PRE_def" ≔ PRE_def;
-builtin "Nat.add" ≔ +;
+builtin "N.add" ≔ +;
 builtin "add_def" ≔ +_def;
-builtin "Nat.mul" ≔ *;
+builtin "N.mul" ≔ *;
 builtin "mul_def" ≔ *_def;
-builtin "Nat.pow" ≔ EXP;
+builtin "N.pow" ≔ EXP;
 builtin "EXP_def" ≔ EXP_def;
-builtin "Peano.le" ≔ <=;
+builtin "N.le" ≔ <=;
 builtin "le_def" ≔ <=_def;
-builtin "Peano.lt" ≔ <;
+builtin "N.lt" ≔ <;
 builtin "lt_def" ≔ <_def;
-builtin "Peano.ge" ≔ >=;
+builtin "N.ge" ≔ >=;
 builtin "ge_def" ≔ >=_def;
-builtin "Peano.gt" ≔ >;
+builtin "N.gt" ≔ >;
 builtin "gt_def" ≔ >_def;
 builtin "COND" ≔ COND;
-builtin "Nat.max" ≔ MAX;
+builtin "N.max" ≔ MAX;
 builtin "MAX_def" ≔ MAX_def;
-builtin "Nat.min" ≔ MIN;
+builtin "N.min" ≔ MIN;
 builtin "MIN_def" ≔ MIN_def;
-builtin "Nat.sub" ≔ -;
+builtin "N.sub" ≔ -;
 builtin "minus_def" ≔ -_def;
-builtin "Factorial.fact" ≔ FACT;
-builtin "FACT_def" ≔ FACT_def;
-builtin "Nat.div" ≔ DIV;
+//builtin "Factorial.fact" ≔ FACT;
+//builtin "FACT_def" ≔ FACT_def;
+builtin "N.div" ≔ DIV;
 builtin "DIV_def" ≔ DIV_def;
-builtin "Nat.modulo" ≔ MOD;
+builtin "N.modulo" ≔ MOD;
 builtin "MOD_def" ≔ MOD_def;
-builtin "Coq.Arith.PeanoNat.Nat.Even" ≔ EVEN;
-builtin "EVEN_def" ≔ EVEN_def;
-builtin "Coq.Arith.PeanoNat.Nat.Odd" ≔ ODD;
-builtin "ODD_def" ≔ ODD_def;
+//builtin "N.Even" ≔ EVEN;
+//builtin "EVEN_def" ≔ EVEN_def;
+//builtin "N.Odd" ≔ ODD;
+//builtin "ODD_def" ≔ ODD_def;
 
 // indtypes
 builtin "NUMLEFT" ≔ NUMLEFT; // not mandatory
@@ -191,8 +191,8 @@ builtin "List.app" ≔ APPEND;
 builtin "APPEND_def" ≔ APPEND_def;
 builtin "List.rev" ≔ REVERSE;
 builtin "REVERSE_def" ≔ REVERSE_def;
-builtin "List.length" ≔ LENGTH;
-builtin "LENGTH_def" ≔ LENGTH_def;
+//builtin "List.length" ≔ LENGTH;
+//builtin "LENGTH_def" ≔ LENGTH_def;
 builtin "List.map" ≔ MAP;
 builtin "MAP_def" ≔ MAP_def;
 builtin "List.removelast" ≔ BUTLAST;
@@ -205,8 +205,8 @@ builtin "PAIRWISE_def" ≔ PAIRWISE_def;
 //builtin "FILTER_def" ≔ FILTER_def;
 builtin "List.In" ≔ MEM;
 builtin "MEM_def" ≔ MEM_def;
-builtin "repeat_with_perm_args" ≔ REPLICATE;
-builtin "REPLICATE_def" ≔ REPLICATE_def;
+//builtin "repeat_with_perm_args" ≔ REPLICATE;
+//builtin "REPLICATE_def" ≔ REPLICATE_def;
 //builtin "fold_right_with_perm_args" ≔ ITLIST;
 //builtin "ITLIST_def" ≔ ITLIST_def;
 builtin "hd" ≔ HD;
@@ -275,10 +275,10 @@ builtin "Rinv" ≔ real_inv;
 builtin "real_inv_def" ≔ real_inv_def;
 builtin "Ropp" ≔ real_neg;
 builtin "real_neg_def" ≔ real_neg_def;
-builtin "INR" ≔ real_of_num;
+builtin "R_of_N" ≔ real_of_num;
 builtin "real_of_num_def" ≔ real_of_num_def;
-builtin "Rpower_nat" ≔ real_pow;
-builtin "real_pow_def" ≔ real_pow_def;
+//builtin "Rpower_nat" ≔ real_pow;
+//builtin "real_pow_def" ≔ real_pow_def;
 builtin "Rabs" ≔ real_abs;
 builtin "real_abs_def" ≔ real_abs_def;
 builtin "Rdiv" ≔ real_div;
@@ -304,6 +304,8 @@ builtin "axiom_25" ≔ axiom_25;
 builtin "axiom_26" ≔ axiom_26;
 //TODO: builtin "div" ≔ div;
 //TODO: builtin "rem" ≔ rem;
+builtin "Z_of_N" ≔ int_of_num;
+builtin "int_of_num_def" ≔ int_of_num_def;
 
 // finite_image
 builtin "finite_image" ≔ finite_image;
@@ -353,3 +355,52 @@ builtin "_mk_tybit1" ≔ _mk_tybit1;
 builtin "_dest_tybit1" ≔ _dest_tybit1;
 builtin "axiom_39" ≔ axiom_39;
 builtin "axiom_40" ≔ axiom_40;
+
+// frag
+builtin "frag" ≔ frag;
+builtin "mk_frag" ≔ mk_frag;
+builtin "dest_frag" ≔ dest_frag;
+builtin "axiom_41" ≔ axiom_41;
+builtin "axiom_42" ≔ axiom_42;
+
+// group
+builtin "Group" ≔ Group;
+builtin "group" ≔ group;
+builtin "group_operations" ≔ group_operations;
+builtin "axiom_43" ≔ axiom_43;
+builtin "axiom_44" ≔ axiom_44;
+
+// matroid
+builtin "Matroid" ≔ Matroid;
+builtin "matroid" ≔ matroid;
+builtin "dest_matroid" ≔ dest_matroid;
+builtin "axiom_45" ≔ axiom_45;
+builtin "axiom_46" ≔ axiom_46;
+
+// topology
+builtin "Topology" ≔ Topology;
+builtin "topology" ≔ topology;
+builtin "open_in" ≔ open_in;
+builtin "axiom_47" ≔ axiom_47;
+builtin "axiom_48" ≔ axiom_48;
+
+// net
+builtin "net" ≔ net;
+builtin "mk_net" ≔ mk_net;
+builtin "dest_net" ≔ dest_net;
+builtin "axiom_49" ≔ axiom_49;
+builtin "axiom_50" ≔ axiom_50;
+
+// metric_space
+builtin "Metric" ≔ Metric;
+builtin "metric" ≔ metric;
+builtin "dest_metric" ≔ dest_metric;
+builtin "axiom_51" ≔ axiom_51;
+builtin "axiom_52" ≔ axiom_52;
+
+// multivector
+builtin "Multivector" ≔ Multivector;
+builtin "mk_multivector" ≔ mk_multivector;
+builtin "dest_multivector" ≔ dest_multivector;
+builtin "axiom_53" ≔ axiom_53;
+builtin "axiom_54" ≔ axiom_54;

With_N.mk

@@ -0,0 +1 @@
+With_N.vo: