theory.cut_minus

Require
orders.semirings.
Require Import
Ring
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}.

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

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.

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.