Library Interval.Real.Xreal

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq:
Copyright (C) 2007-2016, Inria
This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL:
As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import Reals Bool.
From Flocq Require Import Raux.
From mathcomp.ssreflect Require Import ssreflect.

Require Import Stdlib.

Definition is_zero x := Req_bool x 0.
Definition is_positive x := Rlt_bool 0 x.
Definition is_negative x := Rlt_bool x 0.

Lemma is_zero_spec :
   x, Req_bool_prop x 0 (is_zero x).

Lemma is_zero_0 :
  is_zero 0 = true.

Lemma is_zero_true :
   x, x = 0%R is_zero x = true.

Lemma is_zero_false :
   x, x 0%R is_zero x = false.

Lemma is_positive_spec :
   x, Rlt_bool_prop 0 x (is_positive x).

Lemma is_positive_true :
   x, (0 < x)%R is_positive x = true.

Lemma is_positive_false :
   x, (x 0)%R is_positive x = false.

Lemma is_negative_spec :
   x, Rlt_bool_prop x 0 (is_negative x).

Lemma is_negative_true :
   x, (x < 0)%R is_negative x = true.

Lemma is_negative_false :
   x, (0 x)%R is_negative x = false.

Inductive ExtendedR : Set :=
  | Xnan : ExtendedR
  | Xreal : R ExtendedR.

Definition proj_val x :=
  match x with Xreal yy | XnanR0 end.

Definition proj_fun v f x :=
  match f (Xreal x) with Xreal yy | Xnanv end.

Definition notXnan (xR : ExtendedR) : Prop :=
  match xR with
    | Xnanfalse
    | Xreal _true end = true.

Inductive Xcomparison : Set :=
  Xeq | Xlt | Xgt | Xund.

Definition Xcmp x y :=
  match x, y with
  | Xreal u, Xreal v
    match Rcompare u v with
    | LtXlt
    | EqXeq
    | GtXgt
  | _, _Xund

Definition extension f fx := x,
  match fx x, x with
  | Xnan, _True
  | Xreal v, Xreal uf u = v
  | _, _False

Definition Xbind f x :=
  match x with
  | Xreal xf x
  | XnanXnan

Definition Xbind2 f x y :=
  match x, y with
  | Xreal x, Xreal yf x y
  | _, _Xnan

Notation Xlift f := (Xbind (fun xXreal (f x))).
Notation Xlift2 f := (Xbind2 (fun x yXreal (f x y))).

Lemma Xlift2_nan_r :
   f x, Xlift2 f x Xnan = Xnan.

Notation Xneg := (Xlift Ropp).

Lemma Xneg_involutive :
   x, Xneg (Xneg x) = x.

Definition Xinv' x := if is_zero x then Xnan else Xreal (/ x).
Definition Xsqrt' x := Xreal (sqrt x).
Definition Xsqrt_nan' x := if is_negative x then Xnan else Xreal (sqrt x).
Definition Xdiv' x y := if is_zero y then Xnan else Xreal (x / y).

Notation Xinv := (Xbind Xinv').
Notation Xsqrt := (Xbind Xsqrt').
Notation Xsqrt_nan := (Xbind Xsqrt_nan').
Notation Xabs := (Xlift Rabs).
Notation Xadd := (Xlift2 Rplus).
Notation Xsub := (Xlift2 Rminus).
Notation Xmul := (Xlift2 Rmult).
Notation Xdiv := (Xbind2 Xdiv').
Notation Xmin := (Xlift2 Rmin).
Notation Xmax := (Xlift2 Rmax).

Definition Xscale beta x e := Xmul x (Xreal (bpow beta e)).

Delimit Scope XR_scope with XR.

Notation "x + y" := (Xadd x y) : XR_scope.
Notation "x - y" := (Xsub x y) : XR_scope.
Notation " - y" := (Xneg y) : XR_scope.
Notation "x * y" := (Xmul x y) : XR_scope.
Notation "x / y" := (Xdiv x y) : XR_scope.

Lemma Xsub_split :
   x y, Xsub x y = Xadd x (Xneg y).

Lemma Xdiv_split :
   x y, Xdiv x y = Xmul x (Xinv y).

Definition Xtan' x := if is_zero (cos x) then Xnan else Xreal (tan x).
Definition Xln' x := if is_positive x then Xreal (ln x) else Xnan.
Definition Xpower_int' x n :=
  match n with
  | 0%ZXreal 1%R
  | Zpos pXreal (pow x (nat_of_P p))
  | Zneg pif is_zero x then Xnan else Xreal (Rinv (pow x (nat_of_P p)))

Notation Xsqr := (Xlift Rsqr).
Notation Xcos := (Xlift cos).
Notation Xsin := (Xlift sin).
Notation Xtan := (Xbind Xtan').
Notation Xatan := (Xlift atan).
Notation Xexp := (Xlift exp).
Notation Xln := (Xbind Xln').
Definition Xpower_int x n := Xbind (fun xXpower_int' x n) x.

Lemma Xpower_int_correct :
   n, extension (fun xpowerRZ x n) (fun xXpower_int x n).

Lemma Xadd_comm :
   x y,
  Xadd x y = Xadd y x.

Lemma Xadd_0_l :
  Xadd (Xreal 0) x = x.

Lemma Xadd_0_r :
  Xadd x (Xreal 0) = x.

Lemma Xmul_comm :
   x y,
  Xmul x y = Xmul y x.

Lemma Xmul_assoc :
   x y z,
  Xmul (Xmul x y) z = Xmul x (Xmul y z).

Lemma Xmul_1_l :
  Xmul (Xreal 1) x = x.

Lemma Xmul_1_r :
  Xmul x (Xreal 1) = x.

Lemma Xmul_Xadd_distr_r :
   x y z,
  Xmul (Xadd x y) z = Xadd (Xmul x z) (Xmul y z).

Lemma Xmul_Xneg_distr_l :
   x y,
  Xmul (Xneg x) y = Xneg (Xmul x y).

Lemma Xmul_Xneg_distr_r :
   x y,
  Xmul x (Xneg y) = Xneg (Xmul x y).

Lemma Xinv_Xmul_distr :
   x y,
  Xinv (Xmul x y) = Xmul (Xinv x) (Xinv y).

Definition Xmask x y :=
  match y with
  | Xreal _x
  | XnanXnan

Lemma Xmul_Xinv :
  Xmul x (Xinv x) = Xmask (Xreal 1) (Xinv x).

Lemma Xdiv_0_r :
  Xdiv x (Xreal 0) = Xnan.