summaryrefslogtreecommitdiff
path: root/contrib/micromega/OrderedRing.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/micromega/OrderedRing.v')
-rw-r--r--contrib/micromega/OrderedRing.v458
1 files changed, 0 insertions, 458 deletions
diff --git a/contrib/micromega/OrderedRing.v b/contrib/micromega/OrderedRing.v
deleted file mode 100644
index 149b7731..00000000
--- a/contrib/micromega/OrderedRing.v
+++ /dev/null
@@ -1,458 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-(* Evgeny Makarov, INRIA, 2007 *)
-(************************************************************************)
-
-Require Import Setoid.
-Require Import Ring.
-
-(** Generic properties of ordered rings on a setoid equality *)
-
-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 : Type := 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).(@Equivalence_Reflexive _ _ )
- symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _ )
- transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _ )
-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.
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 15:19:14 +0000