Library Coq.micromega.OrderedRing


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
}.


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.