aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/EnvRing.v85
-rw-r--r--plugins/micromega/QMicromega.v4
-rw-r--r--plugins/micromega/RingMicromega.v5
-rw-r--r--plugins/micromega/Tauto.v1
-rw-r--r--plugins/micromega/VarMap.v13
-rw-r--r--plugins/micromega/ZMicromega.v10
-rw-r--r--plugins/micromega/micromega.ml18
7 files changed, 71 insertions, 65 deletions
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 78bfe480b3..2762bb6b32 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -19,6 +19,47 @@ Require Export Ring_theory.
Local Open Scope positive_scope.
Import RingSyntax.
+(** Definition of polynomial expressions *)
+#[universes(template)]
+Inductive PExpr {C} : Type :=
+| PEc : C -> PExpr
+| PEX : positive -> PExpr
+| PEadd : PExpr -> PExpr -> PExpr
+| PEsub : PExpr -> PExpr -> PExpr
+| PEmul : PExpr -> PExpr -> PExpr
+| PEopp : PExpr -> PExpr
+| PEpow : PExpr -> N -> PExpr.
+Arguments PExpr : clear implicits.
+
+ (* Definition of multivariable polynomials with coefficients in C :
+ Type [Pol] represents [X1 ... Xn].
+ The representation is Horner's where a [n] variable polynomial
+ (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients
+ are polynomials with [n-1] variables (C[X2..Xn]).
+ There are several optimisations to make the repr compacter:
+ - [Pc c] is the constant polynomial of value c
+ == c*X1^0*..*Xn^0
+ - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables.
+ variable indices are shifted of j in Q.
+ == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn}
+ - [PX P i Q] is an optimised Horner form of P*X^i + Q
+ with P not the null polynomial
+ == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn}
+
+ In addition:
+ - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden
+ since they can be represented by the simpler form (PX P (i+j) Q)
+ - (Pinj i (Pinj j P)) is (Pinj (i+j) P)
+ - (Pinj i (Pc c)) is (Pc c)
+ *)
+
+#[universes(template)]
+Inductive Pol {C} : Type :=
+| Pc : C -> Pol
+| Pinj : positive -> Pol -> Pol
+| PX : Pol -> positive -> Pol -> Pol.
+Arguments Pol : clear implicits.
+
Section MakeRingPol.
(* Ring elements *)
@@ -96,33 +137,11 @@ Section MakeRingPol.
match goal with |- ?t == _ => mul_permut_rec t end).
- (* Definition of multivariable polynomials with coefficients in C :
- Type [Pol] represents [X1 ... Xn].
- The representation is Horner's where a [n] variable polynomial
- (C[X1..Xn]) is seen as a polynomial on [X1] which coefficients
- are polynomials with [n-1] variables (C[X2..Xn]).
- There are several optimisations to make the repr compacter:
- - [Pc c] is the constant polynomial of value c
- == c*X1^0*..*Xn^0
- - [Pinj j Q] is a polynomial constant w.r.t the [j] first variables.
- variable indices are shifted of j in Q.
- == X1^0 *..* Xj^0 * Q{X1 <- Xj+1;..; Xn-j <- Xn}
- - [PX P i Q] is an optimised Horner form of P*X^i + Q
- with P not the null polynomial
- == P * X1^i + Q{X1 <- X2; ..; Xn-1 <- Xn}
+ Notation PExpr := (PExpr C).
+ Notation Pol := (Pol C).
- In addition:
- - polynomials of the form (PX (PX P i (Pc 0)) j Q) are forbidden
- since they can be represented by the simpler form (PX P (i+j) Q)
- - (Pinj i (Pinj j P)) is (Pinj (i+j) P)
- - (Pinj i (Pc c)) is (Pc c)
- *)
-
- #[universes(template)]
- Inductive Pol : Type :=
- | Pc : C -> Pol
- | Pinj : positive -> Pol -> Pol
- | PX : Pol -> positive -> Pol -> Pol.
+ Implicit Types pe : PExpr.
+ Implicit Types P : Pol.
Definition P0 := Pc cO.
Definition P1 := Pc cI.
@@ -152,7 +171,7 @@ Section MakeRingPol.
| _ => Pinj j P
end.
- Definition mkPinj_pred j P:=
+ Definition mkPinj_pred j P :=
match j with
| xH => P
| xO j => Pinj (Pos.pred_double j) P
@@ -938,18 +957,6 @@ Qed.
rewrite <- IHm; auto.
Qed.
- (** Definition of polynomial expressions *)
-
- #[universes(template)]
- Inductive PExpr : Type :=
- | PEc : C -> PExpr
- | PEX : positive -> PExpr
- | PEadd : PExpr -> PExpr -> PExpr
- | PEsub : PExpr -> PExpr -> PExpr
- | PEmul : PExpr -> PExpr -> PExpr
- | PEopp : PExpr -> PExpr
- | PEpow : PExpr -> N -> PExpr.
-
(** evaluation of polynomial expressions towards R *)
Definition mk_X j := mkPinj_pred j mkX.
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index a99f21ad47..3c72d3268f 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -68,7 +68,7 @@ Require Import EnvRing.
Fixpoint Qeval_expr (env: PolEnv Q) (e: PExpr Q) : Q :=
match e with
| PEc c => c
- | PEX _ j => env j
+ | PEX j => env j
| PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
| PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
| PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
@@ -80,7 +80,7 @@ Lemma Qeval_expr_simpl : forall env e,
Qeval_expr env e =
match e with
| PEc c => c
- | PEX _ j => env j
+ | PEX j => env j
| PEadd pe1 pe2 => (Qeval_expr env pe1) + (Qeval_expr env pe2)
| PEsub pe1 pe2 => (Qeval_expr env pe1) - (Qeval_expr env pe2)
| PEmul pe1 pe2 => (Qeval_expr env pe1) * (Qeval_expr env pe2)
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 75801162a7..cddc140f51 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -289,7 +289,6 @@ destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor).
now apply (Rplus_nonneg_nonneg sor).
Qed.
-#[universes(template)]
Inductive Psatz : Type :=
| PsatzIn : nat -> Psatz
| PsatzSquare : PolC -> Psatz
@@ -892,7 +891,7 @@ Fixpoint xdenorm (jmp : positive) (p: Pol C) : PExpr C :=
| Pc c => PEc c
| Pinj j p => xdenorm (Pos.add j jmp ) p
| PX p j q => PEadd
- (PEmul (xdenorm jmp p) (PEpow (PEX _ jmp) (Npos j)))
+ (PEmul (xdenorm jmp p) (PEpow (PEX jmp) (Npos j)))
(xdenorm (Pos.succ jmp) q)
end.
@@ -961,7 +960,7 @@ Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c).
Fixpoint map_PExpr (e : PExpr S) : PExpr C :=
match e with
| PEc c => PEc (C_of_S c)
- | PEX _ p => PEX _ p
+ | PEX p => PEX p
| PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2)
| PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2)
| PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2)
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 56032befba..d6ccf582ae 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -27,7 +27,6 @@ Section S.
Context {AA : Type}. (* type of annotations for atoms *)
Context {AF : Type}. (* type of formulae identifiers *)
- #[universes(template)]
Inductive GFormula : Type :=
| TT : GFormula
| FF : GFormula
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 79cb6a3a3e..f93fe021f9 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -27,16 +27,18 @@ Set Implicit Arguments.
* As a side note, by dropping the polymorphism, one gets small, yet noticeable, speed-up.
*)
+Inductive t {A} : Type :=
+| Empty : t
+| Elt : A -> t
+| Branch : t -> A -> t -> t .
+Arguments t : clear implicits.
+
Section MakeVarMap.
Variable A : Type.
Variable default : A.
- #[universes(template)]
- Inductive t : Type :=
- | Empty : t
- | Elt : A -> t
- | Branch : t -> A -> t -> t .
+ Notation t := (t A).
Fixpoint find (vm : t) (p:positive) {struct vm} : A :=
match vm with
@@ -49,7 +51,6 @@ Section MakeVarMap.
end
end.
-
Fixpoint singleton (x:positive) (v : A) : t :=
match x with
| xH => Elt v
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 3ea7635244..c0d22486b5 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -65,7 +65,7 @@ Qed.
Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z :=
match e with
| PEc c => c
- | PEX _ x => env x
+ | PEX x => env x
| PEadd e1 e2 => Zeval_expr env e1 + Zeval_expr env e2
| PEmul e1 e2 => Zeval_expr env e1 * Zeval_expr env e2
| PEpow e1 n => Z.pow (Zeval_expr env e1) (Z.of_N n)
@@ -78,7 +78,7 @@ Definition eval_expr := eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x
Fixpoint Zeval_const (e: PExpr Z) : option Z :=
match e with
| PEc c => Some c
- | PEX _ x => None
+ | PEX x => None
| PEadd e1 e2 => map_option2 (fun x y => Some (x + y))
(Zeval_const e1) (Zeval_const e2)
| PEmul e1 e2 => map_option2 (fun x y => Some (x * y))
@@ -742,7 +742,7 @@ Module Vars.
Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t :=
match e with
| PEc _ => Vars.empty
- | PEX _ x => Vars.singleton x
+ | PEX x => Vars.singleton x
| PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 =>
let v1 := vars_of_pexpr e1 in
let v2 := vars_of_pexpr e2 in
@@ -774,10 +774,10 @@ Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type}
end.
Definition bound_var (v : positive) : Formula Z :=
- Build_Formula (PEX _ v) OpGe (PEc 0).
+ Build_Formula (PEX v) OpGe (PEc 0).
Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z :=
- Build_Formula (PEX _ x) OpEq (PEsub (PEX _ y) (PEX _ t)).
+ Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)).
Section BOUND.
Context {TX TG ID : Type}.
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index a64a5a84b3..2e97dfea19 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -556,6 +556,15 @@ let zeq_bool x y =
| Eq -> true
| _ -> false
+type 'c pExpr =
+| PEc of 'c
+| PEX of positive
+| PEadd of 'c pExpr * 'c pExpr
+| PEsub of 'c pExpr * 'c pExpr
+| PEmul of 'c pExpr * 'c pExpr
+| PEopp of 'c pExpr
+| PEpow of 'c pExpr * n
+
type 'c pol =
| Pc of 'c
| Pinj of positive * 'c pol
@@ -868,15 +877,6 @@ let rec psquare cO cI cadd cmul ceqb = function
let p3 = psquare cO cI cadd cmul ceqb p2 in
mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2
-type 'c pExpr =
-| PEc of 'c
-| PEX of positive
-| PEadd of 'c pExpr * 'c pExpr
-| PEsub of 'c pExpr * 'c pExpr
-| PEmul of 'c pExpr * 'c pExpr
-| PEopp of 'c pExpr
-| PEpow of 'c pExpr * n
-
(** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **)
let mk_X cO cI j =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:29:03 +0000