Library Coq.micromega.OrderedRing
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
}.
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 (@Equivalence_Reflexive _ _ (SORsetoid sor))
symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
as sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Add Morphism ropp with signature req ==> req as ropp_morph.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Add Ring SOR : (SORrt sor).
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
Theorem Rneq_symm : forall n m : R, n ~= m -> m ~= n.
Theorem Rplus_0_l : forall n : R, 0 + n == n.
Theorem Rplus_0_r : forall n : R, n + 0 == n.
Theorem Rtimes_0_r : forall n : R, n * 0 == 0.
Theorem Rplus_comm : forall n m : R, n + m == m + n.
Theorem Rtimes_0_l : forall n : R, 0 * n == 0.
Theorem Rtimes_comm : forall n m : R, n * m == m * n.
Theorem Rminus_eq_0 : forall n m : R, n - m == 0 <-> n == m.
Theorem Rplus_cancel_l : forall n m p : R, p + n == p + m <-> n == m.
Theorem Rle_refl : forall n : R, n <= n.
Theorem Rle_antisymm : forall n m : R, n <= m -> m <= n -> n == m.
Theorem Rle_trans : forall n m p : R, n <= m -> m <= p -> n <= p.
Theorem Rlt_trichotomy : forall n m : R, n < m \/ n == m \/ m < n.
Theorem Rlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m.
Theorem Rneq_0_1 : 0 ~= 1.
Theorem Req_em : forall n m : R, n == m \/ n ~= m.
Theorem Req_dne : forall n m : R, ~ ~ n == m <-> n == m.
Theorem Rle_lt_eq : forall n m : R, n <= m <-> n < m \/ n == m.
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.
Theorem Rle_lt_trans : forall n m p : R, n <= m -> m < p -> n < p.
Theorem Rlt_le_trans : forall n m p : R, n < m -> m <= p -> n < p.
Theorem Rle_gt_cases : forall n m : R, n <= m \/ m < n.
Theorem Rlt_neq : forall n m : R, n < m -> n ~= m.
Theorem Rle_ngt : forall n m : R, n <= m <-> ~ m < n.
Theorem Rlt_nge : forall n m : R, n < m <-> ~ m <= n.
Theorem Rplus_le_mono_l : forall n m p : R, n <= m <-> p + n <= p + m.
Theorem Rplus_le_mono_r : forall n m p : R, n <= m <-> n + p <= m + p.
Theorem Rplus_lt_mono_l : forall n m p : R, n < m <-> p + n < p + m.
Theorem Rplus_lt_mono_r : forall n m p : R, n < m <-> n + p < m + p.
Theorem Rplus_lt_mono : forall n m p q : R, n < m -> p < q -> n + p < m + q.
Theorem Rplus_le_mono : forall n m p q : R, n <= m -> p <= q -> n + p <= m + q.
Theorem Rplus_lt_le_mono : forall n m p q : R, n < m -> p <= q -> n + p < m + q.
Theorem Rplus_le_lt_mono : forall n m p q : R, n <= m -> p < q -> n + p < m + q.
Theorem Rplus_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n + m.
Theorem Rplus_pos_nonneg : forall n m : R, 0 < n -> 0 <= m -> 0 < n + m.
Theorem Rplus_nonneg_pos : forall n m : R, 0 <= n -> 0 < m -> 0 < n + m.
Theorem Rplus_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n + m.
Theorem Rle_le_minus : forall n m : R, n <= m <-> 0 <= m - n.
Theorem Rlt_lt_minus : forall n m : R, n < m <-> 0 < m - n.
Theorem Ropp_lt_mono : forall n m : R, n < m <-> - m < - n.
Theorem Ropp_pos_neg : forall n : R, 0 < - n <-> n < 0.
Theorem Rtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m.
Theorem Rtimes_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n * m.
Theorem Rtimes_pos_neg : forall n m : R, 0 < n -> m < 0 -> n * m < 0.
Theorem Rtimes_neg_neg : forall n m : R, n < 0 -> m < 0 -> 0 < n * m.
Theorem Rtimes_square_nonneg : forall n : R, 0 <= n * n.
Theorem Rtimes_neq_0 : forall n m : R, n ~= 0 /\ m ~= 0 -> n * m ~= 0.
Theorem Ropp_neg_pos : forall n : R, - n < 0 <-> 0 < n.
Theorem Rlt_0_1 : 0 < 1.
Theorem Rlt_succ_r : forall n : R, n < 1 + n.
Theorem Rlt_lt_succ : forall n m : R, n < m -> n < 1 + m.
End STRICT_ORDERED_RING.