Merge PR #11990: [micromega] use Coqlib.lib_ref to get Coq constants.

Reviewed-by: maximedenes

theories/Init/Datatypes.v

@@ -26,6 +26,8 @@ Inductive Empty_set : Set :=.
 Inductive unit : Set :=
     tt : unit.
 
+Register unit as core.unit.type.
+Register tt as core.unit.tt.
 
 (********************************************************************)
 (** * The boolean datatype *)
@@ -198,6 +200,10 @@ Notation "x + y" := (sum x y) : type_scope.
 Arguments inl {A B} _ , [A] B _.
 Arguments inr {A B} _ , A [B] _.
 
+Register sum as core.sum.type.
+Register inl as core.sum.inl.
+Register inr as core.sum.inr.
+
 (** [prod A B], written [A * B], is the product of [A] and [B];
     the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
 

theories/QArith/QArith_base.v

@@ -22,6 +22,10 @@ Declare Scope Q_scope.
 Delimit Scope Q_scope with Q.
 Bind Scope Q_scope with Q.
 Arguments Qmake _%Z _%positive.
+
+Register Q as rat.Q.type.
+Register Qmake as rat.Q.Qmake.
+
 Open Scope Q_scope.
 Ltac simpl_mult := rewrite ?Pos2Z.inj_mul.
 
@@ -101,6 +105,10 @@ Notation "x > y" := (Qlt y x)(only parsing) : Q_scope.
 Notation "x >= y" := (Qle y x)(only parsing) : Q_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
 
+Register Qeq as rat.Q.Qeq.
+Register Qle as rat.Q.Qle.
+Register Qlt as rat.Q.Qlt.
+
 (** injection from Z is injective. *)
 
 Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b.
@@ -278,6 +286,11 @@ Infix "*" := Qmult : Q_scope.
 Notation "/ x" := (Qinv x) : Q_scope.
 Infix "/" := Qdiv : Q_scope.
 
+Register Qplus  as rat.Q.Qplus.
+Register Qminus as rat.Q.Qminus.
+Register Qopp   as rat.Q.Qopp.
+Register Qmult  as rat.Q.Qmult.
+
 (** A light notation for [Zpos] *)
 
 Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b).
@@ -1053,6 +1066,8 @@ Definition Qpower (q:Q) (z:Z) :=
 
 Notation " q ^ z " := (Qpower q z) : Q_scope.
 
+Register Qpower as  rat.Q.Qpower.
+
 Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower.
 Proof.
 intros x x' Hx y y' Hy. rewrite <- Hy; clear y' Hy.

theories/Reals/Rregisternames.v

@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Reals.
+Require Import Raxioms Rfunctions Qreals.
 
 (*****************************************************************)
 (**           Register names for use in plugins                  *)
@@ -18,6 +18,9 @@ Register R as reals.R.type.
 Register R0 as reals.R.R0.
 Register R1 as reals.R.R1.
 Register Rle as reals.R.Rle.
+Register Rgt as reals.R.Rgt.
+Register Rlt as reals.R.Rlt.
+Register Rge as reals.R.Rge.
 Register Rplus as reals.R.Rplus.
 Register Ropp as reals.R.Ropp.
 Register Rminus as reals.R.Rminus.
@@ -26,5 +29,6 @@ Register Rinv as reals.R.Rinv.
 Register Rdiv as reals.R.Rdiv.
 Register IZR as reals.R.IZR.
 Register Rabs as reals.R.Rabs.
-Register sqrt as reals.R.sqrt.
 Register powerRZ as reals.R.powerRZ.
+Register pow as reals.R.pow.
+Register Qreals.Q2R as reals.R.Q2R.

theories/ZArith/BinInt.v

@@ -44,6 +44,7 @@ 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 pow as num.Z.pow.
 Register of_nat as num.Z.of_nat.
 
 (** When including property functors, only inline t eq zero one two *)

theories/micromega/DeclConstant.v

@@ -35,6 +35,7 @@ Require Import List.
 (** Ground terms (see [GT] below) are built inductively from declared constants. *)
 
 Class DeclaredConstant {T : Type} (F : T).
+Register DeclaredConstant as micromega.DeclaredConstant.type.
 
 Class GT {T : Type} (F : T).
 

theories/micromega/EnvRing.v

@@ -31,6 +31,14 @@ Inductive PExpr {C} : Type :=
 | PEpow : PExpr -> N -> PExpr.
 Arguments PExpr : clear implicits.
 
+Register PEc as micromega.PExpr.PEc.
+Register PEX as micromega.PExpr.PEX.
+Register PEadd as micromega.PExpr.PEadd.
+Register PEsub as micromega.PExpr.PEsub.
+Register PEmul as micromega.PExpr.PEmul.
+Register PEopp as micromega.PExpr.PEopp.
+Register PEpow as micromega.PExpr.PEpow.
+
  (* Definition of multivariable polynomials with coefficients in C :
     Type [Pol] represents [X1 ... Xn].
     The representation is Horner's where a [n] variable polynomial
@@ -60,6 +68,10 @@ Inductive Pol {C} : Type :=
 | PX : Pol -> positive -> Pol -> Pol.
 Arguments Pol : clear implicits.
 
+Register Pc as micromega.Pol.Pc.
+Register Pinj as micromega.Pol.Pinj.
+Register PX   as micromega.Pol.PX.
+
 Section MakeRingPol.
 
  (* Ring elements *)

theories/micromega/Lra.v

@@ -20,6 +20,7 @@ Require Import Rdefinitions.
 Require Import RingMicromega.
 Require Import VarMap.
 Require Coq.micromega.Tauto.
+Require Import Rregisternames.
 Declare ML Module "micromega_plugin".
 
 Ltac rchange := 

theories/micromega/QMicromega.v

@@ -154,6 +154,9 @@ Qed.
 
 Definition QWitness := Psatz Q.
 
+Register QWitness as micromega.QWitness.type.
+
+
 Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qeq_bool Qle_bool.
 
 Require Import List.

theories/micromega/RMicromega.v

@@ -150,7 +150,17 @@ Inductive Rcst :=
   | CInv  (r : Rcst)
   | COpp  (r : Rcst).
 
-
+Register Rcst   as micromega.Rcst.type.
+Register C0     as micromega.Rcst.C0.
+Register C1     as micromega.Rcst.C1.
+Register CQ     as micromega.Rcst.CQ.
+Register CZ     as micromega.Rcst.CZ.
+Register CPlus  as micromega.Rcst.CPlus.
+Register CMinus as micromega.Rcst.CMinus.
+Register CMult  as micromega.Rcst.CMult.
+Register CPow   as micromega.Rcst.CPow.
+Register CInv   as micromega.Rcst.CInv.
+Register COpp   as micromega.Rcst.COpp.
 
 Definition z_of_exp (z : Z + nat) :=
   match z with

theories/micromega/RingMicromega.v

@@ -298,6 +298,15 @@ Inductive Psatz : Type :=
 | PsatzC    : C -> Psatz
 | PsatzZ    : Psatz.
 
+Register PsatzIn     as micromega.Psatz.PsatzIn.
+Register PsatzSquare as micromega.Psatz.PsatzSquare.
+Register PsatzMulC   as micromega.Psatz.PsatzMulC.
+Register PsatzMulE   as micromega.Psatz.PsatzMulE.
+Register PsatzAdd    as micromega.Psatz.PsatzAdd.
+Register PsatzC      as micromega.Psatz.PsatzC.
+Register PsatzZ      as micromega.Psatz.PsatzZ.
+
+
 (** Given a list [l] of NFormula and an extended polynomial expression
    [e], if [eval_Psatz l e] succeeds (= Some f) then [f] is a
    logic consequence of the conjunction of the formulae in l.
@@ -672,6 +681,13 @@ Inductive Op2 : Set := (* binary relations *)
 | OpLt
 | OpGt.
 
+Register OpEq  as micromega.Op2.OpEq.
+Register OpNEq as micromega.Op2.OpNEq.
+Register OpLe  as micromega.Op2.OpLe.
+Register OpGe  as micromega.Op2.OpGe.
+Register OpLt  as micromega.Op2.OpLt.
+Register OpGt  as micromega.Op2.OpGt.
+
 Definition eval_op2 (o : Op2) : R -> R -> Prop :=
 match o with
 | OpEq => req
@@ -686,12 +702,15 @@ Definition  eval_pexpr : PolEnv -> PExpr C -> R :=
  PEeval rplus rtimes rminus ropp phi pow_phi rpow.
 
 #[universes(template)]
-Record Formula (T:Type) : Type := {
+Record Formula (T:Type) : Type := Build_Formula{
   Flhs : PExpr T;
   Fop : Op2;
   Frhs : PExpr T
 }.
 
+Register Formula as micromega.Formula.type.
+Register Build_Formula as micromega.Formula.Build_Formula.
+
 Definition eval_formula (env : PolEnv) (f : Formula C) : Prop :=
   let (lhs, op, rhs) := f in
     (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs).

theories/micromega/Tauto.v

@@ -37,6 +37,16 @@ Section S.
   | N    : GFormula  -> GFormula
   | I    : GFormula  -> option AF -> GFormula  -> GFormula.
 
+  Register TT as micromega.GFormula.TT.
+  Register FF as micromega.GFormula.FF.
+  Register X  as micromega.GFormula.X.
+  Register A  as micromega.GFormula.A.
+  Register Cj as micromega.GFormula.Cj.
+  Register D  as micromega.GFormula.D.
+  Register N  as micromega.GFormula.N.
+  Register I  as micromega.GFormula.I.
+
+
   Section MAPX.
     Variable F : TX -> TX.
 
@@ -137,6 +147,8 @@ End S.
 (** Typical boolean formulae *)
 Definition BFormula (A : Type) := @GFormula A Prop unit unit.
 
+Register BFormula as micromega.BFormula.type.
+
 Section MAPATOMS.
   Context {TA TA':Type}.
   Context {TX  : Type}.

theories/micromega/VarMap.v

@@ -33,6 +33,11 @@ Inductive t {A} : Type :=
 | Branch : t  -> A -> t  -> t .
 Arguments t : clear implicits.
 
+Register Branch as micromega.VarMap.Branch.
+Register Elt    as micromega.VarMap.Elt.
+Register Empty  as micromega.VarMap.Empty.
+Register t      as micromega.VarMap.type.
+
 Section MakeVarMap.
 
   Variable A : Type.

theories/micromega/ZMicromega.v

@@ -564,10 +564,14 @@ Inductive ZArithProof :=
 .
 (*| SplitProof :   PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*)
 
+Register ZArithProof as micromega.ZArithProof.type.
+Register DoneProof   as micromega.ZArithProof.DoneProof.
+Register RatProof    as micromega.ZArithProof.RatProof.
+Register CutProof    as micromega.ZArithProof.CutProof.
+Register EnumProof   as micromega.ZArithProof.EnumProof.
+Register ExProof     as micromega.ZArithProof.ExProof.
 
 
-(* n/d <= x  -> d*x - n >= 0 *)
-
 
 (* In order to compute the 'cut', we need to express a polynomial P as a * Q + b.
    - b is the constant