Library Stdlib.Reals.Abstract.ConstructiveMinMax

From Stdlib Require Import QArith.
From Stdlib Require Import Qabs.
From Stdlib Require Import ConstructiveReals.
From Stdlib Require Import ConstructiveAbs.
From Stdlib Require Import ConstructiveRealsMorphisms.

Local Open Scope ConstructiveReals.

Definition CRmin {R : ConstructiveReals} (x y : CRcarrier R) : CRcarrier R
  := (x + y - CRabs _ (y - x)) * CR_of_Q _ (1#2).

Lemma CRmin_lt_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRmin x y < y -> CRmin x y == x.

Add Parametric Morphism {R : ConstructiveReals} : CRmin
    with signature (CReq R) ==> (CReq R) ==> (CReq R)
      as CRmin_morph.

#[global]
Instance CRmin_morphT
  : forall {R : ConstructiveReals},
    CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (@CRmin R).

Lemma CRmin_l : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRmin x y <= x.

Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRmin x y <= y.

Lemma CRnegPartAbsMin : forall {R : ConstructiveReals} (x : CRcarrier R),
    CRmin 0 x == (x - CRabs _ x) * (CR_of_Q _ (1#2)).

Lemma CRmin_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRmin x y == CRmin y x.

Lemma CRmin_mult :
  forall {R : ConstructiveReals} (p q r : CRcarrier R),
    0 <= r -> CRmin (r * p) (r * q) == r * CRmin p q.

Lemma CRmin_plus : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    x + CRmin y z == CRmin (x + y) (x + z).

Lemma CRmin_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x <= y -> CRmin x y == x.

Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
    y <= x -> CRmin x y == y.

Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    z < x -> z < y -> z < CRmin x y.

Lemma CRmin_contract : forall {R : ConstructiveReals} (x y a : CRcarrier R),
    CRabs _ (CRmin x a - CRmin y a) <= CRabs _ (x - y).

Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R),
    z <= x -> z <= y -> z <= CRmin x y.

Lemma CRmin_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R),
    CRmin a (CRmin b c) == CRmin (CRmin a b) c.

Lemma CRlt_min : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    z < CRmin x y -> prod (z < x) (z < y).


Definition CRmax {R : ConstructiveReals} (x y : CRcarrier R) : CRcarrier R
  := (x + y + CRabs _ (y - x)) * CR_of_Q _ (1#2).

Add Parametric Morphism {R : ConstructiveReals} : CRmax
    with signature (CReq R) ==> (CReq R) ==> (CReq R)
      as CRmax_morph.

#[global]
Instance CRmax_morphT
  : forall {R : ConstructiveReals},
    CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (@CRmax R).

Lemma CRmax_lub : forall {R : ConstructiveReals} (x y z:CRcarrier R),
    x <= z -> y <= z -> CRmax x y <= z.

Lemma CRmax_l : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x <= CRmax x y.

Lemma CRmax_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
    y <= CRmax x y.

Lemma CRposPartAbsMax : forall {R : ConstructiveReals} (x : CRcarrier R),
    CRmax 0 x == (x + CRabs _ x) * (CR_of_Q R (1#2)).

Lemma CRmax_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRmax x y == CRmax y x.

Lemma CRmax_plus : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    x + CRmax y z == CRmax (x + y) (x + z).

Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
    y <= x -> CRmax x y == x.

Lemma CRmax_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x <= y -> CRmax x y == y.

Lemma CRmax_contract : forall {R : ConstructiveReals} (x y a : CRcarrier R),
    CRabs _ (CRmax x a - CRmax y a) <= CRabs _ (x - y).

Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    x < z -> y < z -> CRmax x y < z.

Lemma CRmax_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R),
    CRmax a (CRmax b c) == CRmax (CRmax a b) c.

Lemma CRmax_min_mult_neg :
  forall {R : ConstructiveReals} (p q r:CRcarrier R),
    r <= 0 -> CRmax (r * p) (r * q) == r * CRmin p q.

Lemma CRlt_max : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    CRmax x y < z -> prod (x < z) (y < z).

Lemma CRmax_mult :
  forall {R : ConstructiveReals} (p q r:CRcarrier R),
    0 <= r -> CRmax (r * p) (r * q) == r * CRmax p q.

Lemma CRmin_max_mult_neg :
  forall {R : ConstructiveReals} (p q r:CRcarrier R),
    r <= 0 -> CRmin (r * p) (r * q) == r * CRmax p q.

Lemma CRmorph_min : forall {R1 R2 : ConstructiveReals}
                      (f : @ConstructiveRealsMorphism R1 R2)
                      (a b : CRcarrier R1),
    CRmorph f (CRmin a b)
    == CRmin (CRmorph f a) (CRmorph f b).