[coqlib] Rebindable Coqlib namespace.

We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.

This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.

Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

4 files changed, 55 insertions, 0 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 1241345338..8fc3ab56c9 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -38,6 +38,14 @@ Module Z
 
 Include BinIntDef.Z.
 
+Register add as num.Z.add.
+Register opp as num.Z.opp.
+Register succ as num.Z.succ.
+Register pred as num.Z.pred.
+Register sub as num.Z.sub.
+Register mul as num.Z.mul.
+Register of_nat as num.Z.of_nat.
+
 (** When including property functors, only inline t eq zero one two *)
 
 Set Inline Level 30.
@@ -68,6 +76,11 @@ Notation "( x | y )" := (divide x y) (at level 0).
 Definition Even a := exists b, a = 2*b.
 Definition Odd a := exists b, a = 2*b+1.
 
+Register le as num.Z.le.
+Register lt as num.Z.lt.
+Register ge as num.Z.ge.
+Register gt as num.Z.gt.
+
 (** * Decidability of equality. *)
 
 Definition eq_dec (x y : Z) : {x = y} + {x <> y}.
@@ -477,6 +490,10 @@ Qed.
 
 Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
+Register eq_decidable as num.Z.eq_decidable.
+Register le_decidable as num.Z.le_decidable.
+Register lt_decidable as num.Z.lt_decidable.
+
 
 (** ** Specification of absolute value *)
 
@@ -1752,6 +1769,8 @@ weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos)
 
 Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *)
 
+Register Zne as plugins.omega.Zne.
+
 Ltac elim_compare com1 com2 :=
   case (Dcompare (com1 ?= com2)%Z);
     [ idtac | let x := fresh "H" in
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 5c960da1fb..776efa2978 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -609,6 +609,8 @@ Proof.
  destruct n. trivial. simpl. apply Pos2Z.inj_succ.
 Qed.
 
+Register inj_succ as num.Nat2Z.inj_succ.
+
 (** [Z.of_N] produce non-negative integers *)
 
 Lemma is_nonneg n : 0 <= Z.of_nat n.
@@ -676,11 +678,15 @@ Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_add, N2Z.inj_add.
 Qed.
 
+Register inj_add as num.Nat2Z.inj_add.
+
 Lemma inj_mul n m : Z.of_nat (n*m) = Z.of_nat n * Z.of_nat m.
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_mul, N2Z.inj_mul.
 Qed.
 
+Register inj_mul as num.Nat2Z.inj_mul.
+
 Lemma inj_sub_max n m : Z.of_nat (n-m) = Z.max 0 (Z.of_nat n - Z.of_nat m).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub_max.
@@ -692,6 +698,8 @@ Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub.
 Qed.
 
+Register inj_sub as num.Nat2Z.inj_sub.
+
 Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max.
@@ -951,6 +959,14 @@ Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m).
 Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m).
 Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m).
 
+Register neq as plugins.omega.neq.
+Register inj_eq as plugins.omega.inj_eq.
+Register inj_neq as plugins.omega.inj_neq.
+Register inj_le as plugins.omega.inj_le.
+Register inj_lt as plugins.omega.inj_lt.
+Register inj_ge as plugins.omega.inj_ge.
+Register inj_gt as plugins.omega.inj_gt.
+
 (** For the others, a Notation is fine *)
 
 Notation inj_0 := Nat2Z.inj_0 (only parsing).
@@ -1017,3 +1033,5 @@ Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0.
 Proof.
  intros. rewrite not_le_minus_0; auto with arith.
 Qed.
+
+Register inj_minus2 as plugins.omega.inj_minus2.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 208e84aeb7..bd460f77f0 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -64,6 +64,11 @@ Proof.
   apply Z.lt_gt_cases.
 Qed.
 
+Register dec_Zne as plugins.omega.dec_Zne.
+Register dec_Zgt as plugins.omega.dec_Zgt.
+Register dec_Zge as plugins.omega.dec_Zge.
+Register not_Zeq as plugins.omega.not_Zeq.
+
 (** * Relating strict and large orders *)
 
 Notation Zgt_lt := Z.gt_lt (compat "8.7").
@@ -119,6 +124,12 @@ Proof.
   destruct (Z.eq_decidable n m); [assumption|now elim H].
 Qed.
 
+Register Znot_le_gt as plugins.omega.Znot_le_gt.
+Register Znot_lt_ge as plugins.omega.Znot_lt_ge.
+Register Znot_ge_lt as plugins.omega.Znot_ge_lt.
+Register Znot_gt_le as plugins.omega.Znot_gt_le.
+Register not_Zne as plugins.omega.not_Zne.
+
 (** * Equivalence and order properties *)
 
 (** Reflexivity *)
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 306a856381..fd357502d2 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -94,3 +94,10 @@ Proof.
  now apply Z.add_lt_mono_l.
 Qed.
 
+Register Zegal_left as plugins.omega.Zegal_left.
+Register Zne_left as plugins.omega.Zne_left.
+Register Zlt_left as plugins.omega.Zlt_left.
+Register Zgt_left as plugins.omega.Zgt_left.
+Register Zle_left as plugins.omega.Zle_left.
+Register Zge_left as plugins.omega.Zge_left.
+Register Zmult_le_approx as plugins.omega.Zmult_le_approx.