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.