Library Stdlib.Reals.Cauchy.ConstructiveCauchyAbs

From Stdlib Require Import QArith.
From Stdlib Require Import Qabs.
From Stdlib Require Import Qpower.
From Stdlib Require Import ConstructiveCauchyReals.
From Stdlib Require Import ConstructiveCauchyRealsMult.
From Stdlib Require Import Lia.
From Stdlib Require Import Lqa.
From Stdlib Require Import QExtra.

Local Open Scope CReal_scope.

Local Ltac simplify_Qabs :=
  match goal with |- context [(Qabs ?a)%Q] => ring_simplify a end.

Local Ltac simplify_Qlt :=
  match goal with |- (?l < ?r)%Q => ring_simplify l; ring_simplify r end.

Local Lemma Qopp_mult_mone : forall q : Q,
  (-1 * q == -q)%Q.

Local Lemma Qabs_involutive: forall q : Q,
  (Qabs (Qabs q) == Qabs q)%Q.

The constructive formulation of the absolute value on the real numbers. This is followed by the constructive definitions of minimum and maximum, as min x y := (x + y - |x-y|) / 2.

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

Definition CReal_abs_seq (x : CReal) (n : Z) := Qabs (seq x n).

Definition CReal_abs_scale (x : CReal) := scale x.

Lemma CReal_abs_cauchy: forall (x : CReal),
    QCauchySeq (CReal_abs_seq x).

Lemma CReal_abs_bound : forall (x : CReal),
  QBound (CReal_abs_seq x) (CReal_abs_scale x).

Definition CReal_abs (x : CReal) : CReal :=
{|
  seq := CReal_abs_seq x;
  scale := CReal_abs_scale x;
  cauchy := CReal_abs_cauchy x;
  bound := CReal_abs_bound x
|}.

Lemma CRealLt_RQ_from_single_dist : forall (r : CReal) (q : Q) (n :Z),
    (2^n < q - seq r n)%Q
-> r < inject_Q q.

Lemma CRealLe_0R_to_single_dist : forall (x : CReal) (n : Z),
    0 <= x -> (-(2^n ) <= seq x n)%Q.

Lemma CReal_abs_right : forall x : CReal, 0 <= x -> CReal_abs x == x.

Lemma CReal_le_abs : forall x : CReal, x <= CReal_abs x.

Lemma CReal_abs_pos : forall x : CReal, 0 <= CReal_abs x.

Lemma CReal_abs_opp : forall x : CReal, CReal_abs (-x) == CReal_abs x.

Lemma CReal_abs_left : forall x : CReal, x <= 0 -> CReal_abs x == -x.

Lemma CReal_abs_appart_0 : forall x : CReal,
    0 < CReal_abs x -> x # 0.

Add Parametric Morphism : CReal_abs
    with signature CRealEq ==> CRealEq
      as CReal_abs_morph.

Lemma CReal_abs_le : forall a b:CReal, -b <= a <= b -> CReal_abs a <= b.

Lemma CReal_abs_minus_sym : forall x y : CReal,
    CReal_abs (x - y) == CReal_abs (y - x).

Lemma CReal_abs_lt : forall x y : CReal,
    CReal_abs x < y -> prod (x < y) (-x < y).

Lemma CReal_abs_triang : forall x y : CReal,
    CReal_abs (x + y) <= CReal_abs x + CReal_abs y.

Lemma CReal_abs_triang_inv : forall x y : CReal,
    CReal_abs x - CReal_abs y <= CReal_abs (x - y).

Lemma CReal_abs_triang_inv2 : forall x y : CReal,
    CReal_abs (CReal_abs x - CReal_abs y) <= CReal_abs (x - y).

Lemma CReal_abs_gt : forall x : CReal,
    x < CReal_abs x -> x < 0.

Lemma Rabs_def1 : forall x y : CReal,
    x < y -> -x < y -> CReal_abs x < y.

Lemma CReal_abs_mult : forall x y : CReal,
    CReal_abs (x * y) == CReal_abs x * CReal_abs y.

Lemma CReal_abs_def2 : forall x a:CReal,
    CReal_abs x <= a -> (x <= a ) /\ (- a <= x ).

Definition CReal_min (x y : CReal) : CReal
  := (x + y - CReal_abs (y - x)) * inject_Q (1#2).

Definition CReal_max (x y : CReal) : CReal
  := (x + y + CReal_abs (y - x)) * inject_Q (1#2).

Add Parametric Morphism : CReal_min
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_min_morph.

Add Parametric Morphism : CReal_max
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_max_morph.

Lemma CReal_double : forall x:CReal, 2 * x == x + x.

Lemma CReal_max_lub : forall x y z:CReal,
    x <= z -> y <= z -> CReal_max x y <= z.

Lemma CReal_min_glb : forall x y z:CReal,
    z <= x -> z <= y -> z <= CReal_min x y.

Lemma CReal_max_l : forall x y : CReal, x <= CReal_max x y.

Lemma CReal_max_r : forall x y : CReal, y <= CReal_max x y.

Lemma CReal_min_l : forall x y : CReal, CReal_min x y <= x.

Lemma CReal_min_r : forall x y : CReal, CReal_min x y <= y.

Lemma CReal_min_left : forall x y : CReal,
    x <= y -> CReal_min x y == x.

Lemma CReal_min_right : forall x y : CReal,
    y <= x -> CReal_min x y == y.

Lemma CReal_max_left : forall x y : CReal,
    y <= x -> CReal_max x y == x.

Lemma CReal_max_right : forall x y : CReal,
    x <= y -> CReal_max x y == y.

Lemma CReal_min_lt_r : forall x y : CReal,
    CReal_min x y < y -> CReal_min x y == x.

Lemma posPartAbsMax : forall x : CReal,
    CReal_max 0 x == (x + CReal_abs x ) * (inject_Q (1#2)).

Lemma negPartAbsMin : forall x : CReal,
    CReal_min 0 x == (x - CReal_abs x ) * (inject_Q (1#2)).

Lemma CReal_min_sym : forall (x y : CReal),
    CReal_min x y == CReal_min y x.

Lemma CReal_max_sym : forall (x y : CReal),
    CReal_max x y == CReal_max y x.

Lemma CReal_min_mult :
  forall (p q r:CReal), 0 <= r -> CReal_min (r * p) (r * q) == r * CReal_min p q.

Lemma CReal_min_plus : forall (x y z : CReal),
    x + CReal_min y z == CReal_min (x + y) (x + z).

Lemma CReal_max_plus : forall (x y z : CReal),
    x + CReal_max y z == CReal_max (x + y) (x + z).

Lemma CReal_min_lt : forall x y z : CReal,
    z < x -> z < y -> z < CReal_min x y.

Lemma CReal_max_assoc : forall a b c : CReal,
    CReal_max a (CReal_max b c) == CReal_max (CReal_max a b) c.

Lemma CReal_min_max_mult_neg :
  forall (p q r:CReal), r <= 0 -> CReal_min (r * p) (r * q) == r * CReal_max p q.

Lemma CReal_min_assoc : forall a b c : CReal,
    CReal_min a (CReal_min b c) == CReal_min (CReal_min a b) c.

Lemma CReal_max_lub_lt : forall x y z : CReal,
    x < z -> y < z -> CReal_max x y < z.

Lemma CReal_max_contract : forall x y a : CReal,
    CReal_abs (CReal_max x a - CReal_max y a)
    <= CReal_abs (x - y).

Lemma CReal_min_contract : forall x y a : CReal,
    CReal_abs (CReal_min x a - CReal_min y a)
    <= CReal_abs (x - y).