diff options
Diffstat (limited to 'contrib/micromega')
| -rw-r--r-- | contrib/micromega/CheckerMaker.v | 121 | ||||
| -rw-r--r-- | contrib/micromega/Examples.v | 103 | ||||
| -rw-r--r-- | contrib/micromega/OrderedRing.v | 443 | ||||
| -rw-r--r-- | contrib/micromega/Refl.v | 74 | ||||
| -rw-r--r-- | contrib/micromega/RingMicromega.v | 570 | ||||
| -rw-r--r-- | contrib/micromega/ZCoeff.v | 142 |
6 files changed, 1453 insertions, 0 deletions
diff --git a/contrib/micromega/CheckerMaker.v b/contrib/micromega/CheckerMaker.v new file mode 100644 index 000000000..8aeada77b --- /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 000000000..976815142 --- /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 000000000..ac1833a13 --- /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 000000000..8dced223b --- /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 000000000..2d565321a --- /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 000000000..20c900780 --- /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. + + |