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.