# orders.semirings

Require Import
Relation_Definitions Ring
abstract_algebra interfaces.orders theory.rings.
Require Export
orders.orders orders.maps.

Section semiring_order.
Context `{SemiRing R} `{!SemiRingOrder Rle}.
Add Ring R : (stdlib_semiring_theory R).

Global Instance: (z : R), OrderEmbedding (+z).

Global Instance: z, LeftCancellation (+) z.

Global Instance: z, RightCancellation (+) z.

Lemma nonneg_plus_le_compat_r x z : 0 z x x + z.

Lemma nonneg_plus_le_compat_l x z : 0 z x z + x.

Lemma plus_le_compat x₁ y₁ x₂ y₂ : x₁ y₁ x₂ y₂ x₁ + x₂ y₁ + y₂.

Lemma plus_le_compat_r x y z : 0 z x y x y + z.

Lemma plus_le_compat_l x y z : 0 z x y x z + y.

Lemma nonpos_plus_compat x y : x 0 y 0 x + y 0.

Instance nonneg_plus_compat (x y : R) : PropHolds (0 x) PropHolds (0 y) PropHolds (0 x + y).

Lemma decompose_le {x y} : x y z, 0 z y = x + z.

Lemma compose_le x y z : 0 z y = x + z x y.

Global Instance: (z : R), PropHolds (0 z) OrderPreserving (z *.).

Global Instance: (z : R), PropHolds (0 z) OrderPreserving (.* z).

Lemma mult_le_compat x₁ y₁ x₂ y₂ :
0 x₁ 0 x₂ x₁ y₁ x₂ y₂ x₁ * x₂ y₁ * y₂.

Lemma ge_1_mult_le_compat_r x y z : 1 z 0 y x y x y * z.

Lemma ge_1_mult_le_compat_l x y z : 1 z 0 y x y x z * y.

Lemma flip_nonpos_mult_l x y z : z 0 x y z * y z * x.

Lemma flip_nonpos_mult_r x y z : z 0 x y y * z x * z.

Lemma nonpos_mult x y : x 0 y 0 0 x * y.

Lemma nonpos_nonneg_mult x y : x 0 0 y x * y 0.

Lemma nonneg_nonpos_mult x y : 0 x y 0 x * y 0.
End semiring_order.

Hint Extern 7 (PropHolds (0 _ + _)) => eapply @nonneg_plus_compat : typeclass_instances.

Section strict_semiring_order.
Context `{SemiRing R} `{Apart R} `{!StrictSemiRingOrder Rlt}.
Add Ring Rs : (stdlib_semiring_theory R).

Global Instance: (z : R), StrictOrderEmbedding (+z).

Lemma pos_plus_lt_compat_r x z : 0 < z x < x + z.

Lemma pos_plus_lt_compat_l x z : 0 < z x < z + x.

Lemma plus_lt_compat x₁ y₁ x₂ y₂ : x₁ < y₁ x₂ < y₂ x₁ + x₂ < y₁ + y₂.

Lemma plus_lt_compat_r x y z : 0 < z x < y x < y + z.

Lemma plus_lt_compat_l x y z : 0 < z x < y x < z + y.

Lemma neg_plus_compat x y : x < 0 y < 0 x + y < 0.

Instance pos_plus_compat (x y : R) : PropHolds (0 < x) PropHolds (0 < y) PropHolds (0 < x + y).

Lemma compose_lt x y z : 0 < z y = x + z x < y.

Lemma decompose_lt {x y} : x < y z, 0 < z y = x + z.

Global Instance: (z : R), PropHolds (0 < z) StrictlyOrderPreserving (z *.).

Global Instance: (z : R), PropHolds (0 < z) StrictlyOrderPreserving (.* z).

Lemma mult_lt_compat x₁ y₁ x₂ y₂ :
0 < x₁ 0 < x₂ x₁ < y₁ x₂ < y₂ x₁ * x₂ < y₁ * y₂.

Lemma gt_1_mult_lt_compat_r x y z : 1 < z 0 < y x < y x < y * z.

Lemma gt_1_mult_lt_compat_l x y z : 1 < z 0 < y x < y x < z * y.

Lemma flip_neg_mult_l x y z : z < 0 x < y z * y < z * x.

Lemma flip_neg_mult_r x y z : z < 0 x < y y * z < x * z.

Lemma neg_mult x y : x < 0 y < 0 0 < x * y.

Lemma neg_pos_mult x y : x < 0 0 < y x * y < 0.

Lemma pos_neg_mult x y : 0 < x y < 0 x * y < 0.
End strict_semiring_order.

Hint Extern 7 (PropHolds (0 < _ + _)) => eapply @pos_plus_compat : typeclass_instances.

Section pseudo_semiring_order.
Context `{SemiRing R} `{Apart R} `{!PseudoSemiRingOrder Rlt}.
Add Ring Rp : (stdlib_semiring_theory R).

Instance: StrongSetoid R := pseudo_order_setoid.

Global Instance: StrictSemiRingOrder Rlt.

Global Instance: StrongSetoid_BinaryMorphism (+).

Global Instance: z, StrongLeftCancellation (+) z.

Global Instance: z, StrongRightCancellation (+) z.

Lemma neg_mult_decompose x y : x * y < 0 (x < 0 0 < y) (0 < x y < 0).

Lemma pos_mult_decompose x y : 0 < x * y (0 < x 0 < y) (x < 0 y < 0).

Global Instance: (z : R), PropHolds (0 < z) StrictlyOrderPreservingBack (z *.).

Global Instance: (z : R), PropHolds (0 < z) StrictlyOrderPreservingBack (.* z).

Global Instance: z, PropHolds (z 0) StrongLeftCancellation (.*.) z.

Global Instance: z, PropHolds (z 0) StrongRightCancellation (.*.) z.

Global Instance: z, PropHolds (z 0) LeftCancellation (.*.) z.

Global Instance: z, PropHolds (z 0) RightCancellation (.*.) z.

Lemma square_pos x : x 0 0 < x * x.

Context `{PropHolds (1 0)}.

Instance lt_0_1 : PropHolds (0 < 1).

Instance lt_0_2 : PropHolds (0 < 2).

Instance lt_0_3 : PropHolds (0 < 3).

Instance lt_0_4 : PropHolds (0 < 4).

Lemma lt_1_2 : 1 < 2.

Lemma lt_1_3 : 1 < 3.

Lemma lt_1_4 : 1 < 4.

Lemma lt_2_3 : 2 < 3.

Lemma lt_2_4 : 2 < 4.

Lemma lt_3_4 : 3 < 4.

Instance apart_0_2 : PropHolds (2 0).
End pseudo_semiring_order.

Hint Extern 7 (PropHolds (0 < 1)) => eapply @lt_0_1 : typeclass_instances.
Hint Extern 7 (PropHolds (0 < 2)) => eapply @lt_0_2 : typeclass_instances.
Hint Extern 7 (PropHolds (0 < 3)) => eapply @lt_0_3 : typeclass_instances.
Hint Extern 7 (PropHolds (0 < 4)) => eapply @lt_0_4 : typeclass_instances.
Hint Extern 7 (PropHolds (2 0)) => eapply @apart_0_2 : typeclass_instances.

Section full_pseudo_semiring_order.
Context `{SemiRing R} `{Apart R} `{!FullPseudoSemiRingOrder Rle Rlt}.

Add Ring Rf : (stdlib_semiring_theory R).

Global Instance: FullPseudoOrder Rle Rlt.

Global Instance: SemiRingOrder Rle.

Global Instance: (z : R), PropHolds (0 < z) OrderPreservingBack (z *.).

Global Instance: (z : R), PropHolds (0 < z) OrderPreservingBack (.* z).

Lemma plus_lt_le_compat x₁ y₁ x₂ y₂ : x₁ < y₁ x₂ y₂ x₁ + x₂ < y₁ + y₂.

Lemma plus_le_lt_compat x₁ y₁ x₂ y₂ : x₁ y₁ x₂ < y₂ x₁ + x₂ < y₁ + y₂.

Lemma nonneg_plus_lt_compat_r x y z : 0 z x < y x < y + z.

Lemma nonneg_plus_lt_compat_l x y z : 0 z x < y x < z + y.

Lemma pos_plus_le_lt_compat_r x y z : 0 < z x y x < y + z.

Lemma pos_plus_le_lt_compat_l x y z : 0 < z x y x < z + y.

Lemma square_nonneg x : 0 x * x.

Instance le_0_1 : PropHolds (0 1).

Instance le_0_2 : PropHolds (0 2).

Instance le_0_3 : PropHolds (0 3).

Instance le_0_4 : PropHolds (0 4).

Lemma le_1_2 : 1 2.

Lemma le_1_3 : 1 3.

Lemma le_1_4 : 1 4.

Lemma le_2_3 : 2 3.

Lemma le_2_4 : 2 4.

Lemma le_3_4 : 3 4.

Lemma ge_1_mult_compat x y : 1 x 1 y 1 x * y.

Lemma gt_1_ge_1_mult_compat x y : 1 < x 1 y 1 < x * y.

Lemma ge_1_gt_1_mult_compat x y : 1 x 1 < y 1 < x * y.

Context `{PropHolds (1 0)}.

Lemma not_le_1_0 : ¬1 0.

Lemma not_le_2_0 : ¬2 0.
End full_pseudo_semiring_order.

Hint Extern 7 (PropHolds (0 1)) => eapply @le_0_1 : typeclass_instances.
Hint Extern 7 (PropHolds (0 2)) => eapply @le_0_2 : typeclass_instances.
Hint Extern 7 (PropHolds (0 3)) => eapply @le_0_3 : typeclass_instances.
Hint Extern 7 (PropHolds (0 4)) => eapply @le_0_4 : typeclass_instances.

Section dec_semiring_order.
Context `{SemiRing A} `{Apart A} `{!TrivialApart A} `{!SemiRingOrder Rle}
`{!NoZeroDivisors A} `{!TotalRelation (≤)} `{ x y, Decision (x = y)}.

Context `{Rlt : Lt A} (lt_correct : x y, x < y x y x y).

Instance: FullPseudoOrder Rle Rlt := dec_full_pseudo_order lt_correct.
Instance: StrongSetoid A := pseudo_order_setoid.

Instance dec_pseudo_srorder: PseudoSemiRingOrder (<).

Instance dec_full_pseudo_srorder: FullPseudoSemiRingOrder (≤) (<).
End dec_semiring_order.

Section another_semiring.
Context `{SemiRing R1} `{SemiRing R2} `{!SemiRingOrder (A:=R1) R1le} `{R2le : Le R2}.

Lemma projected_srorder (f : R2 R1) `{!SemiRing_Morphism f} `{!Injective f} `{!OrderEmbedding f} :
( x y : R2, x y z, y = x + z) SemiRingOrder R2le.

Context `{!SemiRingOrder (A:=R2) R2le} `{!SemiRing_Morphism (f : R1 R2)}.

Lemma preserving_preserves_nonneg : ( x, 0 x 0 f x) OrderPreserving f.

Instance preserves_nonneg `{!OrderPreserving f} x : PropHolds (0 x) PropHolds (0 f x).

Lemma preserves_nonpos `{!OrderPreserving f} x : x 0 f x 0.

Lemma preserves_ge_1 `{!OrderPreserving f} x : 1 x 1 f x.

Lemma preserves_le_1 `{!OrderPreserving f} x : x 1 f x 1.
End another_semiring.

Section another_semiring_strict.
Context `{SemiRing R1} `{SemiRing R2} `{!StrictSemiRingOrder (A:=R1) R1le} `{!StrictSemiRingOrder (A:=R2) R2le}
`{!SemiRing_Morphism (f : R1 R2)}.

Instance preserves_pos `{!StrictlyOrderPreserving f} x : PropHolds (0 < x) PropHolds (0 < f x).

Lemma preserves_neg `{!StrictlyOrderPreserving f} x : x < 0 f x < 0.

Lemma preserves_gt_1 `{!StrictlyOrderPreserving f} x : 1 < x 1 < f x.

Lemma preserves_lt_1 `{!StrictlyOrderPreserving f} x : x < 1 f x < 1.
End another_semiring_strict.

Hint Extern 15 (PropHolds (_ _ _)) => eapply @preserves_nonneg : typeclass_instances.
Hint Extern 15 (PropHolds (_ < _ _)) => eapply @preserves_pos : typeclass_instances.