Library Stdlib.Reals.Abstract.ConstructiveAbs

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

#[local] Open Scope ConstructiveReals.

Properties of constructive absolute value (defined in ConstructiveReals.CRabs). Definition of minimum, maximum and their properties.

WARNING: this file is experimental and likely to change in future releases.

#[global]
Instance CRabs_morph
  : forall {R : ConstructiveReals},
    CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CReq R)) (CRabs R).

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

Lemma CRabs_right : forall {R : ConstructiveReals} (x : CRcarrier R),
    0 <= x -> CRabs R x == x.

Lemma CRabs_opp : forall {R : ConstructiveReals} (x : CRcarrier R),
    CRabs R (- x) == CRabs R x.

Lemma CRabs_minus_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRabs R (x - y) == CRabs R (y - x).

Lemma CRabs_left : forall {R : ConstructiveReals} (x : CRcarrier R),
    x <= 0 -> CRabs R x == - x.

Lemma CRabs_triang : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRabs R (x + y) <= CRabs R x + CRabs R y.

Lemma CRabs_le : forall {R : ConstructiveReals} (a b:CRcarrier R),
    (-b <= a /\ a <= b ) -> CRabs R a <= b.

Lemma CRabs_triang_inv : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRabs R x - CRabs R y <= CRabs R (x - y).

Lemma CRabs_triang_inv2 : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRabs R (CRabs R x - CRabs R y) <= CRabs R (x - y).

Lemma CR_of_Q_abs : forall {R : ConstructiveReals} (q : Q),
    CRabs R (CR_of_Q R q) == CR_of_Q R (Qabs q).

Lemma CRle_abs : forall {R : ConstructiveReals} (x : CRcarrier R),
    x <= CRabs R x.

Lemma CRabs_pos : forall {R : ConstructiveReals} (x : CRcarrier R),
    0 <= CRabs R x.

Lemma CRabs_appart_0 : forall {R : ConstructiveReals} (x : CRcarrier R),
    0 < CRabs R x -> x ≶ 0.

Lemma CRabs_mult : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRabs R (x * y) == CRabs R x * CRabs R y.

Lemma CRabs_lt : forall {R : ConstructiveReals} (x y : CRcarrier R),
    CRabs _ x < y -> prod (x < y) (-x < y).

Lemma CRabs_def1 : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x < y -> -x < y -> CRabs _ x < y.

Lemma CRabs_def2 : forall {R : ConstructiveReals} (x a:CRcarrier R),
    CRabs _ x <= a -> (x <= a ) /\ (- a <= x ).