[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>

7 files changed, 114 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 8a0265438a..75f14bb4da 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -41,6 +41,10 @@ Declare Scope bool_scope.
 Delimit Scope bool_scope with bool.
 Bind Scope bool_scope with bool.
 
+Register bool as core.bool.type.
+Register true as core.bool.true.
+Register false as core.bool.false.
+
 (** Basic boolean operators *)
 
 Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
@@ -62,6 +66,11 @@ Definition negb (b:bool) := if b then false else true.
 Infix "||" := orb : bool_scope.
 Infix "&&" := andb : bool_scope.
 
+Register andb as core.bool.andb.
+Register orb as core.bool.orb.
+Register xorb as core.bool.xorb.
+Register negb as core.bool.negb.
+
 (** Basic properties of [andb] *)
 
 Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
@@ -70,6 +79,8 @@ Proof.
 Qed.
 Hint Resolve andb_prop: bool.
 
+Register andb_prop as core.bool.andb_prop.
+
 Lemma andb_true_intro :
   forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
 Proof.
@@ -77,12 +88,16 @@ Proof.
 Qed.
 Hint Resolve andb_true_intro: bool.
 
+Register andb_true_intro as core.bool.andb_true_intro.
+
 (** Interpretation of booleans as propositions *)
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
 Hint Constructors eq_true : eq_true.
 
+Register eq_true as core.eq_true.type.
+
 (** Another way of interpreting booleans as propositions *)
 
 Definition is_true b := b = true.
@@ -141,6 +156,9 @@ Delimit Scope nat_scope with nat.
 Bind Scope nat_scope with nat.
 Arguments S _%nat.
 
+Register nat as num.nat.type.
+Register O as num.nat.O.
+Register S as num.nat.S.
 
 (********************************************************************)
 (** * Container datatypes *)
@@ -156,6 +174,10 @@ Inductive option (A:Type) : Type :=
 Arguments Some {A} a.
 Arguments None {A}.
 
+Register option as core.option.type.
+Register Some as core.option.Some.
+Register None as core.option.None.
+
 Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
   match o with
     | Some a => @Some B (f a)
@@ -187,11 +209,19 @@ Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
 Arguments pair {A B} _ _.
 
+Register prod as core.prod.type.
+Register pair as core.prod.intro.
+Register prod_rect as core.prod.rect.
+
 Section projections.
   Context {A : Type} {B : Type}.
 
   Definition fst (p:A * B) := match p with (x, y) => x end.
   Definition snd (p:A * B) := match p with (x, y) => y end.
+
+  Register fst as core.prod.proj1.
+  Register snd as core.prod.proj2.
+
 End projections.
 
 Hint Resolve pair inl inr: core.
@@ -239,6 +269,10 @@ Bind Scope list_scope with list.
 
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 
+Register list as core.list.type.
+Register nil as core.list.nil.
+Register cons as core.list.cons.
+
 Local Open Scope list_scope.
 
 Definition length (A : Type) : list A -> nat :=
@@ -269,6 +303,11 @@ Inductive comparison : Set :=
   | Lt : comparison
   | Gt : comparison.
 
+Register comparison as core.comparison.type.
+Register Eq as core.comparison.Eq.
+Register Lt as core.comparison.Lt.
+Register Gt as core.comparison.Gt.
+
 Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
 Proof.
   destruct c, c'; intro H; reflexivity || destruct H; discriminate.
@@ -353,6 +392,10 @@ Arguments identity_ind [A] a P f y i.
 Arguments identity_rec [A] a P f y i.
 Arguments identity_rect [A] a P f y i.
 
+Register identity as core.identity.type.
+Register identity_refl as core.identity.refl.
+Register identity_ind as core.identity.ind.
+
 (** Identity type *)
 
 Definition ID := forall A:Type, A -> A.
@@ -361,6 +404,8 @@ Definition id : ID := fun A x => x.
 Definition IDProp := forall A:Prop, A -> A.
 Definition idProp : IDProp := fun A x => x.
 
+Register IDProp as core.IDProp.type.
+Register idProp as core.IDProp.idProp.
 
 (* begin hide *)
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4ec0049a9c..1db0a8e1b5 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -21,14 +21,21 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Inductive True : Prop :=
   I : True.
 
+Register True as core.True.type.
+Register I as core.True.I.
+
 (** [False] is the always false proposition *)
 Inductive False : Prop :=.
 
+Register False as core.False.type.
+
 (** [not A], written [~A], is the negation of [A] *)
 Definition not (A:Prop) := A -> False.
 
 Notation "~ x" := (not x) : type_scope.
 
+Register not as core.not.type.
+
 (** Create the "core" hint database, and set its transparent state for
   variables and constants explicitely. *)
 
@@ -50,6 +57,9 @@ Inductive and (A B:Prop) : Prop :=
 
 where "A /\ B" := (and A B) : type_scope.
 
+Register and as core.and.type.
+Register conj as core.and.conj.
+
 Section Conjunction.
 
   Variables A B : Prop.
@@ -77,12 +87,18 @@ where "A \/ B" := (or A B) : type_scope.
 Arguments or_introl [A B] _, [A] B _.
 Arguments or_intror [A B] _, A [B] _.
 
+Register or as core.or.type.
+
 (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
 
 Definition iff (A B:Prop) := (A -> B) /\ (B -> A).
 
 Notation "A <-> B" := (iff A B) : type_scope.
 
+Register iff as core.iff.type.
+Register proj1 as core.iff.proj1.
+Register proj2 as core.iff.proj2.
+
 Section Equivalence.
 
 Theorem iff_refl : forall A:Prop, A <-> A.
@@ -257,6 +273,8 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
 Inductive ex (A:Type) (P:A -> Prop) : Prop :=
   ex_intro : forall x:A, P x -> ex (A:=A) P.
 
+Register ex as core.ex.type.
+
 Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
   ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
 
@@ -333,6 +351,11 @@ Hint Resolve I conj or_introl or_intror : core.
 Hint Resolve eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
 
+Register eq as core.eq.type.
+Register eq_refl as core.eq.refl.
+Register eq_ind as core.eq.ind.
+Register eq_rect as core.eq.rect.
+
 Section Logic_lemmas.
 
   Theorem absurd : forall A C:Prop, A -> ~ A -> C.
@@ -351,16 +374,22 @@ Section Logic_lemmas.
       destruct 1; trivial.
     Defined.
 
+    Register eq_sym as core.eq.sym.
+
     Theorem eq_trans : x = y -> y = z -> x = z.
     Proof.
       destruct 2; trivial.
     Defined.
 
+    Register eq_trans as core.eq.trans.
+
     Theorem f_equal : x = y -> f x = f y.
     Proof.
       destruct 1; trivial.
     Defined.
 
+    Register f_equal as core.eq.congr.
+
     Theorem not_eq_sym : x <> y -> y <> x.
     Proof.
       red; intros h1 h2; apply h1; destruct h2; trivial.
@@ -373,6 +402,8 @@ Section Logic_lemmas.
     intros A x P H y H0. elim eq_sym with (1 := H0); assumption.
   Defined.
 
+  Register eq_ind_r as core.eq.ind_r.
+
   Definition eq_rec_r :
     forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
     intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
@@ -458,6 +489,8 @@ Proof.
   destruct 1; destruct 1; reflexivity.
 Qed.
 
+Register f_equal2 as core.eq.congr2.
+
 Theorem f_equal3 :
   forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
     (x2 y2:A2) (x3 y3:A3),
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 6f10a93997..587de12a15 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -51,6 +51,11 @@ Section identity_is_a_congruence.
 
 End identity_is_a_congruence.
 
+Register identity_sym as core.identity.sym.
+Register identity_trans as core.identity.trans.
+Register identity_congr as core.identity.congr.
+
+
 Definition identity_ind_r :
   forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
  intros A x P H y H0; case identity_sym with (1 := H0); trivial.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index eb4ba0e5e6..7e7a1ced58 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -42,6 +42,8 @@ Definition pred n :=
     | S u => u
   end.
 
+Register pred as num.nat.pred.
+
 Fixpoint add n m :=
   match n with
   | 0 => m
@@ -50,6 +52,8 @@ Fixpoint add n m :=
 
 where "n + m" := (add n m) : nat_scope.
 
+Register add as num.nat.add.
+
 Definition double n := n + n.
 
 Fixpoint mul n m :=
@@ -60,6 +64,8 @@ Fixpoint mul n m :=
 
 where "n * m" := (mul n m) : nat_scope.
 
+Register mul as num.nat.mul.
+
 (** Truncated subtraction: [n-m] is [0] if [n<=m] *)
 
 Fixpoint sub n m :=
@@ -70,6 +76,8 @@ Fixpoint sub n m :=
 
 where "n - m" := (sub n m) : nat_scope.
 
+Register sub as num.nat.sub.
+
 (** ** Comparisons *)
 
 Fixpoint eqb n m : bool :=
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 65e5e76a22..4489f4cb15 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -182,6 +182,11 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 
+Register le as num.nat.le.
+Register lt as num.nat.lt.
+Register ge as num.nat.ge.
+Register gt as num.nat.gt.
+
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
 induction 1; auto. destruct m; simpl; auto.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index a5f926f7ab..e4796a8059 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -27,6 +27,10 @@ Require Import Logic.
 Inductive sig (A:Type) (P:A -> Prop) : Type :=
     exist : forall x:A, P x -> sig P.
 
+Register sig as core.sig.type.
+Register exist as core.sig.intro.
+Register sig_rect as core.sig.rect.
+
 Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
     exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
@@ -36,6 +40,10 @@ Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
 Inductive sigT (A:Type) (P:A -> Type) : Type :=
     existT : forall x:A, P x -> sigT P.
 
+Register sigT as core.sigT.type.
+Register existT as core.sigT.intro.
+Register sigT_rect as core.sigT.rect.
+
 Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
     existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
 
@@ -93,6 +101,9 @@ Section Subset_projections.
     | exist _ a b => b
     end.
 
+  Register proj1_sig as core.sig.proj1.
+  Register proj2_sig as core.sig.proj2.
+
 End Subset_projections.
 
 
@@ -152,6 +163,9 @@ Section Projections.
     | existT _ _ h => h
     end.
 
+  Register projT1 as core.sigT.proj1.
+  Register projT2 as core.sigT.proj2.
+
 End Projections.
 
 Local Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ;  '/  ' y )").
@@ -681,6 +695,8 @@ Add Printing If sumbool.
 Arguments left {A B} _, [A] B _.
 Arguments right {A B} _ , A [B] _.
 
+Register sumbool as core.sumbool.type.
+
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index c27ffa33f8..f4cb34c713 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -42,6 +42,8 @@ Section Well_founded.
 
  Definition well_founded := forall a:A, Acc a.
 
+ Register well_founded as core.wf.well_founded.
+
  (** Well-founded induction on [Set] and [Prop] *)
 
  Hypothesis Rwf : well_founded.