Library Coq.Reals.Cauchy.ConstructiveCauchyAbs

Require Import QArith.
Require Import Qabs.
Require Import Qpower.
Require Import ConstructiveCauchyReals.
Require Import ConstructiveCauchyRealsMult.
Require Import Lia.
Require Import Lqa.
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.

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

Library Coq.Reals.Cauchy.ConstructiveCauchyAbs

Navigation