theory.cut_minus

Require
  orders.semirings.
Require Import
  Ring
  abstract_algebra interfaces.additional_operations
  interfaces.orders orders.minmax.

Section cut_minus_properties.
  Context `{SemiRing R} `{Apart R} `{!FullPseudoSemiRingOrder Rle Rlt} `{!TrivialApart R}
    `{ x y, Decision (x = y)} `{!CutMinusSpec R cm}.

  Add Ring SR: (rings.stdlib_semiring_theory R).
  Hint Resolve (@orders.le_flip R _ _).

  Global Instance cut_minus_proper: Proper ((=) ==> (=) ==> (=)) cut_minus | 1.

  Hint Resolve cut_minus_0.
  Hint Resolve cut_minus_le.

  Lemma cut_minus_diag x : x x = 0.

  Lemma cut_minus_rightidentity x : 0 x x 0 = x.

  Lemma cut_minus_leftabsorb x : 0 x 0 x = 0.

  Lemma cut_minus_rightabsorb x : x 0 x 0 = 0.

  Lemma cut_minus_nonneg x y : 0 x y.

  Lemma cut_minus_le_trans x y z : y x z y (x y) + (y z) = x z.
  Hint Resolve cut_minus_le_trans.

  Lemma cut_minus_plus_distr x1 x2 y1 y2 :
     y1 x1 y2 x2 (x1 y1) + (x2 y2) = (x1 + x2) (y1 + y2).

  Lemma cut_minus_mult_distr_l (x y z : R) : 0 x x * (y z) = x * y x * z.

  Lemma cut_minus_mult_distr_r (x y z : R) : 0 x (y z) * x = y * x z * x.

  Lemma cut_minus_plus_l_rev x y z : y z = (x + y) (x + z).

  Lemma cut_minus_plus_r_rev x y z : y z = (y + x) (z + x).

  Lemma cut_minus_plus_toggle1 x y z : x y z y (y x) + (x z) = (y z) + (z x).

  Lemma cut_minus_plus_toggle2 x y z : y x y z (x z) + (z y) = (z x) + (x y).

  Lemma cut_minus_plus_toggle3 x1 x2 y1 y2 : x1 y1 y2 x2
      (y1 x1) + ((x1 + x2) (y1 + y2)) = (x2 y2) + ((y1 + y2) (x1 + x2)).

  Lemma cut_minus_zero_plus_toggle x : x + (0 x) = x 0.

  Lemma cut_minus_zeros_le x y : x y (y x) + (x 0) + (0 y) = (y 0) + (0 x).

  Section min.
  Context `{ (x y : R), Decision (x y)}.
  Lemma cut_minus_min1 x y z : x min y z = x y + (min x y z).

  Lemma cut_minus_min2 x y z : y z + (min y z x) = y x + (min x y z).

  Lemma cut_minus_min3 x y z : (x + min y z) min (x + y) (x + z) = min (x + y) (x + z) (x + min y z).
  End min.

  Context `{GroupInv R} `{!Ring R}.
  Add Ring R: (rings.stdlib_ring_theory R).

  Lemma cut_minus_ring_minus (x y : R) : y x x y = x - y.

  Lemma cut_minus_opp (x : R) : x 0 0 x = -x.
End cut_minus_properties.

Section cut_minus_default.
  Context `{Ring R} `{!SemiRingOrder o} `{ (x y : R), Decision (x y)}.

  Global Instance default_cut_minus: CutMinus R | 10 := λ x y, if decide_rel (≤) x y then 0 else x - y.

  Add Ring R2: (rings.stdlib_ring_theory R).

  Global Instance: CutMinusSpec R default_cut_minus.
End cut_minus_default.

Typeclasses Opaque default_cut_minus.

Section order_preserving.
  Context `{SemiRing A} `{Apart A} `{!TrivialApart A}
   `{!FullPseudoSemiRingOrder (A:=A) Ale Alt} `{!CutMinusSpec A cmA} `{ (x y : A), Decision (x = y)}
   `{SemiRing B} `{Apart B} `{!TrivialApart B}
   `{!FullPseudoSemiRingOrder (A:=B) Ble Blt} `{!CutMinusSpec B cmB} `{ (x y : B), Decision (x = y)}
     {f : A B} `{!OrderPreserving f} `{!SemiRing_Morphism f}.

  Lemma preserves_cut_minus x y : f (x y) = f x f y.
End order_preserving.