Library Coq.Reals.Abstract.ConstructiveMinMax

Require Import QArith.
Require Import Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveAbs.
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).