Added transitivity and irreflexivity of <, as well as < -elimination for binary positive numbers.

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 1453 insertions, 0 deletions

diff --git a/contrib/micromega/CheckerMaker.v b/contrib/micromega/CheckerMaker.v
new file mode 100644
index 0000000000..8aeada77b1
--- /dev/null
+++ b/contrib/micromega/CheckerMaker.v
@@ -0,0 +1,121 @@
+(********************************************************************)
+(*                                                                  *)
+(* Micromega: A reflexive tactics using the Positivstellensatz      *)
+(*                                                                  *)
+(*  Frédéric Besson (Irisa/Inria) 2006				    *)
+(*                                                                  *)
+(********************************************************************)
+
+Require Import Decidable.
+Require Import List.
+Require Import Refl.
+
+Set Implicit Arguments.
+
+Section CheckerMaker.
+
+(* 'Formula' is a syntactic representation of a certain kind of propositions. *)
+Variable Formula : Type.
+
+Variable Env : Type.
+
+Variable eval : Env -> Formula -> Prop.
+
+Variable Formula' : Type.
+
+Variable eval' : Env -> Formula' -> Prop.
+
+Variable normalise : Formula -> Formula'.
+
+Variable negate : Formula -> Formula'.
+
+Hypothesis normalise_sound :
+  forall (env : Env) (t : Formula), eval env t -> eval' env (normalise t).
+
+Hypothesis negate_correct :
+  forall (env : Env) (t : Formula), eval env t <-> ~ (eval' env (negate t)).
+
+Variable Witness : Type.
+
+Variable check_formulas' : list Formula' -> Witness -> bool.
+
+Hypothesis check_formulas'_sound :
+  forall (l : list Formula') (w : Witness),
+    check_formulas' l w = true ->
+      forall env : Env, make_impl (eval' env) l False.
+
+Definition normalise_list : list Formula -> list Formula' := map normalise.
+Definition negate_list : list Formula -> list Formula' := map negate.
+
+Definition check_formulas (l : list Formula) (w : Witness) : bool :=
+  check_formulas' (map normalise l) w.
+
+(* Contraposition of normalise_sound for lists *)
+Lemma normalise_sound_contr : forall (env : Env) (l : list Formula),
+  make_impl (eval' env) (map normalise l) False -> make_impl (eval env) l False.
+Proof.
+intros env l; induction l as [| t l IH]; simpl in *.
+trivial.
+intros H1 H2. apply IH. apply H1. now apply normalise_sound.
+Qed.
+
+Theorem check_formulas_sound :
+  forall (l : list Formula) (w : Witness),
+    check_formulas l w = true -> forall env : Env, make_impl (eval env) l False.
+Proof.
+unfold check_formulas; intros l w H env. destruct l as [| t l]; simpl in *.
+pose proof (check_formulas'_sound H env) as H1; now simpl in H1.
+intro H1. apply normalise_sound in H1.
+pose proof (check_formulas'_sound H env) as H2; simpl in H2.
+apply H2 in H1. now apply normalise_sound_contr.
+Qed.
+
+(* In check_conj_formulas', t2 is supposed to be a list of negations of
+formulas. If, for example, t1 = [A1, A2] and t2 = [~ B1, ~ B2], then
+check_conj_formulas' checks that each of [~ B1, A1, A2] and [~ B2, A1, A2] is
+inconsistent. This means that A1 /\ A2 -> B1 and A1 /\ A2 -> B1, i.e., that
+A1 /\ A2 -> B1 /\ B2. *)
+
+Fixpoint check_conj_formulas'
+  (t1 : list Formula') (wits : list Witness) (t2 : list Formula') {struct wits} : bool :=
+match t2 with
+| nil => true
+| t':: rt2 =>
+  match wits with
+  | nil => false
+  | w :: rwits =>
+    match check_formulas' (t':: t1) w with
+    | true => check_conj_formulas' t1 rwits rt2
+    | false => false
+    end
+  end
+end.
+
+(* checks whether the conjunction of t1 implies the conjunction of t2 *)
+
+Definition check_conj_formulas
+  (t1 : list Formula) (wits : list Witness) (t2 : list Formula) : bool :=
+    check_conj_formulas' (normalise_list t1) wits (negate_list t2).
+
+Theorem check_conj_formulas_sound :
+  forall (t1 : list Formula) (t2 : list Formula) (wits : list Witness),
+    check_conj_formulas t1 wits t2 = true ->
+      forall env : Env, make_impl (eval env) t1 (make_conj (eval env) t2).
+Proof.
+intro t1; induction t2 as [| a2 t2' IH].
+intros; apply make_impl_true.
+intros wits H env.
+unfold check_conj_formulas in H; simpl in H.
+destruct wits as [| w ws]; simpl in H. discriminate.
+case_eq (check_formulas' (negate a2 :: normalise_list t1) w);
+intro H1; rewrite H1 in H; [| discriminate].
+assert (H2 : make_impl (eval' env) (negate a2 :: normalise_list t1) False) by
+now apply check_formulas'_sound with (w := w). clear H1.
+pose proof (IH ws H env) as H1. simpl in H2.
+assert (H3 : eval' env (negate a2) -> make_impl (eval env) t1 False)
+by auto using normalise_sound_contr. clear H2. rewrite <- make_conj_impl in *.
+rewrite make_conj_cons. intro H2. split.
+apply <- negate_correct. intro; now elim H3. exact (H1 H2).
+Qed.
+
+End CheckerMaker.
diff --git a/contrib/micromega/Examples.v b/contrib/micromega/Examples.v
new file mode 100644
index 0000000000..976815142b
--- /dev/null
+++ b/contrib/micromega/Examples.v
@@ -0,0 +1,103 @@
+Require Import OrderedRing.
+Require Import RingMicromega.
+Require Import Ring_polynom.
+Require Import ZCoeff.
+Require Import Refl.
+Require Import ZArith.
+Require Import List.
+
+Import OrderedRingSyntax.
+
+Section Examples.
+
+Variable R : Type.
+Variables rO rI : R.
+Variables rplus rtimes rminus: R -> R -> R.
+Variable ropp : R -> R.
+Variables req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Definition phi : Z -> R := gen_order_phi_Z 0 1 rplus rtimes ropp.
+
+Lemma ZSORaddon :
+  SORaddon 0 1 rplus rtimes rminus ropp req rle (* ring elements *)
+           0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *)
+           Zeq_bool Zle_bool
+           phi (fun x => x) (pow_N 1 rtimes).
+Proof.
+constructor.
+exact (Zring_morph sor).
+exact (pow_N_th 1 rtimes sor.(SORsetoid)).
+apply (Zcneqb_morph sor).
+apply (Zcleb_morph sor).
+Qed.
+
+Definition Zeval_formula :=
+  eval_formula 0 rplus rtimes rminus ropp req rle rlt phi (fun x => x) (pow_N 1 rtimes).
+Definition Z_In := S_In 0%Z Zeq_bool Zle_bool.
+Definition Z_Square := S_Square 0%Z Zeq_bool Zle_bool.
+
+(* Example: forall x y : Z, x + y = 0 -> x - y = 0 -> x < 0 -> False *)
+
+Lemma plus_minus : forall x y : R, x + y == 0 -> x - y == 0 -> x < 0 -> False.
+Proof.
+intros x y.
+Open Scope Z_scope.
+set (varmap := fun (x y : R) => x :: y :: nil).
+set (expr :=
+ Build_Formula (PEadd (PEX Z 1) (PEX Z 2)) OpEq (PEc 0)
+   :: Build_Formula (PEsub (PEX Z 1) (PEX Z 2)) OpEq (PEc 0)
+      :: Build_Formula (PEX Z 1) OpLt (PEc 0) :: nil).
+set (cert :=
+   S_Add (S_Mult (S_Pos 0 Zeq_bool Zle_bool 2 (refl_equal true)) (Z_In 2))
+     (S_Add (S_Ideal (PEc 1) (Z_In 1)) (S_Ideal (PEc 1) (Z_In 0)))).
+change (make_impl (Zeval_formula (varmap x y)) expr False).
+apply (check_formulas_sound sor ZSORaddon expr cert).
+reflexivity.
+Close Scope Z_scope.
+Qed.
+
+(* Example *)
+
+Let four : R := ((1 + 1) * (1 + 1)).
+Lemma Zdiscr :
+  forall a b c x : R,
+    a * (x * x) + b * x + c == 0 -> 0 <= b * b - four * a * c.
+Proof.
+Open Scope Z_scope.
+set (varmap := fun (a b c x : R) => a :: b :: c :: x:: nil).
+set (poly1 :=
+     (Build_Formula
+           (PEadd
+              (PEadd (PEmul (PEX Z 1) (PEmul (PEX Z 4) (PEX Z 4)))
+                 (PEmul (PEX Z 2) (PEX Z 4))) (PEX Z 3)) OpEq (PEc 0)) :: nil).
+set (poly2 :=
+     (Build_Formula
+        (PEsub (PEmul (PEX Z 2) (PEX Z 2))
+           (PEmul (PEmul (PEc 4) (PEX Z 1)) (PEX Z 3))) OpGe (PEc 0)) :: nil).
+set (wit :=
+    (S_Add (Z_In 0)
+       (S_Add (S_Ideal (PEmul (PEc (-4)) (PEX Z 1)) (Z_In 1))
+          (Z_Square
+             (PEadd (PEmul (PEc 2) (PEmul (PEX Z 1) (PEX Z 4))) (PEX Z 2))))) :: nil).
+intros a b c x.
+change (make_impl (Zeval_formula (varmap a b c x)) poly1
+  (make_conj (Zeval_formula (varmap a b c x)) poly2)).
+apply (check_conj_formulas_sound sor ZSORaddon poly1 poly2 wit).
+reflexivity.
+Qed.
+
+End Examples.
+
diff --git a/contrib/micromega/OrderedRing.v b/contrib/micromega/OrderedRing.v
new file mode 100644
index 0000000000..ac1833a135
--- /dev/null
+++ b/contrib/micromega/OrderedRing.v
@@ -0,0 +1,443 @@
+Require Import Setoid.
+Require Import Ring.
+
+Set Implicit Arguments.
+
+Module Import OrderedRingSyntax.
+Export RingSyntax.
+
+Reserved Notation "x ~= y" (at level 70, no associativity).
+Reserved Notation "x [=] y" (at level 70, no associativity).
+Reserved Notation "x [~=] y" (at level 70, no associativity).
+Reserved Notation "x [<] y" (at level 70, no associativity).
+Reserved Notation "x [<=] y" (at level 70, no associativity).
+End OrderedRingSyntax.
+
+Section DEFINITIONS.
+
+Variable R : Type.
+Variable (rO rI : R) (rplus rtimes rminus: R -> R -> R) (ropp : R -> R).
+Variable req rle rlt : R -> R -> Prop.
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Record SOR : Prop := mk_SOR_theory {
+  SORsetoid : Setoid_Theory R req;
+  SORplus_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2;
+  SORtimes_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2;
+  SORopp_wd : forall x1 x2, x1 == x2 ->  -x1 == -x2;
+  SORle_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 <= y1 <-> x2 <= y2);
+  SORlt_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 < y1 <-> x2 < y2);
+  SORrt : ring_theory rO rI rplus rtimes rminus ropp req;
+  SORle_refl : forall n : R, n <= n;
+  SORle_antisymm : forall n m : R, n <= m -> m <= n -> n == m;
+  SORle_trans : forall n m p : R, n <= m -> m <= p -> n <= p;
+  SORlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m;
+  SORlt_trichotomy : forall n m : R,  n < m \/ n == m \/ m < n;
+  SORplus_le_mono_l : forall n m p : R, n <= m -> p + n <= p + m;
+  SORtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m;
+  SORneq_0_1 : 0 ~= 1
+}.
+
+(* We cannot use Relation_Definitions.order.ord_antisym and
+Relations_1.Antisymmetric because they refer to Leibniz equality *)
+
+End DEFINITIONS.
+
+Section STRICT_ORDERED_RING.
+
+Variable R : Type.
+Variable (rO rI : R) (rplus rtimes rminus: R -> R -> R) (ropp : R -> R).
+Variable req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Add Relation R req
+  reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
+  symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
+  transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+as sor_setoid.
+
+Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
+Proof.
+exact sor.(SORplus_wd).
+Qed.
+Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
+Proof.
+exact sor.(SORtimes_wd).
+Qed.
+Add Morphism ropp with signature req ==> req as ropp_morph.
+Proof.
+exact sor.(SORopp_wd).
+Qed.
+Add Morphism rle with signature req ==> req ==> iff as rle_morph.
+Proof.
+exact sor.(SORle_wd).
+Qed.
+Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
+Proof.
+exact sor.(SORlt_wd).
+Qed.
+
+Add Ring SOR : sor.(SORrt).
+
+Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
+Proof.
+intros x1 x2 H1 y1 y2 H2.
+rewrite (sor.(SORrt).(Rsub_def) x1 y1).
+rewrite (sor.(SORrt).(Rsub_def) x2 y2).
+rewrite H1; now rewrite H2.
+Qed.
+
+Theorem Rneq_symm : forall n m : R, n ~= m -> m ~= n.
+Proof.
+intros n m H1 H2; rewrite H2 in H1; now apply H1.
+Qed.
+
+(* Propeties of plus, minus and opp *)
+
+Theorem Rplus_0_l : forall n : R, 0 + n == n.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rplus_0_r : forall n : R, n + 0 == n.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rtimes_0_r : forall n : R, n * 0 == 0.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rplus_comm : forall n m : R, n + m == m + n.
+Proof.
+intros; ring.
+Qed.
+
+Theorem Rtimes_0_l : forall n : R, 0 * n == 0.
+Proof.
+intro; ring.
+Qed.
+
+Theorem Rtimes_comm : forall n m : R, n * m == m * n.
+Proof.
+intros; ring.
+Qed.
+
+Theorem Rminus_eq_0 : forall n m : R, n - m == 0 <-> n == m.
+Proof.
+intros n m.
+split; intro H. setoid_replace n with ((n - m) + m) by ring. rewrite H. now rewrite Rplus_0_l.
+rewrite H; ring.
+Qed.
+
+Theorem Rplus_cancel_l : forall n m p : R, p + n == p + m <-> n == m.
+Proof.
+intros n m p; split; intro H.
+setoid_replace n with (- p + (p + n)) by ring.
+setoid_replace m with (- p + (p + m)) by ring. now rewrite H.
+now rewrite H.
+Qed.
+
+(* Relations *)
+
+Theorem Rle_refl : forall n : R, n <= n.
+Proof sor.(SORle_refl).
+
+Theorem Rle_antisymm : forall n m : R, n <= m -> m <= n -> n == m.
+Proof sor.(SORle_antisymm).
+
+Theorem Rle_trans : forall n m p : R, n <= m -> m <= p -> n <= p.
+Proof sor.(SORle_trans).
+
+Theorem Rlt_trichotomy : forall n m : R,  n < m \/ n == m \/ m < n.
+Proof sor.(SORlt_trichotomy).
+
+Theorem Rlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m.
+Proof sor.(SORlt_le_neq).
+
+Theorem Rneq_0_1 : 0 ~= 1.
+Proof sor.(SORneq_0_1).
+
+Theorem Req_em : forall n m : R, n == m \/ n ~= m.
+Proof.
+intros n m. destruct (Rlt_trichotomy n m) as [H | [H | H]]; try rewrite Rlt_le_neq in H.
+right; now destruct H.
+now left.
+right; apply Rneq_symm; now destruct H.
+Qed.
+
+Theorem Req_dne : forall n m : R, ~ ~ n == m <-> n == m.
+Proof.
+intros n m; destruct (Req_em n m) as [H | H].
+split; auto.
+split. intro H1; false_hyp H H1. auto.
+Qed.
+
+Theorem Rle_lt_eq : forall n m : R, n <= m <-> n < m \/ n == m.
+Proof.
+intros n m; rewrite Rlt_le_neq.
+split; [intro H | intros [[H1 H2] | H]].
+destruct (Req_em n m) as [H1 | H1]. now right. left; now split.
+assumption.
+rewrite H; apply Rle_refl.
+Qed.
+
+Ltac le_less := rewrite Rle_lt_eq; left; try assumption.
+Ltac le_equal := rewrite Rle_lt_eq; right; try reflexivity; try assumption.
+Ltac le_elim H := rewrite Rle_lt_eq in H; destruct H as [H | H].
+
+Theorem Rlt_trans : forall n m p : R, n < m -> m < p -> n < p.
+Proof.
+intros n m p; repeat rewrite Rlt_le_neq; intros [H1 H2] [H3 H4]; split.
+now apply Rle_trans with m.
+intro H. rewrite H in H1. pose proof (Rle_antisymm H3 H1). now apply H4.
+Qed.
+
+Theorem Rle_lt_trans : forall n m p : R, n <= m -> m < p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+now apply Rlt_trans with (m := m). now rewrite H1.
+Qed.
+
+Theorem Rlt_le_trans : forall n m p : R, n < m -> m <= p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H2.
+now apply Rlt_trans with (m := m). now rewrite <- H2.
+Qed.
+
+Theorem Rle_gt_cases : forall n m : R, n <= m \/ m < n.
+Proof.
+intros n m; destruct (Rlt_trichotomy n m) as [H | [H | H]].
+left; now le_less. left; now le_equal. now right.
+Qed.
+
+Theorem Rlt_neq : forall n m : R, n < m -> n ~= m.
+Proof.
+intros n m; rewrite Rlt_le_neq; now intros [_ H].
+Qed.
+
+Theorem Rle_ngt : forall n m : R, n <= m <-> ~ m < n.
+Proof.
+intros n m; split.
+intros H H1; assert (H2 : n < n) by now apply Rle_lt_trans with m. now apply (Rlt_neq H2).
+intro H. destruct (Rle_gt_cases n m) as [H1 | H1]. assumption. false_hyp H1 H.
+Qed.
+
+Theorem Rlt_nge : forall n m : R, n < m <-> ~ m <= n.
+Proof.
+intros n m; split.
+intros H H1; assert (H2 : n < n) by now apply Rlt_le_trans with m. now apply (Rlt_neq H2).
+intro H. destruct (Rle_gt_cases m n) as [H1 | H1]. false_hyp H1 H. assumption.
+Qed.
+
+(* Plus, minus and order *)
+
+Theorem Rplus_le_mono_l : forall n m p : R, n <= m <-> p + n <= p + m.
+Proof.
+intros n m p; split.
+apply sor.(SORplus_le_mono_l).
+intro H. apply (sor.(SORplus_le_mono_l) (p + n) (p + m) (- p)) in H.
+setoid_replace (- p + (p + n)) with n in H by ring.
+setoid_replace (- p + (p + m)) with m in H by ring. assumption.
+Qed.
+
+Theorem Rplus_le_mono_r : forall n m p : R, n <= m <-> n + p <= m + p.
+Proof.
+intros n m p; rewrite (Rplus_comm n p); rewrite (Rplus_comm m p).
+apply Rplus_le_mono_l.
+Qed.
+
+Theorem Rplus_lt_mono_l : forall n m p : R, n < m <-> p + n < p + m.
+Proof.
+intros n m p; do 2 rewrite Rlt_le_neq. rewrite Rplus_cancel_l.
+now rewrite <- Rplus_le_mono_l.
+Qed.
+
+Theorem Rplus_lt_mono_r : forall n m p : R, n < m <-> n + p < m + p.
+Proof.
+intros n m p.
+rewrite (Rplus_comm n p); rewrite (Rplus_comm m p); apply Rplus_lt_mono_l.
+Qed.
+
+Theorem Rplus_lt_mono : forall n m p q : R, n < m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rlt_trans with (m + p); [now apply -> Rplus_lt_mono_r | now apply -> Rplus_lt_mono_l].
+Qed.
+
+Theorem Rplus_le_mono : forall n m p q : R, n <= m -> p <= q -> n + p <= m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rle_trans with (m + p); [now apply -> Rplus_le_mono_r | now apply -> Rplus_le_mono_l].
+Qed.
+
+Theorem Rplus_lt_le_mono : forall n m p q : R, n < m -> p <= q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rlt_le_trans with (m + p); [now apply -> Rplus_lt_mono_r | now apply -> Rplus_le_mono_l].
+Qed.
+
+Theorem Rplus_le_lt_mono : forall n m p q : R, n <= m -> p < q -> n + p < m + q.
+Proof.
+intros n m p q H1 H2.
+apply Rle_lt_trans with (m + p); [now apply -> Rplus_le_mono_r | now apply -> Rplus_lt_mono_l].
+Qed.
+
+Theorem Rplus_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_lt_mono.
+Qed.
+
+Theorem Rplus_pos_nonneg : forall n m : R, 0 < n -> 0 <= m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_lt_le_mono.
+Qed.
+
+Theorem Rplus_nonneg_pos : forall n m : R, 0 <= n -> 0 < m -> 0 < n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_le_lt_mono.
+Qed.
+
+Theorem Rplus_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n + m.
+Proof.
+intros n m H1 H2. rewrite <- (Rplus_0_l 0). now apply Rplus_le_mono.
+Qed.
+
+Theorem Rle_le_minus : forall n m : R, n <= m <-> 0 <= m - n.
+Proof.
+intros n m. rewrite (@Rplus_le_mono_r n m (- n)).
+setoid_replace (n + - n) with 0 by ring.
+now setoid_replace (m + - n) with (m - n) by ring.
+Qed.
+
+Theorem Rlt_lt_minus : forall n m : R, n < m <-> 0 < m - n.
+Proof.
+intros n m. rewrite (@Rplus_lt_mono_r n m (- n)).
+setoid_replace (n + - n) with 0 by ring.
+now setoid_replace (m + - n) with (m - n) by ring.
+Qed.
+
+Theorem Ropp_lt_mono : forall n m : R, n < m <-> - m < - n.
+Proof.
+intros n m. split; intro H.
+apply -> (@Rplus_lt_mono_l n m (- n - m)) in H.
+setoid_replace (- n - m + n) with (- m) in H by ring.
+now setoid_replace (- n - m + m) with (- n) in H by ring.
+apply -> (@Rplus_lt_mono_l (- m) (- n) (n + m)) in H.
+setoid_replace (n + m + - m) with n in H by ring.
+now setoid_replace (n + m + - n) with m in H by ring.
+Qed.
+
+Theorem Ropp_pos_neg : forall n : R, 0 < - n <-> n < 0.
+Proof.
+intro n; rewrite (Ropp_lt_mono n 0). now setoid_replace (- 0) with 0 by ring.
+Qed.
+
+(* Times and order *)
+
+Theorem Rtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m.
+Proof sor.(SORtimes_pos_pos).
+
+Theorem Rtimes_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n * m.
+Proof.
+intros n m H1 H2.
+le_elim H1. le_elim H2.
+le_less; now apply Rtimes_pos_pos.
+rewrite <- H2; rewrite Rtimes_0_r; le_equal.
+rewrite <- H1; rewrite Rtimes_0_l; le_equal.
+Qed.
+
+Theorem Rtimes_pos_neg : forall n m : R, 0 < n -> m < 0 -> n * m < 0.
+Proof.
+intros n m H1 H2. apply -> Ropp_pos_neg.
+setoid_replace (- (n * m)) with (n * (- m)) by ring.
+apply Rtimes_pos_pos. assumption. now apply <- Ropp_pos_neg.
+Qed.
+
+Theorem Rtimes_neg_neg : forall n m : R, n < 0 -> m < 0 -> 0 < n * m.
+Proof.
+intros n m H1 H2.
+setoid_replace (n * m) with ((- n) * (- m)) by ring.
+apply Rtimes_pos_pos; now apply <- Ropp_pos_neg.
+Qed.
+
+Theorem Rtimes_square_nonneg : forall n : R, 0 <= n * n.
+Proof.
+intro n; destruct (Rlt_trichotomy 0 n) as [H | [H | H]].
+le_less; now apply Rtimes_pos_pos.
+rewrite <- H, Rtimes_0_l; le_equal.
+le_less; now apply Rtimes_neg_neg.
+Qed.
+
+Theorem Rtimes_neq_0 : forall n m : R, n ~= 0 /\ m ~= 0 -> n * m ~= 0.
+Proof.
+intros n m [H1 H2].
+destruct (Rlt_trichotomy n 0) as [H3 | [H3 | H3]];
+destruct (Rlt_trichotomy m 0) as [H4 | [H4 | H4]];
+try (false_hyp H3 H1); try (false_hyp H4 H2).
+apply Rneq_symm. apply Rlt_neq. now apply Rtimes_neg_neg.
+apply Rlt_neq. rewrite Rtimes_comm. now apply Rtimes_pos_neg.
+apply Rlt_neq. now apply Rtimes_pos_neg.
+apply Rneq_symm. apply Rlt_neq. now apply Rtimes_pos_pos.
+Qed.
+
+(* The following theorems are used to build a morphism from Z to R and
+prove its properties in ZCoeff.v. They are not used in RingMicromega.v. *)
+
+(* Surprisingly, multilication is needed to prove the following theorem *)
+
+Theorem Ropp_neg_pos : forall n : R, - n < 0 <-> 0 < n.
+Proof.
+intro n; setoid_replace n with (- - n) by ring. rewrite Ropp_pos_neg.
+now setoid_replace (- - n) with n by ring.
+Qed.
+
+Theorem Rlt_0_1 : 0 < 1.
+Proof.
+apply <- Rlt_le_neq. split.
+setoid_replace 1 with (1 * 1) by ring; apply Rtimes_square_nonneg.
+apply Rneq_0_1.
+Qed.
+
+Theorem Rlt_succ_r : forall n : R, n < 1 + n.
+Proof.
+intro n. rewrite <- (Rplus_0_l n); setoid_replace (1 + (0 + n)) with (1 + n) by ring.
+apply -> Rplus_lt_mono_r. apply Rlt_0_1.
+Qed.
+
+Theorem Rlt_lt_succ : forall n m : R, n < m -> n < 1 + m.
+Proof.
+intros n m H; apply Rlt_trans with m. assumption. apply Rlt_succ_r.
+Qed.
+
+(*Theorem Rtimes_lt_mono_pos_l : forall n m p : R, 0 < p -> n < m -> p * n < p * m.
+Proof.
+intros n m p H1 H2. apply <- Rlt_lt_minus.
+setoid_replace (p * m - p * n) with (p * (m - n)) by ring.
+apply Rtimes_pos_pos. assumption. now apply -> Rlt_lt_minus.
+Qed.*)
+
+End STRICT_ORDERED_RING.
+
diff --git a/contrib/micromega/Refl.v b/contrib/micromega/Refl.v
new file mode 100644
index 0000000000..8dced223b6
--- /dev/null
+++ b/contrib/micromega/Refl.v
@@ -0,0 +1,74 @@
+(********************************************************************)
+(*                                                                  *)
+(* Micromega: A reflexive tactics using the Positivstellensatz *)
+(*                                                                  *)
+(*  Frédéric Besson (Irisa/Inria) 2006				    *)
+(*                                                                  *)
+(********************************************************************)
+Require Import List.
+
+Set Implicit Arguments.
+
+(* Refl of '->' '/\': basic properties *)
+
+Fixpoint make_impl (A : Type) (eval : A -> Prop) (l : list A) (goal : Prop) {struct l} : Prop :=
+  match l with
+    | nil => goal
+    | cons e l => (eval e) -> (make_impl eval l goal)
+  end.
+
+Theorem make_impl_true :
+  forall (A : Type) (eval : A -> Prop) (l : list A), make_impl eval l True.
+Proof.
+induction l as [| a l IH]; simpl.
+trivial.
+intro; apply IH.
+Qed.
+
+Fixpoint make_conj (A : Type) (eval : A -> Prop) (l : list A) {struct l} : Prop :=
+  match l with
+    | nil => True
+    | cons e nil => (eval e)
+    | cons e l2 => ((eval e) /\ (make_conj eval l2))
+  end.
+
+Theorem make_conj_cons : forall (A : Type) (eval : A -> Prop) (a : A) (l : list A),
+  make_conj eval (a :: l) <-> eval a /\ make_conj eval l.
+Proof.
+intros; destruct l; simpl; tauto.
+Qed.
+
+Lemma make_conj_impl : forall (A : Type) (eval : A -> Prop) (l : list A) (g : Prop),
+  (make_conj eval l -> g) <-> make_impl eval l g.
+Proof.
+  induction l.
+  simpl.
+  tauto.
+  simpl.
+  intros.
+  destruct l.
+  simpl.
+  tauto.
+  generalize (IHl g).
+  tauto.
+Qed.
+
+Lemma make_conj_in : forall (A : Type) (eval : A -> Prop) (l : list A),
+  make_conj eval l -> (forall p, In p l -> eval p).
+Proof.
+  induction l.
+  simpl.
+  tauto.
+  simpl.
+  intros.
+  destruct l.
+  simpl in H0.
+  destruct H0.
+  subst; auto.
+  tauto.
+  destruct H.
+  destruct H0.
+  subst;auto.
+  apply IHl; auto.
+Qed.
+
diff --git a/contrib/micromega/RingMicromega.v b/contrib/micromega/RingMicromega.v
new file mode 100644
index 0000000000..2d565321ac
--- /dev/null
+++ b/contrib/micromega/RingMicromega.v
@@ -0,0 +1,570 @@
+Require Import Ring_polynom.
+
+
+Require Import NArith.
+Require Import Relation_Definitions.
+Require Import Setoid.
+Require Import Ring_polynom.
+Require Import List.
+Require Import Bool.
+Require Import OrderedRing.
+Require Import Refl.
+Require Import CheckerMaker.
+
+Set Implicit Arguments.
+
+Import OrderedRingSyntax.
+
+Section Micromega.
+
+(* Assume we have a strict(ly?) ordered ring *)
+
+Variable R : Type.
+Variables rO rI : R.
+Variables rplus rtimes rminus: R -> R -> R.
+Variable ropp : R -> R.
+Variables req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+(* Assume we have a type of coefficients C and a morphism from C to R *)
+
+Variable C : Type.
+Variables cO cI : C.
+Variables cplus ctimes cminus: C -> C -> C.
+Variable copp : C -> C.
+Variables ceqb cleb : C -> C -> bool.
+Variable phi : C -> R.
+
+(* Power coefficients *)
+Variable E : Set. (* the type of exponents *)
+Variable pow_phi : N -> E.
+Variable rpow : R -> E -> R.
+
+Notation "[ x ]" := (phi x).
+Notation "x [=] y" := (ceqb x y).
+Notation "x [<=] y" := (cleb x y).
+
+(* Let's collect all hypotheses in addition to the ordered ring axioms into
+one structure *)
+
+Record SORaddon := mk_SOR_addon {
+  SORrm : ring_morph 0 1 rplus rtimes rminus ropp req cO cI cplus ctimes cminus copp ceqb phi;
+  SORpower : power_theory rI rtimes req pow_phi rpow;
+  SORcneqb_morph : forall x y : C, x [=] y = false -> [x] ~= [y];
+  SORcleb_morph : forall x y : C, x [<=] y = true -> [x] <= [y]
+}.
+
+Variable addon : SORaddon.
+
+Add Relation R req
+  reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
+  symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
+  transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+as micomega_sor_setoid.
+
+Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
+Proof.
+exact sor.(SORplus_wd).
+Qed.
+Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
+Proof.
+exact sor.(SORtimes_wd).
+Qed.
+Add Morphism ropp with signature req ==> req as ropp_morph.
+Proof.
+exact sor.(SORopp_wd).
+Qed.
+Add Morphism rle with signature req ==> req ==> iff as rle_morph.
+Proof.
+exact sor.(SORle_wd).
+Qed.
+Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
+Proof.
+exact sor.(SORlt_wd).
+Qed.
+
+Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
+Proof (rminus_morph sor). (* We already proved that minus is a morphism in OrderedRing.v *)
+
+Definition cneqb (x y : C) := negb (ceqb x y).
+Definition cltb (x y : C) := (cleb x y) && (cneqb x y).
+
+Notation "x [~=] y" := (cneqb x y).
+Notation "x [<] y" := (cltb x y).
+
+Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
+Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
+Ltac le_elim H := rewrite (Rle_lt_eq sor) in H; destruct H as [H | H].
+
+Lemma cleb_sound : forall x y : C, x [<=] y = true -> [x] <= [y].
+Proof addon.(SORcleb_morph).
+
+Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
+Proof.
+intros x y H1. apply addon.(SORcneqb_morph). unfold cneqb, negb in H1.
+destruct (ceqb x y); now try discriminate.
+Qed.
+
+Lemma cltb_sound : forall x y : C, x [<] y = true -> [x] < [y].
+Proof.
+intros x y H. unfold cltb in H. apply andb_prop in H. destruct H as [H1 H2].
+apply cleb_sound in H1. apply cneqb_sound in H2. apply <- (Rlt_le_neq sor). now split.
+Qed.
+
+(* Begin Micromega *)
+
+Definition PExprC := PExpr C. (* arbitrary expressions built from +, *, - *)
+Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom *)
+Definition Env := list R.
+
+Definition eval_pexpr : Env -> PExprC -> R := PEeval 0 rplus rtimes rminus ropp phi pow_phi rpow.
+Definition eval_pol : Env -> PolC -> R := Pphi 0 rplus rtimes phi.
+
+Inductive Op2 : Set := (* binary relations *)
+| OpEq
+| OpNEq
+| OpLe
+| OpGe
+| OpLt
+| OpGt.
+
+Definition eval_op2 (o : Op2) : R -> R -> Prop :=
+match o with
+| OpEq => req
+| OpNEq => fun x y : R => x ~= y
+| OpLe => rle
+| OpGe => fun x y : R => y <= x
+| OpLt => fun x y : R => x < y
+| OpGt => fun x y : R => y < x
+end.
+
+Record Formula : Type := {
+  Flhs : PExprC;
+  Fop : Op2;
+  Frhs : PExprC
+}.
+
+Definition eval_formula (env : Env) (f : Formula) : Prop :=
+  let (lhs, op, rhs) := f in
+    (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs).
+
+(* We normalize Formulas by moving terms to one side *)
+
+Inductive Op1 : Set := (* relations with 0 *)
+| Equal (* == 0 *)
+| NonEqual (* ~= 0 *)
+| Strict (* > 0 *)
+| NonStrict (* >= 0 *).
+
+Definition NFormula := (PExprC * Op1)%type. (* normalized formula *)
+
+Definition eval_op1 (o : Op1) : R -> Prop :=
+match o with
+| Equal => fun x => x == 0
+| NonEqual => fun x : R => x ~= 0
+| Strict => fun x : R => 0 < x
+| NonStrict => fun x : R => 0 <= x
+end.
+
+Definition eval_nformula (env : Env) (f : NFormula) : Prop :=
+let (p, op) := f in eval_op1 op (eval_pexpr env p).
+
+Definition normalise (f : Formula) : NFormula :=
+let (lhs, op, rhs) := f in
+  match op with
+  | OpEq => (PEsub lhs rhs, Equal)
+  | OpNEq => (PEsub lhs rhs, NonEqual)
+  | OpLe => (PEsub rhs lhs, NonStrict)
+  | OpGe => (PEsub lhs rhs, NonStrict)
+  | OpGt => (PEsub lhs rhs, Strict)
+  | OpLt => (PEsub rhs lhs, Strict)
+  end.
+
+Definition negate (f : Formula) : NFormula :=
+let (lhs, op, rhs) := f in
+  match op with
+  | OpEq => (PEsub rhs lhs, NonEqual)
+  | OpNEq => (PEsub rhs lhs, Equal)
+  | OpLe => (PEsub lhs rhs, Strict) (* e <= e' == ~ e > e' *)
+  | OpGe => (PEsub rhs lhs, Strict)
+  | OpGt => (PEsub rhs lhs, NonStrict)
+  | OpLt => (PEsub lhs rhs, NonStrict)
+end.
+
+Theorem normalise_sound :
+  forall (env : Env) (f : Formula),
+    eval_formula env f -> eval_nformula env (normalise f).
+Proof.
+intros env f H; destruct f as [lhs op rhs]; simpl in *.
+destruct op; simpl in *.
+now apply <- (Rminus_eq_0 sor).
+intros H1. apply -> (Rminus_eq_0 sor) in H1. now apply H.
+now apply -> (Rle_le_minus sor).
+now apply -> (Rle_le_minus sor).
+now apply -> (Rlt_lt_minus sor).
+now apply -> (Rlt_lt_minus sor).
+Qed.
+
+Theorem negate_correct :
+  forall (env : Env) (f : Formula),
+    eval_formula env f <-> ~ (eval_nformula env (negate f)).
+Proof.
+intros env f; destruct f as [lhs op rhs]; simpl.
+destruct op; simpl.
+symmetry. rewrite (Rminus_eq_0 sor).
+split; intro H; [symmetry; now apply -> (Req_dne sor) | symmetry in H; now apply <- (Req_dne sor)].
+rewrite (Rminus_eq_0 sor). split; intro; now apply (Rneq_symm sor).
+rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor).
+rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor).
+rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor).
+rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor).
+Qed.
+
+Definition OpMult (o o' : Op1) : Op1 :=
+match o with
+| Equal => Equal
+| NonStrict => NonStrict (* (OpMult NonStrict Equal) could be defined as Equal *)
+| Strict => o'
+| NonEqual => NonEqual (* does not matter what we return here; see the following lemmas *)
+end.
+
+Definition OpAdd (o o': Op1) : Op1 :=
+match o with
+| Equal => o'
+| NonStrict =>
+  match o' with
+  | Strict => Strict
+  | _ => NonStrict
+  end
+| Strict => Strict
+| NonEqual => NonEqual (* does not matter what we return here *)
+end.
+
+Lemma OpMultNonEqual :
+  forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpMult o o' <> NonEqual.
+Proof.
+intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
+try (intro H; apply H1; reflexivity);
+try (intro H; apply H2; reflexivity).
+Qed.
+
+Lemma OpAdd_NonEqual :
+  forall o o' : Op1, o <> NonEqual -> o' <> NonEqual -> OpAdd o o' <> NonEqual.
+Proof.
+intros o o' H1 H2; destruct o; destruct o'; simpl; try discriminate;
+try (intro H; apply H1; reflexivity);
+try (intro H; apply H2; reflexivity).
+Qed.
+
+Lemma OpMult_sound :
+  forall (o o' : Op1) (x y : R), o <> NonEqual -> o' <> NonEqual ->
+    eval_op1 o x -> eval_op1 o' y -> eval_op1 (OpMult o o') (x * y).
+Proof.
+unfold eval_op1; destruct o; simpl; intros o' x y H1 H2 H3 H4.
+rewrite H3; now rewrite (Rtimes_0_l sor).
+elimtype False; now apply H1.
+destruct o'.
+rewrite H4; now rewrite (Rtimes_0_r sor).
+elimtype False; now apply H2.
+now apply (Rtimes_pos_pos sor).
+apply (Rtimes_nonneg_nonneg sor); [le_less | assumption].
+destruct o'.
+rewrite H4, (Rtimes_0_r sor); le_equal.
+elimtype False; now apply H2.
+apply (Rtimes_nonneg_nonneg sor); [assumption | le_less].
+now apply (Rtimes_nonneg_nonneg sor).
+Qed.
+
+Lemma OpAdd_sound :
+  forall (o o' : Op1) (e e' : R), o <> NonEqual -> o' <> NonEqual ->
+    eval_op1 o e -> eval_op1 o' e' -> eval_op1 (OpAdd o o') (e + e').
+Proof.
+unfold eval_op1; destruct o; simpl; intros o' e e' H1 H2 H3 H4.
+destruct o'.
+now rewrite H3, H4, (Rplus_0_l sor).
+elimtype False; now apply H2.
+now rewrite H3, (Rplus_0_l sor).
+now rewrite H3, (Rplus_0_l sor).
+elimtype False; now apply H1.
+destruct o'.
+now rewrite H4, (Rplus_0_r sor).
+elimtype False; now apply H2.
+now apply (Rplus_pos_pos sor).
+now apply (Rplus_pos_nonneg sor).
+destruct o'.
+now rewrite H4, (Rplus_0_r sor).
+elimtype False; now apply H2.
+now apply (Rplus_nonneg_pos sor).
+now apply (Rplus_nonneg_nonneg sor).
+Qed.
+
+(* We consider a monoid whose generators are polynomials from the
+hypotheses of the form (p ~= 0). Thus it follows from the hypotheses that
+every element of the monoid (i.e., arbitrary product of generators) is ~=
+0. Therefore, the square of every element is > 0. *)
+
+Inductive Monoid (l : list NFormula) : PExprC -> Prop :=
+| M_One : Monoid l (PEc cI)
+| M_In : forall p : PExprC, In (p, NonEqual) l -> Monoid l p
+| M_Mult : forall (e1 e2 : PExprC), Monoid l e1 -> Monoid l e2 -> Monoid l (PEmul e1 e2).
+
+Inductive Cone (l : list (NFormula)) : PExprC -> Op1 -> Prop :=
+| InC : forall p op, In (p, op) l -> op <> NonEqual -> Cone l p op
+| IsIdeal : forall p, Cone l p Equal -> forall p', Cone l (PEmul p p') Equal
+| IsSquare : forall p, Cone l (PEmul p p) NonStrict
+| IsMonoid : forall p, Monoid l p -> Cone l (PEmul p p) Strict
+| IsMult : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEmul p q) (OpMult op oq)
+| IsAdd : forall p op q oq, Cone l p op -> Cone l q oq -> Cone l (PEadd p q) (OpAdd op oq)
+| IsPos : forall c : C, cltb cO c = true -> Cone l (PEc c) Strict
+| IsZ : Cone l (PEc cO) Equal.
+
+(* As promised, if all hypotheses are true in some environment, then every
+member of the monoid is nonzero in this environment *)
+
+Lemma monoid_nonzero : forall (l : list NFormula) (env : Env),
+  (forall f : NFormula, In f l -> eval_nformula env f) ->
+    forall p : PExprC, Monoid l p -> eval_pexpr env p ~= 0.
+Proof.
+intros l env H1 p H2. induction H2 as [| f H | e1 e2 H3 IH1 H4 IH2]; simpl.
+rewrite addon.(SORrm).(morph1). apply (Rneq_symm sor). apply (Rneq_0_1 sor).
+apply H1 in H. now simpl in H.
+simpl in IH1, IH2. apply (Rtimes_neq_0 sor). now split.
+Qed.
+
+(* If all members of a cone base are true in some environment, then every
+member of the cone is true as well *)
+
+Lemma cone_true :
+  forall (l : list NFormula) (env : Env),
+    (forall (f : NFormula), In f l -> eval_nformula env f) ->
+      forall (p : PExprC) (op : Op1), Cone l p op ->
+        op <> NonEqual /\ eval_nformula env (p, op).
+Proof.
+intros l env H1 p op H2. induction H2; simpl in *.
+split. assumption. apply H1 in H. now unfold eval_nformula in H.
+split. discriminate. destruct IHCone as [_ H3]. rewrite H3. now rewrite (Rtimes_0_l sor).
+split. discriminate. apply (Rtimes_square_nonneg sor).
+split. discriminate. apply <- (Rlt_le_neq sor). split. apply (Rtimes_square_nonneg sor).
+apply (Rneq_symm sor). apply (Rtimes_neq_0 sor). split; now apply monoid_nonzero with l.
+destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
+split. now apply OpMultNonEqual. now apply OpMult_sound.
+destruct IHCone1 as [IH1 IH2]; destruct IHCone2 as [IH3 IH4].
+split. now apply OpAdd_NonEqual. now apply OpAdd_sound.
+split. discriminate. rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
+split. discriminate. apply addon.(SORrm).(morph0).
+Qed.
+
+(* Every element of a monoid is a product of some generators; therefore,
+to determine an element we can give a list of generators' indices *)
+
+Definition MonoidMember : Set := list nat.
+
+Inductive ConeMember : Type :=
+| S_In : nat -> ConeMember
+| S_Ideal : PExprC -> ConeMember -> ConeMember
+| S_Square : PExprC -> ConeMember
+| S_Monoid : MonoidMember -> ConeMember
+| S_Mult : ConeMember -> ConeMember -> ConeMember
+| S_Add : ConeMember -> ConeMember -> ConeMember
+| S_Pos : forall c : C, cltb cO c = true -> ConeMember (* the proof of cltb 0 c = true should be (refl_equal true) *)
+| S_Z : ConeMember.
+
+Definition nformula_times (f f' : NFormula) : NFormula :=
+let (p, op) := f in
+  let (p', op') := f' in
+    (PEmul p p', OpMult op op').
+
+Definition nformula_plus (f f' : NFormula) : NFormula :=
+let (p, op) := f in
+  let (p', op') := f' in
+    (PEadd p p', OpAdd op op').
+
+Definition nformula_times_0 (p : PExprC) (f : NFormula) : NFormula :=
+let (q, op) := f in
+  match op with
+  | Equal => (PEmul q p, Equal)
+  | _ => f
+  end.
+
+Fixpoint eval_monoid (l : list NFormula) (ns : MonoidMember) {struct ns} : PExprC :=
+match ns with
+| nil => PEc cI
+| n :: ns =>
+  let p := match nth n l (PEc cI, NonEqual) with
+           | (q, NonEqual) => q
+           | _ => PEc cI
+           end in
+    PEmul p (eval_monoid l ns)
+end.
+
+Theorem eval_monoid_in_monoid :
+  forall (l : list NFormula) (ns : MonoidMember), Monoid l (eval_monoid l ns).
+Proof.
+intro l; induction ns; simpl in *.
+constructor.
+apply M_Mult; [| assumption].
+destruct (nth_in_or_default a l (PEc cI, NonEqual)).
+destruct (nth a l (PEc cI, NonEqual)). destruct o; try constructor. assumption.
+rewrite e; simpl. constructor.
+Qed.
+
+(* Provides the cone member from the witness, i.e., ConeMember *)
+Fixpoint eval_cone (l : list NFormula) (cm : ConeMember) {struct cm} : NFormula :=
+match cm with
+| S_In n => match nth n l (PEc cO, Equal) with
+            | (_, NonEqual) => (PEc cO, Equal)
+            | f => f
+            end
+| S_Ideal p cm' => nformula_times_0 p (eval_cone l cm')
+| S_Square p => (PEmul p p, NonStrict)
+| S_Monoid m => let p := eval_monoid l m in (PEmul p p, Strict)
+| S_Mult p q => nformula_times (eval_cone l p) (eval_cone l q)
+| S_Add p q => nformula_plus (eval_cone l p) (eval_cone l q)
+| S_Pos c _ => (PEc c, Strict)
+| S_Z => (PEc cO, Equal)
+end.
+
+Theorem eval_cone_in_cone :
+  forall (l : list NFormula) (cm : ConeMember),
+    let (p, op) := eval_cone l cm in Cone l p op.
+Proof.
+intros l cm; induction cm; simpl.
+destruct (nth_in_or_default n l (PEc cO, Equal)).
+destruct (nth n l (PEc cO, Equal)). destruct o; try (now apply InC). apply IsZ.
+rewrite e. apply IsZ.
+destruct (eval_cone l cm). destruct o; simpl; try assumption. now apply IsIdeal.
+apply IsSquare.
+apply IsMonoid. apply eval_monoid_in_monoid.
+destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_times. now apply IsMult.
+destruct (eval_cone l cm1). destruct (eval_cone l cm2). unfold nformula_plus. now apply IsAdd.
+now apply IsPos. apply IsZ.
+Qed.
+
+(* (inconsistent_cone_member l p) means (p, op) is in the cone for some op
+(> 0, >= 0, == 0, or ~= 0) and this formula is inconsistent. This fact
+implies that l is inconsistent, as shown by the next lemma. Inconsistency
+of a formula (p, op) can be established by normalizing p and showing that
+it is a constant c for which (c, op) is false. (This is only a sufficient,
+not necessary, condition, of course.) Membership in the cone can be
+verified if we have a certificate. *)
+
+Definition inconsistent_cone_member (l : list NFormula) (p : PExprC) :=
+  exists op : Op1, Cone l p op /\
+    forall env : Env, ~ eval_op1 op (eval_pexpr env p).
+
+Implicit Arguments make_impl [A].
+
+(* If some element of a cone is inconsistent, then the base of the cone
+is also inconsistent *)
+
+Lemma prove_inconsistent :
+  forall (l : list NFormula) (p : PExprC),
+    inconsistent_cone_member l p -> forall env, make_impl (eval_nformula env) l False.
+Proof.
+intros l p H env.
+destruct H as [o [wit H]].
+apply -> make_conj_impl.
+intro H1. apply H with env.
+pose proof (@cone_true l env) as H2.
+cut (forall f : NFormula, In f l -> eval_nformula env f). intro H3.
+apply (proj2 (H2 H3 p o wit)). intro. now apply make_conj_in.
+Qed.
+
+Definition normalise_pexpr : PExprC -> PolC :=
+  norm_aux cO cI cplus ctimes cminus copp ceqb.
+
+Let Reqe := mk_reqe rplus rtimes ropp req
+  sor.(SORplus_wd)
+  sor.(SORtimes_wd)
+  sor.(SORopp_wd).
+
+Theorem normalise_pexpr_correct :
+  forall (env : Env) (e : PExprC), eval_pexpr env e == eval_pol env (normalise_pexpr e).
+intros env e. unfold eval_pexpr, eval_pol, normalise_pexpr.
+apply (norm_aux_spec sor.(SORsetoid) Reqe (Rth_ARth sor.(SORsetoid) Reqe sor.(SORrt))
+addon.(SORrm) addon.(SORpower) nil). constructor.
+Qed.
+
+(* Check that a formula f is inconsistent by normalizing and comparing the
+resulting constant with 0 *)
+
+Definition check_inconsistent (f : NFormula) : bool :=
+let (e, op) := f in
+  match normalise_pexpr e with
+  | Pc c =>
+    match op with
+    | Equal => cneqb c cO
+    | NonStrict => c [<] cO
+    | Strict => c [<=] cO
+    | NonEqual => false (* eval_cone never returns (p, NonEqual) *)
+    end
+  | _ => false (* not a constant *)
+  end.
+
+Lemma check_inconsistent_sound :
+  forall (p : PExprC) (op : Op1),
+    check_inconsistent (p, op) = true -> forall env, ~ eval_op1 op (eval_pexpr env p).
+Proof.
+intros p op H1 env. unfold check_inconsistent in H1.
+destruct op; simpl; rewrite normalise_pexpr_correct;
+destruct (normalise_pexpr p); simpl; try discriminate H1;
+rewrite <- addon.(SORrm).(morph0).
+now apply cneqb_sound.
+apply cleb_sound in H1. now apply -> (Rle_ngt sor).
+apply cltb_sound in H1. now apply -> (Rlt_nge sor).
+Qed.
+
+Definition check_normalised_formulas : list NFormula -> ConeMember -> bool :=
+  fun l cm => check_inconsistent (eval_cone l cm).
+
+Lemma checker_nf_sound :
+  forall (l : list NFormula) (cm : ConeMember),
+    check_normalised_formulas l cm = true ->
+      forall env : Env, make_impl (eval_nformula env) l False.
+Proof.
+intros l cm H env.
+unfold check_normalised_formulas in H.
+case_eq (eval_cone l cm). intros p op H1.
+apply prove_inconsistent with p. unfold inconsistent_cone_member. exists op. split.
+pose proof (eval_cone_in_cone l cm) as H2. now rewrite H1 in H2.
+apply check_inconsistent_sound. now rewrite <- H1.
+Qed.
+
+Definition check_formulas :=
+  CheckerMaker.check_formulas normalise check_normalised_formulas.
+
+Theorem check_formulas_sound :
+  forall (l : list Formula) (w : ConeMember),
+    check_formulas l w = true ->
+      forall env : Env, make_impl (eval_formula env) l False.
+Proof.
+exact (CheckerMaker.check_formulas_sound eval_formula eval_nformula normalise
+       normalise_sound check_normalised_formulas checker_nf_sound).
+Qed.
+
+Definition check_conj_formulas :=
+  CheckerMaker.check_conj_formulas normalise negate check_normalised_formulas.
+
+Theorem check_conj_formulas_sound :
+  forall (l1 : list Formula) (l2 : list Formula) (ws : list ConeMember),
+    check_conj_formulas l1 ws l2 = true ->
+      forall env : Env, make_impl (eval_formula env) l1 (make_conj (eval_formula env) l2).
+Proof.
+exact (check_conj_formulas_sound eval_formula eval_nformula normalise negate
+       normalise_sound negate_correct check_normalised_formulas checker_nf_sound).
+Qed.
+
+End Micromega.
+
diff --git a/contrib/micromega/ZCoeff.v b/contrib/micromega/ZCoeff.v
new file mode 100644
index 0000000000..20c9007804
--- /dev/null
+++ b/contrib/micromega/ZCoeff.v
@@ -0,0 +1,142 @@
+Require Import OrderedRing.
+Require Import RingMicromega.
+Require Import ZArith.
+Require Import InitialRing.
+Require Import Setoid.
+
+Import OrderedRingSyntax.
+
+Set Implicit Arguments.
+
+Section InitialMorphism.
+
+Variable R : Type.
+Variables rO rI : R.
+Variables rplus rtimes rminus: R -> R -> R.
+Variable ropp : R -> R.
+Variables req rle rlt : R -> R -> Prop.
+
+Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
+
+Notation "0" := rO.
+Notation "1" := rI.
+Notation "x + y" := (rplus x y).
+Notation "x * y " := (rtimes x y).
+Notation "x - y " := (rminus x y).
+Notation "- x" := (ropp x).
+Notation "x == y" := (req x y).
+Notation "x ~= y" := (~ req x y).
+Notation "x <= y" := (rle x y).
+Notation "x < y" := (rlt x y).
+
+Add Relation R req
+  reflexivity proved by sor.(SORsetoid).(Seq_refl _ _)
+  symmetry proved by sor.(SORsetoid).(Seq_sym _ _)
+  transitivity proved by sor.(SORsetoid).(Seq_trans _ _)
+as sor_setoid.
+
+Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
+Proof.
+exact sor.(SORplus_wd).
+Qed.
+Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
+Proof.
+exact sor.(SORtimes_wd).
+Qed.
+Add Morphism ropp with signature req ==> req as ropp_morph.
+Proof.
+exact sor.(SORopp_wd).
+Qed.
+Add Morphism rle with signature req ==> req ==> iff as rle_morph.
+Proof.
+exact sor.(SORle_wd).
+Qed.
+Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
+Proof.
+exact sor.(SORlt_wd).
+Qed.
+Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
+Proof (rminus_morph sor).
+
+Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
+Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
+
+Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp.
+
+Notation phi_pos := (gen_phiPOS 1 rplus rtimes).
+Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes).
+
+Notation "[ x ]" := (gen_order_phi_Z x).
+
+Lemma ring_ops_wd : ring_eq_ext rplus rtimes ropp req.
+Proof.
+constructor.
+exact rplus_morph.
+exact rtimes_morph.
+exact ropp_morph.
+Qed.
+
+Lemma Zring_morph :
+  ring_morph 0 1 rplus rtimes rminus ropp req
+             0%Z 1%Z Zplus Zmult Zminus Zopp
+             Zeq_bool gen_order_phi_Z.
+Proof.
+exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)).
+Qed.
+
+Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x.
+Proof.
+induction x as [x IH | x IH |]; simpl;
+try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_pos_pos sor);
+try apply (Rlt_0_1 sor); assumption.
+Qed.
+
+Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Psucc x) == 1 + phi_pos1 x.
+Proof.
+exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd
+        (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))).
+Qed.
+
+Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
+Proof.
+intros x y H. pattern y; apply Plt_ind with x.
+rewrite phi_pos1_succ; apply (Rlt_succ_r sor).
+clear y H; intros y _ H. rewrite phi_pos1_succ. now apply (Rlt_lt_succ sor).
+assumption.
+Qed.
+
+Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].
+Proof.
+unfold Zlt; intros x y H;
+do 2 rewrite (same_genZ sor.(SORsetoid) ring_ops_wd sor.(SORrt));
+destruct x; destruct y; simpl in *; try discriminate.
+apply phi_pos1_pos.
+now apply clt_pos_morph.
+apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
+apply (Rlt_trans sor) with 0. apply <- (Ropp_neg_pos sor); apply phi_pos1_pos.
+apply phi_pos1_pos.
+rewrite Pcompare_antisym in H; simpl in H. apply -> (Ropp_lt_mono sor).
+now apply clt_pos_morph.
+Qed.
+
+Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y].
+Proof.
+unfold Zle_bool; intros x y H.
+case_eq (x ?= y)%Z; intro H1; rewrite H1 in H.
+le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1.
+le_less. now apply clt_morph.
+discriminate.
+Qed.
+
+Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y].
+Proof.
+intros x y H. unfold Zeq_bool in H.
+case_eq (Zcompare x y); intro H1; rewrite H1 in *; (discriminate || clear H).
+apply (Rlt_neq sor). now apply clt_morph.
+fold (x > y)%Z in H1. rewrite Zgt_iff_lt in H1.
+apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph.
+Qed.
+
+End InitialMorphism.
+
+