diff options
| -rwxr-xr-x | configure | 10 | ||||
| -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 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 30 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZOrder.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlusOrder.v | 107 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZTimesOrder.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 220 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 7 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPlusOrder.v | 67 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZTimesOrder.v | 43 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NPlusOrder.v | 87 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NTimesOrder.v | 46 |
20 files changed, 1729 insertions, 361 deletions
@@ -399,24 +399,24 @@ esac # Very basic for the moment: if camlp5 exists, we use it... if [ "$camlp5dir" != "" ]; then - CAMLP4=camlp5 + CAMLP4=$camlp5dir CAMLP4LIB=$camlp5dir camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` elif [ "$CAMLTAG" = "OCAML310" ]; then if [ -x "${CAMLLIB}/camlp5" ]; then - CAMLP4LIB=+camlp5 + CAMLP4=camlp5 elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then - CAMLP4LIB=+site-lib/camlp5 + CAMLP4=site-lib/camlp5 else echo "Objective Caml 3.10 found but no Camlp5 installed." echo "Configuration script failed!" exit 1 fi - CAMLP4=camlp5 + CAMLP4LIB=+$CAMLP4 camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'` else CAMLP4=camlp4 - CAMLP4LIB=+camlp4 + CAMLP4LIB=+$CAMLP4 fi if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then 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. + + diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index fafc3285bc..d7486bc2bb 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -965,6 +965,11 @@ Proof. rewrite H; apply Pcompare_p_Sp. Qed. +Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m. +Proof. +unfold Plt; intros n m H; apply <- Pcompare_p_Sq; now left. +Qed. + (** 1 is the least positive number *) Lemma Pcompare_1 : forall p, ~ (p ?= xH) Eq = Lt. @@ -972,6 +977,31 @@ Proof. destruct p; discriminate. Qed. +Lemma Plt_irrefl : forall p : positive, ~ p < p. +Proof. +intro p; unfold Plt; rewrite Pcompare_refl; discriminate. +Qed. + +Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p. +Proof. +intros n m p; unfold Plt; elim p using Pind. +intros _ H; false_hyp H Pcompare_1. +clear p; intros p IH H1 H2. apply -> Pcompare_p_Sq in H2. +apply Plt_lt_succ. destruct H2 as [H2 | H2]. +now apply IH. now rewrite H2 in H1. +Qed. + +Theorem Plt_ind : forall (A : positive -> Prop) (n : positive), + A (Psucc n) -> + (forall m : positive, n < m -> A m -> A (Psucc m)) -> + forall m : positive, n < m -> A m. +Proof. +intros A n AB AS m. elim m using Pind; unfold Plt. +intro H; false_hyp H Pcompare_1. +clear m; intros m H1 H2. apply -> Pcompare_p_Sq in H2. destruct H2 as [H2 | H2]. +auto. now rewrite <- H2. +Qed. + (**********************************************************************) (** Properties of subtraction on binary positive numbers *) diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index ab863eb1f6..bde3d9a920 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -10,7 +10,7 @@ Open Local Scope NatIntScope. Notation Z := NZ (only parsing). Notation E := NZE (only parsing). -Parameter Inline Zopp : Z -> Z. +Parameter Zopp : Z -> Z. Add Morphism Zopp with signature E ==> E as Zopp_wd. diff --git a/theories/Numbers/Integer/Abstract/ZOrder.v b/theories/Numbers/Integer/Abstract/ZOrder.v index 295f5355aa..e0ef2f15d9 100644 --- a/theories/Numbers/Integer/Abstract/ZOrder.v +++ b/theories/Numbers/Integer/Abstract/ZOrder.v @@ -23,6 +23,9 @@ Proof NZlt_le_incl. Theorem Zlt_neq : forall n m : Z, n < m -> n ~= m. Proof NZlt_neq. +Theorem Zlt_le_neq : forall n m : Z, n < m <-> n <= m /\ n ~= m. +Proof NZlt_le_neq. + Theorem Zle_refl : forall n : Z, n <= n. Proof NZle_refl. diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index bab1bb4a08..6a13aa3db6 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -30,14 +30,32 @@ Proof NZplus_lt_le_mono. Theorem Zplus_le_lt_mono : forall n m p q : Z, n <= m -> p < q -> n + p < m + q. Proof NZplus_le_lt_mono. +Theorem Zplus_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n + m. +Proof NZplus_pos_pos. + +Theorem Zplus_pos_nonneg : forall n m : Z, 0 < n -> 0 <= m -> 0 < n + m. +Proof NZplus_pos_nonneg. + +Theorem Zplus_nonneg_pos : forall n m : Z, 0 <= n -> 0 < m -> 0 < n + m. +Proof NZplus_nonneg_pos. + +Theorem Zplus_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof NZplus_nonneg_nonneg. + +Theorem Zlt_plus_pos_l : forall n m : Z, 0 < n -> m < n + m. +Proof NZlt_plus_pos_l. + +Theorem Zlt_plus_pos_r : forall n m : Z, 0 < n -> m < m + n. +Proof NZlt_plus_pos_r. + Theorem Zle_lt_plus_lt : forall n m p q : Z, n <= m -> p + m < q + n -> p < q. Proof NZle_lt_plus_lt. Theorem Zlt_le_plus_lt : forall n m p q : Z, n < m -> p + m <= q + n -> p < q. Proof NZlt_le_plus_lt. -Theorem Zle_le_plus_lt : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. -Proof NZle_le_plus_lt. +Theorem Zle_le_plus_le : forall n m p q : Z, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_plus_le. Theorem Zplus_lt_cases : forall n m p q : Z, n + m < p + q -> n < p \/ m < q. Proof NZplus_lt_cases. @@ -57,89 +75,6 @@ Proof NZplus_nonpos_cases. Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m. Proof NZplus_nonneg_cases. -(** Multiplication and order *) - -Theorem Ztimes_lt_pred : - forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). -Proof NZtimes_lt_pred. - -Theorem Ztimes_lt_mono_pos_l : forall p n m : Z, 0 < p -> (n < m <-> p * n < p * m). -Proof NZtimes_lt_mono_pos_l. - -Theorem Ztimes_lt_mono_pos_r : forall p n m : Z, 0 < p -> (n < m <-> n * p < m * p). -Proof NZtimes_lt_mono_pos_r. - -Theorem Ztimes_lt_mono_neg_l : forall p n m : Z, p < 0 -> (n < m <-> p * m < p * n). -Proof NZtimes_lt_mono_neg_l. - -Theorem Ztimes_lt_mono_neg_r : forall p n m : Z, p < 0 -> (n < m <-> m * p < n * p). -Proof NZtimes_lt_mono_neg_r. - -Theorem Ztimes_le_mono_nonneg_l : forall n m p : Z, 0 <= p -> n <= m -> p * n <= p * m. -Proof NZtimes_le_mono_nonneg_l. - -Theorem Ztimes_le_mono_nonpos_l : forall n m p : Z, p <= 0 -> n <= m -> p * m <= p * n. -Proof NZtimes_le_mono_nonpos_l. - -Theorem Ztimes_le_mono_nonneg_r : forall n m p : Z, 0 <= p -> n <= m -> n * p <= m * p. -Proof NZtimes_le_mono_nonneg_r. - -Theorem Ztimes_le_mono_nonpos_r : forall n m p : Z, p <= 0 -> n <= m -> m * p <= n * p. -Proof NZtimes_le_mono_nonpos_r. - -Theorem Ztimes_cancel_l : forall n m p : Z, p ~= 0 -> (p * n == p * m <-> n == m). -Proof NZtimes_cancel_l. - -Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m). -Proof NZtimes_le_mono_pos_l. - -Theorem Ztimes_le_mono_pos_r : forall n m p : Z, 0 < p -> (n <= m <-> n * p <= m * p). -Proof NZtimes_le_mono_pos_r. - -Theorem Ztimes_le_mono_neg_l : forall n m p : Z, p < 0 -> (n <= m <-> p * m <= p * n). -Proof NZtimes_le_mono_neg_l. - -Theorem Ztimes_le_mono_neg_r : forall n m p : Z, p < 0 -> (n <= m <-> m * p <= n * p). -Proof NZtimes_le_mono_neg_r. - -Theorem Ztimes_lt_mono : - forall n m p q : Z, 0 <= n -> n < m -> 0 <= p -> p < q -> n * p < m * q. -Proof NZtimes_lt_mono. - -Theorem Ztimes_le_mono : - forall n m p q : Z, 0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q. -Proof NZtimes_le_mono. - -Theorem Ztimes_pos_pos : forall n m : Z, 0 < n -> 0 < m -> 0 < n * m. -Proof NZtimes_pos_pos. - -Theorem Ztimes_nonneg_nonneg : forall n m : Z, 0 <= n -> 0 <= m -> 0 <= n * m. -Proof NZtimes_nonneg_nonneg. - -Theorem Ztimes_neg_neg : forall n m : Z, n < 0 -> m < 0 -> 0 < n * m. -Proof NZtimes_neg_neg. - -Theorem Ztimes_nonpos_nonpos : forall n m : Z, n <= 0 -> m <= 0 -> 0 <= n * m. -Proof NZtimes_nonpos_nonpos. - -Theorem Ztimes_pos_neg : forall n m : Z, 0 < n -> m < 0 -> n * m < 0. -Proof NZtimes_pos_neg. - -Theorem Ztimes_nonneg_nonpos : forall n m : Z, 0 <= n -> m <= 0 -> n * m <= 0. -Proof NZtimes_nonneg_nonpos. - -Theorem Ztimes_neg_pos : forall n m : Z, n < 0 -> 0 < m -> n * m < 0. -Proof NZtimes_neg_pos. - -Theorem Ztimes_nonpos_nonneg : forall n m : Z, n <= 0 -> 0 <= m -> n * m <= 0. -Proof NZtimes_nonpos_nonneg. - -Theorem Ztimes_eq_0 : forall n m : Z, n * m == 0 -> n == 0 \/ m == 0. -Proof NZtimes_eq_0. - -Theorem Ztimes_neq_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZtimes_neq_0. - (** Theorems that are either not valid on N or have different proofs on N and Z *) (** Minus and order *) @@ -252,7 +187,7 @@ Qed. Theorem Zle_le_minus_lt : forall n m p q : Z, n <= m -> p - n <= q - m -> p <= q. Proof. -intros n m p q H1 H2. apply (Zle_le_plus_lt (- m) (- n)); +intros n m p q H1 H2. apply (Zle_le_plus_le (- m) (- n)); [now apply -> Zopp_le_mono | now do 2 rewrite Zplus_opp_minus]. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index d63dc0d8c6..4381420950 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -94,6 +94,9 @@ Theorem Ztimes_neg : forall n m : Z, n * m < 0 <-> (n < 0 /\ m > 0) \/ (n > 0 /\ m < 0). Proof NZtimes_neg. +Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZtimes_2_mono_l. + (** Theorems that are either not valid on N or have different proofs on N and Z *) (* None? *) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index cb8ac3b5b1..0a52d214a2 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -132,7 +132,14 @@ Qed. End NZOrdAxiomsMod. -Definition Zopp := Zopp. +Definition Zopp (x : Z) := +match x with +| Z0 => Z0 +| Zpos x => Zneg x +| Zneg x => Zpos x +end. + +Notation "- x" := (Zopp x) : Z_scope. Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd. Proof. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 5c8b5890d5..9a012b26cf 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -1,48 +1,82 @@ Require Import NMinus. (* The most complete file for natural numbers *) -Require Import ZTimesOrder. (* The most complete file for integers *) +Require Export ZTimesOrder. (* The most complete file for integers *) Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig. Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *) -Notation Local N := NZ. (* To remember N without having to use a long qualifying name *) -Notation Local NE := NZE (only parsing). -Notation Local plus_wd := NZplus_wd (only parsing). + +(* The definitios of functions (NZplus, NZtimes, etc.) will be unfolded by +the properties functor. Since we don't want Zplus_comm to refer to unfolded +definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1), +we will provide an extra layer of definitions. *) + Open Local Scope NatIntScope. +Definition Z := (N * N)%type. +Definition Z0 : Z := (0, 0). +Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). +Definition Zsucc (n : Z) : Z := (S (fst n), snd n). +Definition Zpred (n : Z) : Z := (fst n, S (snd n)). -Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. -Module Export NZAxiomsMod <: NZAxiomsSig. +(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc n) = n. It +could be possible to consider as canonical only pairs where one of the +elements is 0, and make all operations convert canonical values into other +canonical values. In that case, we could get rid of setoids as well as +arrive at integers as signed natural numbers. *) + +Definition Zplus (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)). +Definition Zminus (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)). -Definition NZ : Set := (NZ * NZ)%type. -Definition NZE (p1 p2 : NZ) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). -Notation Z := NZ (only parsing). -Notation E := NZE (only parsing). -Definition NZ0 := (0, 0). -Definition NZsucc (n : Z) := (S (fst n), snd n). -Definition NZpred (n : Z) := (fst n, S (snd n)). -(* We do not have P (S n) = n but only P (S n) == n. It could be possible -to consider as canonical only pairs where one of the elements is 0, and -make all operations convert canonical values into other canonical values. -In that case, we could get rid of setoids as well as arrive at integers as -signed natural numbers. *) -Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)). -Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)). (* Unfortunately, the elements of the pair keep increasing, even during subtraction *) -Definition NZtimes (n m : Z) := + +Definition Ztimes (n m : Z) : Z := ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)). +Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n). +Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n). -Theorem ZE_refl : reflexive Z E. +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z. +Notation "x == y" := (Zeq x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope. +Notation "0" := Z0 : IntScope. +Notation "1" := (Zsucc Z0) : IntScope. +Notation "x + y" := (Zplus x y) : IntScope. +Notation "x - y" := (Zminus x y) : IntScope. +Notation "x * y" := (Ztimes x y) : IntScope. +Notation "x < y" := (Zlt x y) : IntScope. +Notation "x <= y" := (Zle x y) : IntScope. +Notation "x > y" := (Zlt y x) (only parsing) : IntScope. +Notation "x >= y" := (Zle y x) (only parsing) : IntScope. + +Notation Local N := NZ. +(* To remember N without having to use a long qualifying name. since NZ will be redefined *) +Notation Local NE := NZE (only parsing). +Notation Local plus_wd := NZplus_wd (only parsing). + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ : Set := Z. +Definition NZE := Zeq. +Definition NZ0 := Z0. +Definition NZsucc := Zsucc. +Definition NZpred := Zpred. +Definition NZplus := Zplus. +Definition NZminus := Zminus. +Definition NZtimes := Ztimes. + +Theorem ZE_refl : reflexive Z Zeq. Proof. -unfold reflexive, E; reflexivity. +unfold reflexive, Zeq. reflexivity. Qed. -Theorem ZE_symm : symmetric Z E. +Theorem ZE_symm : symmetric Z Zeq. Proof. -unfold symmetric, E; now symmetry. +unfold symmetric, Zeq; now symmetry. Qed. -Theorem ZE_trans : transitive Z E. +Theorem ZE_trans : transitive Z Zeq. Proof. -unfold transitive, E. intros n m p H1 H2. +unfold transitive, Zeq. intros n m p H1 H2. assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m)) by now apply plus_wd. stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring. @@ -50,46 +84,46 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring. now apply -> plus_cancel_r in H3. Qed. -Theorem NZE_equiv : equiv Z E. +Theorem NZE_equiv : equiv Z Zeq. Proof. unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm]. Qed. -Add Relation Z E +Add Relation Z Zeq reflexivity proved by (proj1 NZE_equiv) symmetry proved by (proj2 (proj2 NZE_equiv)) transitivity proved by (proj1 (proj2 NZE_equiv)) as NZE_rel. -Add Morphism (@pair N N) with signature NE ==> NE ==> E as Zpair_wd. +Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd. Proof. -intros n1 n2 H1 m1 m2 H2; unfold E; simpl; rewrite H1; now rewrite H2. +intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2. Qed. -Add Morphism NZsucc with signature E ==> E as NZsucc_wd. +Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd. Proof. -unfold NZsucc, E; intros n m H; simpl. +unfold NZsucc, Zeq; intros n m H; simpl. do 2 rewrite plus_succ_l; now rewrite H. Qed. -Add Morphism NZpred with signature E ==> E as NZpred_wd. +Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd. Proof. -unfold NZpred, E; intros n m H; simpl. +unfold NZpred, Zeq; intros n m H; simpl. do 2 rewrite plus_succ_r; now rewrite H. Qed. -Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd. +Add Morphism NZplus with signature Zeq ==> Zeq ==> Zeq as NZplus_wd. Proof. -unfold E, NZplus; intros n1 m1 H1 n2 m2 H2; simpl. +unfold Zeq, NZplus; intros n1 m1 H1 n2 m2 H2; simpl. assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2)) by now apply plus_wd. stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. Qed. -Add Morphism NZminus with signature E ==> E ==> E as NZminus_wd. +Add Morphism NZminus with signature Zeq ==> Zeq ==> Zeq as NZminus_wd. Proof. -unfold E, NZminus; intros n1 m1 H1 n2 m2 H2; simpl. +unfold Zeq, NZminus; intros n1 m1 H1 n2 m2 H2; simpl. symmetry in H2. assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2)) by now apply plus_wd. @@ -97,9 +131,9 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring. now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring. Qed. -Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd. +Add Morphism NZtimes with signature Zeq ==> Zeq ==> Zeq as NZtimes_wd. Proof. -unfold NZtimes, E; intros n1 m1 H1 n2 m2 H2; simpl. +unfold NZtimes, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring. apply plus_times_repl_pair with (n := fst m2) (m := snd m2); [| now idtac]. @@ -117,39 +151,20 @@ apply plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac]. ring. Qed. -Delimit Scope IntScope with Int. -Bind Scope IntScope with NZ. -Open Local Scope IntScope. -Notation "x == y" := (NZE x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope. -Notation "0" := NZ0 : IntScope. -Notation "'S'" := NZsucc : IntScope. -Notation "'P'" := NZpred : IntScope. -Notation "1" := (S 0) : IntScope. -Notation "x + y" := (NZplus x y) : IntScope. -Notation "x - y" := (NZminus x y) : IntScope. -Notation "x * y" := (NZtimes x y) : IntScope. - -Theorem NZpred_succ : forall n : Z, P (S n) == n. -Proof. -unfold NZpred, NZsucc, E; intro n; simpl. -rewrite plus_succ_l; now rewrite plus_succ_r. -Qed. - Section Induction. Open Scope NatIntScope. (* automatically closes at the end of the section *) Variable A : Z -> Prop. -Hypothesis A_wd : predicate_wd E A. +Hypothesis A_wd : predicate_wd Zeq A. -Add Morphism A with signature E ==> iff as A_morph. +Add Morphism A with signature Zeq ==> iff as A_morph. Proof. exact A_wd. Qed. Theorem NZinduction : - A 0 -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) + A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) Proof. -intros A0 AS n; unfold NZ0, NZsucc, predicate_wd, fun_wd, E in *. +intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *. destruct n as [n m]. cut (forall p : N, A (p, 0)); [intro H1 |]. cut (forall p : N, A (0, p)); [intro H2 |]. @@ -166,51 +181,56 @@ Qed. End Induction. +(* Time to prove theorems in the language of Z *) + +Open Local Scope IntScope. + +Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n. +Proof. +unfold NZpred, NZsucc, Zeq; intro n; simpl. +rewrite plus_succ_l; now rewrite plus_succ_r. +Qed. + Theorem NZplus_0_l : forall n : Z, 0 + n == n. Proof. -intro n; unfold NZplus, E; simpl. now do 2 rewrite plus_0_l. +intro n; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_0_l. Qed. -Theorem NZplus_succ_l : forall n m : Z, (S n) + m == S (n + m). +Theorem NZplus_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m). Proof. -intros n m; unfold NZplus, E; simpl. now do 2 rewrite plus_succ_l. +intros n m; unfold NZplus, Zeq; simpl. now do 2 rewrite plus_succ_l. Qed. Theorem NZminus_0_r : forall n : Z, n - 0 == n. Proof. -intro n; unfold NZminus, E; simpl. now do 2 rewrite plus_0_r. +intro n; unfold NZminus, Zeq; simpl. now do 2 rewrite plus_0_r. Qed. -Theorem NZminus_succ_r : forall n m : Z, n - (S m) == P (n - m). +Theorem NZminus_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). Proof. -intros n m; unfold NZminus, E; simpl. symmetry; now rewrite plus_succ_r. +intros n m; unfold NZminus, Zeq; simpl. symmetry; now rewrite plus_succ_r. Qed. Theorem NZtimes_0_r : forall n : Z, n * 0 == 0. Proof. -intro n; unfold NZtimes, E; simpl. +intro n; unfold NZtimes, Zeq; simpl. repeat rewrite times_0_r. now rewrite plus_assoc. Qed. -Theorem NZtimes_succ_r : forall n m : Z, n * (S m) == n * m + n. +Theorem NZtimes_succ_r : forall n m : Z, n * (Zsucc m) == n * m + n. Proof. -intros n m; unfold NZtimes, NZsucc, E; simpl. +intros n m; unfold NZtimes, NZsucc, Zeq; simpl. do 2 rewrite times_succ_r. ring. Qed. End NZAxiomsMod. -Definition NZlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n). -Definition NZle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n). - -Notation "x < y" := (NZlt x y) : IntScope. -Notation "x <= y" := (NZle x y) : IntScope. -Notation "x > y" := (NZlt y x) (only parsing) : IntScope. -Notation "x >= y" := (NZle y x) (only parsing) : IntScope. +Definition NZlt := Zlt. +Definition NZle := Zle. -Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd. +Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd. Proof. -unfold NZlt, E; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. +unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. stepr (snd m1 + fst m2) by apply plus_comm. apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption]. stepl (snd m2 + fst n1) by apply plus_comm. @@ -227,58 +247,58 @@ now stepl (fst m1 + snd m2) by apply plus_comm. stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm. Qed. -Open Local Scope IntScope. - -Add Morphism NZle with signature E ==> E ==> iff as NZle_wd. +Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd. Proof. -unfold NZle, E; intros n1 m1 H1 n2 m2 H2; simpl. -do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2). -fold (n1 == n2) (m1 == m2); fold (n1 == m1) in H1; fold (n2 == m2) in H2. +unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. +do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int. +fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%Int in H2. now rewrite H1, H2. Qed. +Open Local Scope IntScope. + Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m. Proof. -intros n m; unfold NZlt, NZle, E; simpl. apply le_lt_or_eq. +intros n m; unfold Zlt, Zle, Zeq; simpl. apply le_lt_or_eq. Qed. Theorem NZlt_irrefl : forall n : Z, ~ (n < n). Proof. -intros n; unfold NZlt, E; simpl. apply lt_irrefl. +intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl. Qed. -Theorem NZlt_succ_le : forall n m : Z, n < (S m) <-> n <= m. +Theorem NZlt_succ_le : forall n m : Z, n < (Zsucc m) <-> n <= m. Proof. -intros n m; unfold NZlt, NZle, E; simpl. rewrite plus_succ_l; apply lt_succ_le. +intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite plus_succ_l; apply lt_succ_le. Qed. End NZOrdAxiomsMod. -Definition Zopp (n : Z) := (snd n, fst n). +Definition Zopp (n : Z) : Z := (snd n, fst n). -Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. +Notation "- x" := (Zopp x) : IntScope. -Add Morphism Zopp with signature E ==> E as Zopp_wd. +Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. Proof. -unfold E; intros n m H; simpl. symmetry. +unfold Zeq; intros n m H; simpl. symmetry. stepl (fst n + snd m) by apply plus_comm. now stepr (fst m + snd n) by apply plus_comm. Qed. Open Local Scope IntScope. -Theorem Zsucc_pred : forall n : Z, S (P n) == n. +Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n. Proof. -intro n; unfold NZsucc, NZpred, E; simpl. +intro n; unfold Zsucc, Zpred, Zeq; simpl. rewrite plus_succ_l; now rewrite plus_succ_r. Qed. Theorem Zopp_0 : - 0 == 0. Proof. -unfold Zopp, E; simpl. now rewrite plus_0_l. +unfold Zopp, Zeq; simpl. now rewrite plus_0_l. Qed. -Theorem Zopp_succ : forall n, - (S n) == P (- n). +Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n). Proof. reflexivity. Qed. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 5c6369fe49..cb3dd3093f 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -44,6 +44,13 @@ Proof. intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl. Qed. +Theorem NZlt_le_neq : forall n m : NZ, n < m <-> n <= m /\ n ~= m. +Proof. +intros n m; split; [intro H | intros [H1 H2]]. +split. le_less. now apply NZlt_neq. +le_elim H1. assumption. false_hyp H1 H2. +Qed. + Theorem NZle_refl : forall n : NZ, n <= n. Proof. intro; now le_equal. diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v deleted file mode 100644 index 6368fa5578..0000000000 --- a/theories/Numbers/NatInt/NZPlusOrder.v +++ /dev/null @@ -1,67 +0,0 @@ -Require Export NZPlus. -Require Export NZOrder. - -Module NZPlusOrderPropFunct - (Import NZPlusMod : NZPlusSig) - (Import NZOrderMod : NZOrderSig with Module NZBaseMod := NZPlusMod.NZBaseMod). - -Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod. -Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod. -Open Local Scope NatIntScope. - -Theorem NZplus_lt_mono_l : forall n m p, n < m <-> p + n < p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZplus_0_l. -intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_lt_mono. -Qed. - -Theorem NZplus_lt_mono_r : forall n m p, n < m <-> n + p < m + p. -Proof. -intros n m p. -rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_lt_mono_l. -Qed. - -Theorem NZplus_lt_mono : forall n m p q, n < m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_trans with (m + p); -[now apply -> NZplus_lt_mono_r | now apply -> NZplus_lt_mono_l]. -Qed. - -Theorem NZplus_le_mono_l : forall n m p, n <= m <-> p + n <= p + m. -Proof. -intros n m p; NZinduct p. -now do 2 rewrite NZplus_0_l. -intro p. do 2 rewrite NZplus_succ_l. now rewrite <- NZsucc_le_mono. -Qed. - -Theorem NZplus_le_mono_r : forall n m p, n <= m <-> n + p <= m + p. -Proof. -intros n m p. -rewrite (NZplus_comm n p); rewrite (NZplus_comm m p); apply NZplus_le_mono_l. -Qed. - -Theorem NZplus_le_mono : forall n m p q, n <= m -> p <= q -> n + p <= m + q. -Proof. -intros n m p q H1 H2. -apply NZle_trans with (m + p); -[now apply -> NZplus_le_mono_r | now apply -> NZplus_le_mono_l]. -Qed. - -Theorem NZplus_lt_le_mono : forall n m p q, n < m -> p <= q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZlt_le_trans with (m + p); -[now apply -> NZplus_lt_mono_r | now apply -> NZplus_le_mono_l]. -Qed. - -Theorem NZplus_le_lt_mono : forall n m p q, n <= m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply NZle_lt_trans with (m + p); -[now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l]. -Qed. - -End NZPlusOrderPropFunct. - diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index 6f702067da..2f3cf678b9 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -61,6 +61,37 @@ apply NZle_lt_trans with (m + p); [now apply -> NZplus_le_mono_r | now apply -> NZplus_lt_mono_l]. Qed. +Theorem NZplus_pos_pos : forall n m : NZ, 0 < n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_mono. +Qed. + +Theorem NZplus_pos_nonneg : forall n m : NZ, 0 < n -> 0 <= m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_lt_le_mono. +Qed. + +Theorem NZplus_nonneg_pos : forall n m : NZ, 0 <= n -> 0 < m -> 0 < n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_lt_mono. +Qed. + +Theorem NZplus_nonneg_nonneg : forall n m : NZ, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof. +intros n m H1 H2. rewrite <- (NZplus_0_l 0). now apply NZplus_le_mono. +Qed. + +Theorem NZlt_plus_pos_l : forall n m : NZ, 0 < n -> m < n + m. +Proof. +intros n m H. apply -> (NZplus_lt_mono_r 0 n m) in H. +now rewrite NZplus_0_l in H. +Qed. + +Theorem NZlt_plus_pos_r : forall n m : NZ, 0 < n -> m < m + n. +Proof. +intros; rewrite NZplus_comm; now apply NZlt_plus_pos_l. +Qed. + Theorem NZle_lt_plus_lt : forall n m p q : NZ, n <= m -> p + m < q + n -> p < q. Proof. intros n m p q H1 H2. destruct (NZle_gt_cases q p); [| assumption]. @@ -75,7 +106,7 @@ pose proof (NZplus_le_lt_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. false_hyp H2 H3. Qed. -Theorem NZle_le_plus_lt : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. +Theorem NZle_le_plus_le : forall n m p q : NZ, n <= m -> p + m <= q + n -> p <= q. Proof. intros n m p q H1 H2. destruct (NZle_gt_cases p q); [assumption |]. pose proof (NZplus_lt_le_mono q p n m H H1) as H3. apply <- NZnle_gt in H3. @@ -370,4 +401,14 @@ elimtype False; now apply (NZlt_asymm (n * m) 0). now apply NZtimes_neg_pos. now apply NZtimes_pos_neg. Qed. +Theorem NZtimes_2_mono_l : forall n m : NZ, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof. +intros n m H. apply -> NZlt_le_succ in H. +apply -> (NZtimes_le_mono_pos_l (S n) m (1 + 1)) in H. +repeat rewrite NZtimes_plus_distr_r in *; repeat rewrite NZtimes_1_l in *. +repeat rewrite NZplus_succ_r in *. repeat rewrite NZplus_succ_l in *. rewrite NZplus_0_l. +now apply <- NZlt_le_succ. +apply NZplus_pos_pos; now apply NZlt_succ_r. +Qed. + End NZTimesOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index f62b5ecb2a..7c2610ccc6 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -25,6 +25,9 @@ Proof NZlt_le_incl. Theorem lt_neq : forall n m : N, n < m -> n ~= m. Proof NZlt_neq. +Theorem lt_le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m. +Proof NZlt_le_neq. + Theorem le_refl : forall n : N, n <= n. Proof NZle_refl. diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v deleted file mode 100644 index c4640858e0..0000000000 --- a/theories/Numbers/Natural/Abstract/NPlusOrder.v +++ /dev/null @@ -1,87 +0,0 @@ -Require Export NPlus. -Require Export NOrder. -Require Import NZPlusOrder. - -Module NPlusOrderPropFunct - (Import NPlusMod : NPlusSig) - (Import NOrderMod : NOrderSig with Module NAxiomsMod := NPlusMod.NAxiomsMod). -Module Export NPlusPropMod := NPlusPropFunct NPlusMod. -Module Export NOrderPropMod := NOrderPropFunct NOrderMod. -Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZPlusMod NZOrderMod. -Open Local Scope NatScope. - -(* Print All locks up here !!! *) -Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. -Proof. -intros n m p; induct p. -now rewrite plus_0_r. -intros x IH H. -rewrite plus_succ_r. apply lt_closed_succ. apply IH; apply H. -Qed. - -Theorem plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. -Proof. -intros n m p H; induct p. -do 2 rewrite plus_0_l; assumption. -intros x IH. do 2 rewrite plus_succ_l. now apply <- lt_resp_succ. -Qed. - -Theorem plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. -Proof. -intros n m p H; rewrite plus_comm. -set (k := p + n); rewrite plus_comm; unfold k; clear k. -now apply plus_lt_compat_l. -Qed. - -Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. -Proof. -intros n m p q H1 H2. -apply lt_trans with (m := m + p); -[now apply plus_lt_compat_r | now apply plus_lt_compat_l]. -Qed. - -Theorem plus_lt_cancel_l : forall p n m, p + n < p + m <-> n < m. -Proof. -intros p n m; induct p. -now do 2 rewrite plus_0_l. -intros p IH. -do 2 rewrite plus_succ_l. now rewrite lt_resp_succ. -Qed. - -Theorem plus_lt_cancel_r : forall p n m, n + p < m + p <-> n < m. -Proof. -intros p n m; -setoid_replace (n + p) with (p + n) by apply plus_comm; -setoid_replace (m + p) with (p + m) by apply plus_comm; -apply plus_lt_cancel_l. -Qed. - -(* The following property is similar to plus_repl_pair in NPlus.v -and is used to prove the correctness of the definition of order -on integers constructed from pairs of natural numbers *) - -Theorem plus_lt_repl_pair : forall n m n' m' u v, - n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. -Proof. -intros n m n' m' u v H1 H2. -apply <- (plus_lt_cancel_r (n + m')) in H1. -set (k := n + m') in H1 at 2; rewrite H2 in H1; unfold k in H1; clear k. -rewrite <- plus_assoc in H1. -setoid_replace (m + v + (n + m')) with (n + m' + (m + v)) in H1 by apply plus_comm. -rewrite <- plus_assoc in H1. apply -> plus_lt_cancel_l in H1. -rewrite plus_assoc in H1. setoid_replace (m + v) with (v + m) in H1 by apply plus_comm. -rewrite plus_assoc in H1. apply -> plus_lt_cancel_r in H1. -now rewrite plus_comm in H1. -Qed. - -Theorem plus_gt_succ : - forall n m p, S p < n + m -> (exists n', n == S n') \/ (exists m', m == S m'). -Proof. -intros n m p H. -apply <- lt_le_succ in H. -apply lt_exists_pred in H. destruct H as [q H]. -now apply plus_eq_succ in H. -Qed. - -End NPlusOrderProperties. - diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index 2dbfd8f977..dc1b977aa4 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -28,22 +28,31 @@ Proof NZplus_lt_le_mono. Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. Proof NZplus_le_lt_mono. +Theorem plus_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m. +Proof NZplus_pos_pos. + +Theorem lt_plus_pos_l : forall n m : N, 0 < n -> m < n + m. +Proof NZlt_plus_pos_l. + +Theorem lt_plus_pos_r : forall n m : N, 0 < n -> m < m + n. +Proof NZlt_plus_pos_r. + Theorem le_lt_plus_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. Proof NZle_lt_plus_lt. Theorem lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. Proof NZlt_le_plus_lt. -Theorem le_le_plus_lt : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. -Proof NZle_le_plus_lt. +Theorem le_le_plus_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_plus_le. Theorem plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. Proof NZplus_lt_cases. -Theorem plus_le_cases : forall n m p q : NZ, n + m <= p + q -> n <= p \/ m <= q. +Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. Proof NZplus_le_cases. -Theorem plus_pos_cases : forall n m : NZ, 0 < n + m -> 0 < n \/ 0 < m. +Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. Proof NZplus_pos_cases. (** Theorems true for natural numbers *) @@ -55,17 +64,25 @@ rewrite plus_0_r; le_equal. intros m IH. rewrite plus_succ_r; now apply le_le_succ. Qed. -Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m. +Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p. Proof. -intros n m; cases m. -intro H; elimtype False; now apply H. -intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r. +intros n m p H; rewrite <- (plus_0_r n). +apply plus_lt_le_mono; [assumption | apply le_0_l]. Qed. -Theorem lt_lt_plus : forall n m p : N, n < m -> n < m + p. +Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m. Proof. -intros n m p H; rewrite <- (plus_0_r n). -apply plus_lt_le_mono; [assumption | apply le_0_l]. +intros n m p; rewrite plus_comm; apply lt_lt_plus_r. +Qed. + +Theorem plus_pos_l : forall n m : N, 0 < n -> 0 < n + m. +Proof. +intros; apply NZplus_pos_nonneg. assumption. apply le_0_l. +Qed. + +Theorem plus_pos_r : forall n m : N, 0 < m -> 0 < n + m. +Proof. +intros; apply NZplus_nonneg_pos. apply le_0_l. assumption. Qed. (* The following property is similar to plus_repl_pair in NPlus.v @@ -123,7 +140,7 @@ Proof. intros; apply NZtimes_le_mono; try assumption; apply le_0_l. Qed. -Theorem times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. +Theorem Ztimes_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. Proof NZtimes_pos_pos. Theorem times_eq_0 : forall n m : N, n * m == 0 -> n == 0 \/ m == 0. @@ -132,11 +149,14 @@ Proof NZtimes_eq_0. Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof NZtimes_neq_0. +Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Proof NZtimes_2_mono_l. + Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. Proof. intros n m; split; [intro H | intros [H1 H2]]. apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. -now apply times_pos_pos. +now apply NZtimes_pos_pos. Qed. End NTimesOrderPropFunct. |