renaming of some files (#8)

Deducteam · Jan 18, 2025 · f5b1a89 · f5b1a89
1 parent cf07bf7
commit f5b1a89
Show file tree

Hide file tree

Showing 11 changed files with 29 additions and 28 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -5,12 +5,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ## Unreleased
 
-- HOLLight_Real.Quotient: remove Local Definition of a
+- renamings of HOLLight_Real into mappings, erasing.lp into mappings.lp
+- section Mappings.Quotient: remove Local Definition of a
 - hol_upto_real.ml: update wrt HOL-Light 3.0
-- erasing.lp: update wrt https://github.com/Deducteam/hol2dk/pull/161 and https://github.com/Deducteam/hol2dk/pull/149
+- mappings.lp: update wrt https://github.com/Deducteam/hol2dk/pull/161 and https://github.com/Deducteam/hol2dk/pull/149
 - reproduce: update hollight, hol2dk and lambdapi versions
 - reproduce: add stage mechanism to run reproduce again by skipping stages that succeeded
-- terms.v, theorems.v: type arguments have readable names now
+- add file mappings.mk for the local dependencies of mappings.v
 
 ## 1.0.0 (2024-11-03)
 

diff --git a/CONFIG b/CONFIG
@@ -1,2 +1,2 @@
 #!/bin/sh
-hol2dk config hol_upto_real.ml HOLLight_Real HOLLight_Real.v deps.mk erasing.lp
+hol2dk config hol_upto_real.ml HOLLight_Real_With_nat mappings.v mappings.mk mappings.lp
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-LIBNAME=HOLLight_Real
+LIBNAME=HOLLight_Real_With_nat
 
 .SUFFIXES:
 

diff --git a/coq-hol-light-real.opam b/coq-hol-light-real.opam
@@ -20,6 +20,6 @@ tags: [
   "keyword:HOL-Light"
   "category:Math/Arith/Misc"
   "category:Math/Arith/Real numbers"
-  "date:2024-11-03"
-  "logpath:HOLLight_Real"
+  "date:2025-01-18"
+  "logpath:HOLLight_Real_With_nat"
 ]
diff --git a/erasing.lp → mappings.lp b/erasing.lp → mappings.lp
diff --git a/deps.mk → mappings.mk b/deps.mk → mappings.mk
diff --git a/HOLLight_Real.v → mappings.v b/HOLLight_Real.v → mappings.v
diff --git a/reproduce b/reproduce
@@ -15,7 +15,7 @@ coq_version=8.20.0
 
 base=hol_upto_real
 dump_simp_option=-before-hol
-root_path=HOLLight_Real
+root_path=HOLLight_Real_With_nat
 jobs='-j32'
 
 line() { echo '------------------------------------------------------------'; }
@@ -96,7 +96,7 @@ translate_proofs() {
     mkdir -p output
     cd output
     if test -f Makefile; then make $jobs clean-all; fi
-    hol2dk config $base.ml $root_path ../../HOLLight_Real.v ../../deps.mk ../../erasing.lp
+    hol2dk config $base.ml $root_path ../../mappings.v ../../mappings.mk ../../mappings.lp
     make split
     make $jobs lp
     make $jobs v
@@ -121,7 +121,7 @@ create_and_check_opam_library() {
     sed -e "s/${base}_//g" -e "/^Require Import ${root_path}.types.$/d" ${base}_terms.v > ../opam/terms.v
     sed -e "s/${base}_//g" -e "/^Require Import ${root_path}.types.$/d" -e '/^Require Import ${root_path}.axioms.$/d' ${base}_opam.v > ../opam/theorems.v
     cd ../opam
-    cp ../../$root_path.v ../../Makefile .
+    cp ../../mappings.v ../../Makefile .
     make
     cd ..
 }

diff --git a/terms.v b/terms.v
@@ -1,5 +1,5 @@
-Require Import HOLLight_Real.
-Require Import HOLLight_Real.theory_hol.
+Require Import HOLLight_Real_With_nat.mappings.
+Require Import HOLLight_Real_With_nat.theory_hol.
 Definition _FALSITY_ : Prop := False.
 Lemma _FALSITY__def : _FALSITY_ = False.
 Proof. exact (eq_refl _FALSITY_). Qed.

diff --git a/theorems.v b/theorems.v
@@ -1,6 +1,6 @@
-Require Import HOLLight_Real.
-Require Import HOLLight_Real.theory_hol.
-Require Import HOLLight_Real.terms.
+Require Import HOLLight_Real_With_nat.mappings.
+Require Import HOLLight_Real_With_nat.theory_hol.
+Require Import HOLLight_Real_With_nat.terms.
 Axiom thm_T_DEF : True = ((fun p : Prop => p) = (fun p : Prop => p)).
 Axiom thm_AND_DEF : and = (fun p : Prop => fun q : Prop => (fun f : Prop -> Prop -> Prop => f p q) = (fun f : Prop -> Prop -> Prop => f True True)).
 Axiom thm_IMP_DEF : imp = (fun p : Prop => fun q : Prop => (p /\ q) = p).
@@ -692,7 +692,7 @@ Axiom thm_BOUNDS_LINEAR : forall A : nat, forall B : nat, forall C : nat, (foral
 Axiom thm_BOUNDS_LINEAR_0 : forall A : nat, forall B : nat, (forall n : nat, Peano.le (Nat.mul A n) B) = (A = (NUMERAL 0)).
 Axiom thm_BOUNDS_DIVIDED : forall P : nat -> nat, (exists B : nat, forall n : nat, Peano.le (P n) B) = (exists A : nat, exists B : nat, forall n : nat, Peano.le (Nat.mul n (P n)) (Nat.add (Nat.mul A n) B)).
 Axiom thm_BOUNDS_NOTZERO : forall P : nat -> nat -> nat, forall A : nat, forall B : nat, (((P (NUMERAL 0) (NUMERAL 0)) = (NUMERAL 0)) /\ (forall m : nat, forall n : nat, Peano.le (P m n) (Nat.add (Nat.mul A (Nat.add m n)) B))) -> exists B' : nat, forall m : nat, forall n : nat, Peano.le (P m n) (Nat.mul B' (Nat.add m n)).
-Axiom thm_BOUNDS_IGNORE : forall P : nat -> nat, forall Q : nat -> nat, (exists B : nat, forall i : nat, Peano.le (P i) (Nat.add (Q i) B)) = (exists B : nat, exists N : nat, forall i : nat, (Peano.le N i) -> Peano.le (P i) (Nat.add (Q i) B)).
+Axiom thm_BOUNDS_IGNORE : forall P : nat -> nat, forall Q : nat -> nat, (exists B : nat, forall i : nat, Peano.le (P i) (Nat.add (Q i) B)) = (exists B : nat, exists N' : nat, forall i : nat, (Peano.le N' i) -> Peano.le (P i) (Nat.add (Q i) B)).
 Axiom thm_is_nadd : forall x : nat -> nat, (is_nadd x) = (exists B : nat, forall m : nat, forall n : nat, Peano.le (dist (@pair nat nat (Nat.mul m (x n)) (Nat.mul n (x m)))) (Nat.mul B (Nat.add m n))).
 Axiom thm_is_nadd_0 : is_nadd (fun n : nat => NUMERAL 0).
 Axiom thm_NADD_CAUCHY : forall x : nadd, exists B : nat, forall m : nat, forall n : nat, Peano.le (dist (@pair nat nat (Nat.mul m (dest_nadd x n)) (Nat.mul n (dest_nadd x m)))) (Nat.mul B (Nat.add m n)).
@@ -747,23 +747,23 @@ Axiom thm_NADD_LE_RMUL : forall x : nadd, forall y : nadd, forall z : nadd, (nad
 Axiom thm_NADD_LE_RADD : forall x : nadd, forall y : nadd, forall z : nadd, (nadd_le (nadd_add x z) (nadd_add y z)) = (nadd_le x y).
 Axiom thm_NADD_LE_LADD : forall x : nadd, forall y : nadd, forall z : nadd, (nadd_le (nadd_add x y) (nadd_add x z)) = (nadd_le y z).
 Axiom thm_NADD_RDISTRIB : forall x : nadd, forall y : nadd, forall z : nadd, nadd_eq (nadd_mul (nadd_add x y) z) (nadd_add (nadd_mul x z) (nadd_mul y z)).
-Axiom thm_NADD_ARCH_MULT : forall x : nadd, forall k : nat, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N : nat, nadd_le (nadd_of_num k) (nadd_mul (nadd_of_num N) x).
+Axiom thm_NADD_ARCH_MULT : forall x : nadd, forall k : nat, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N' : nat, nadd_le (nadd_of_num k) (nadd_mul (nadd_of_num N') x).
 Axiom thm_NADD_ARCH_ZERO : forall x : nadd, forall k : nadd, (forall n : nat, nadd_le (nadd_mul (nadd_of_num n) x) k) -> nadd_eq x (nadd_of_num (NUMERAL 0)).
 Axiom thm_NADD_ARCH_LEMMA : forall x : nadd, forall y : nadd, forall z : nadd, (forall n : nat, nadd_le (nadd_mul (nadd_of_num n) x) (nadd_add (nadd_mul (nadd_of_num n) y) z)) -> nadd_le x y.
 Axiom thm_NADD_COMPLETE : forall P : nadd -> Prop, ((exists x : nadd, P x) /\ (exists M : nadd, forall x : nadd, (P x) -> nadd_le x M)) -> exists M : nadd, (forall x : nadd, (P x) -> nadd_le x M) /\ (forall M' : nadd, (forall x : nadd, (P x) -> nadd_le x M') -> nadd_le M M').
-Axiom thm_NADD_UBOUND : forall x : nadd, exists B : nat, exists N : nat, forall n : nat, (Peano.le N n) -> Peano.le (dest_nadd x n) (Nat.mul B n).
-Axiom thm_NADD_NONZERO : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N : nat, forall n : nat, (Peano.le N n) -> ~ ((dest_nadd x n) = (NUMERAL 0)).
-Axiom thm_NADD_LBOUND : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists A : nat, exists N : nat, forall n : nat, (Peano.le N n) -> Peano.le n (Nat.mul A (dest_nadd x n)).
+Axiom thm_NADD_UBOUND : forall x : nadd, exists B : nat, exists N' : nat, forall n : nat, (Peano.le N' n) -> Peano.le (dest_nadd x n) (Nat.mul B n).
+Axiom thm_NADD_NONZERO : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N' : nat, forall n : nat, (Peano.le N' n) -> ~ ((dest_nadd x n) = (NUMERAL 0)).
+Axiom thm_NADD_LBOUND : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists A : nat, exists N' : nat, forall n : nat, (Peano.le N' n) -> Peano.le n (Nat.mul A (dest_nadd x n)).
 Axiom thm_nadd_rinv : forall x : nadd, (nadd_rinv x) = (fun n : nat => Nat.div (Nat.mul n n) (dest_nadd x n)).
 Axiom thm_NADD_MUL_LINV_LEMMA0 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists A : nat, exists B : nat, forall n : nat, Peano.le (nadd_rinv x n) (Nat.add (Nat.mul A n) B).
 Axiom thm_NADD_MUL_LINV_LEMMA1 : forall x : nadd, forall n : nat, (~ ((dest_nadd x n) = (NUMERAL 0))) -> Peano.le (dist (@pair nat nat (Nat.mul (dest_nadd x n) (nadd_rinv x n)) (Nat.mul n n))) (dest_nadd x n).
-Axiom thm_NADD_MUL_LINV_LEMMA2 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N : nat, forall n : nat, (Peano.le N n) -> Peano.le (dist (@pair nat nat (Nat.mul (dest_nadd x n) (nadd_rinv x n)) (Nat.mul n n))) (dest_nadd x n).
-Axiom thm_NADD_MUL_LINV_LEMMA3 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N : nat, forall m : nat, forall n : nat, (Peano.le N n) -> Peano.le (dist (@pair nat nat (Nat.mul m (Nat.mul (dest_nadd x m) (Nat.mul (dest_nadd x n) (nadd_rinv x n)))) (Nat.mul m (Nat.mul (dest_nadd x m) (Nat.mul n n))))) (Nat.mul m (Nat.mul (dest_nadd x m) (dest_nadd x n))).
-Axiom thm_NADD_MUL_LINV_LEMMA4 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N : nat, forall m : nat, forall n : nat, ((Peano.le N m) /\ (Peano.le N n)) -> Peano.le (Nat.mul (Nat.mul (dest_nadd x m) (dest_nadd x n)) (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m))))) (Nat.add (Nat.mul (Nat.mul m n) (dist (@pair nat nat (Nat.mul m (dest_nadd x n)) (Nat.mul n (dest_nadd x m))))) (Nat.mul (Nat.mul (dest_nadd x m) (dest_nadd x n)) (Nat.add m n))).
-Axiom thm_NADD_MUL_LINV_LEMMA5 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists B : nat, exists N : nat, forall m : nat, forall n : nat, ((Peano.le N m) /\ (Peano.le N n)) -> Peano.le (Nat.mul (Nat.mul (dest_nadd x m) (dest_nadd x n)) (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m))))) (Nat.mul B (Nat.mul (Nat.mul m n) (Nat.add m n))).
-Axiom thm_NADD_MUL_LINV_LEMMA6 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists B : nat, exists N : nat, forall m : nat, forall n : nat, ((Peano.le N m) /\ (Peano.le N n)) -> Peano.le (Nat.mul (Nat.mul m n) (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m))))) (Nat.mul B (Nat.mul (Nat.mul m n) (Nat.add m n))).
-Axiom thm_NADD_MUL_LINV_LEMMA7 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists B : nat, exists N : nat, forall m : nat, forall n : nat, ((Peano.le N m) /\ (Peano.le N n)) -> Peano.le (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m)))) (Nat.mul B (Nat.add m n)).
-Axiom thm_NADD_MUL_LINV_LEMMA7a : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> forall N : nat, exists A : nat, exists B : nat, forall m : nat, forall n : nat, (Peano.le m N) -> Peano.le (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m)))) (Nat.add (Nat.mul A n) B).
+Axiom thm_NADD_MUL_LINV_LEMMA2 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N' : nat, forall n : nat, (Peano.le N' n) -> Peano.le (dist (@pair nat nat (Nat.mul (dest_nadd x n) (nadd_rinv x n)) (Nat.mul n n))) (dest_nadd x n).
+Axiom thm_NADD_MUL_LINV_LEMMA3 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N' : nat, forall m : nat, forall n : nat, (Peano.le N' n) -> Peano.le (dist (@pair nat nat (Nat.mul m (Nat.mul (dest_nadd x m) (Nat.mul (dest_nadd x n) (nadd_rinv x n)))) (Nat.mul m (Nat.mul (dest_nadd x m) (Nat.mul n n))))) (Nat.mul m (Nat.mul (dest_nadd x m) (dest_nadd x n))).
+Axiom thm_NADD_MUL_LINV_LEMMA4 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists N' : nat, forall m : nat, forall n : nat, ((Peano.le N' m) /\ (Peano.le N' n)) -> Peano.le (Nat.mul (Nat.mul (dest_nadd x m) (dest_nadd x n)) (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m))))) (Nat.add (Nat.mul (Nat.mul m n) (dist (@pair nat nat (Nat.mul m (dest_nadd x n)) (Nat.mul n (dest_nadd x m))))) (Nat.mul (Nat.mul (dest_nadd x m) (dest_nadd x n)) (Nat.add m n))).
+Axiom thm_NADD_MUL_LINV_LEMMA5 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists B : nat, exists N' : nat, forall m : nat, forall n : nat, ((Peano.le N' m) /\ (Peano.le N' n)) -> Peano.le (Nat.mul (Nat.mul (dest_nadd x m) (dest_nadd x n)) (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m))))) (Nat.mul B (Nat.mul (Nat.mul m n) (Nat.add m n))).
+Axiom thm_NADD_MUL_LINV_LEMMA6 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists B : nat, exists N' : nat, forall m : nat, forall n : nat, ((Peano.le N' m) /\ (Peano.le N' n)) -> Peano.le (Nat.mul (Nat.mul m n) (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m))))) (Nat.mul B (Nat.mul (Nat.mul m n) (Nat.add m n))).
+Axiom thm_NADD_MUL_LINV_LEMMA7 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists B : nat, exists N' : nat, forall m : nat, forall n : nat, ((Peano.le N' m) /\ (Peano.le N' n)) -> Peano.le (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m)))) (Nat.mul B (Nat.add m n)).
+Axiom thm_NADD_MUL_LINV_LEMMA7a : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> forall N' : nat, exists A : nat, exists B : nat, forall m : nat, forall n : nat, (Peano.le m N') -> Peano.le (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m)))) (Nat.add (Nat.mul A n) B).
 Axiom thm_NADD_MUL_LINV_LEMMA8 : forall x : nadd, (~ (nadd_eq x (nadd_of_num (NUMERAL 0)))) -> exists B : nat, forall m : nat, forall n : nat, Peano.le (dist (@pair nat nat (Nat.mul m (nadd_rinv x n)) (Nat.mul n (nadd_rinv x m)))) (Nat.mul B (Nat.add m n)).
 Axiom thm_nadd_inv : forall x : nadd, (nadd_inv x) = (@COND nadd (nadd_eq x (nadd_of_num (NUMERAL 0))) (nadd_of_num (NUMERAL 0)) (mk_nadd (nadd_rinv x))).
 Axiom thm_NADD_INV : forall x : nadd, (dest_nadd (nadd_inv x)) = (@COND (nat -> nat) (nadd_eq x (nadd_of_num (NUMERAL 0))) (fun n : nat => NUMERAL 0) (nadd_rinv x)).

diff --git a/theory_hol.v b/theory_hol.v
@@ -1,4 +1,4 @@
-Require Import HOLLight_Real.
+Require Import HOLLight_Real_With_nat.mappings.
 Lemma TRANS {a : Type'} {x y z : a} (xy : x = y) (yz : y = z) : x = z.
 Proof. exact (@EQ_MP (x = y) (x = z) (@MK_COMB a Prop (@eq a x) (@eq a x) y z (@eq_refl (a -> Prop) (@eq a x)) yz) xy). Qed.
 Lemma SYM {a : Type'} {x y : a} (xy : x = y) : y = x.