Library Flocq.Core.Raux

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2009-2018 Sylvie Boldo
Copyright (C) 2009-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Missing definitions/lemmas

Require Import Psatz.
Require Export Reals ZArith.
Require Export Zaux.

Section Rmissing.

About R
Theorem Rle_0_minus :
   x y, (x y)%R (0 y - x)%R.

Theorem Rabs_eq_Rabs :
   x y : R,
  Rabs x = Rabs y x = y x = Ropp y.

Theorem Rabs_minus_le:
   x y : R,
  (0 y)%R (y 2×x)%R
  (Rabs (x-y) x)%R.

Theorem Rplus_eq_reg_r :
   r r1 r2 : R,
  (r1 + r = r2 + r)%R (r1 = r2)%R.

Theorem Rmult_lt_compat :
   r1 r2 r3 r4,
  (0 r1)%R (0 r3)%R (r1 < r2)%R (r3 < r4)%R
  (r1 × r3 < r2 × r4)%R.

Theorem Rmult_minus_distr_r :
   r r1 r2 : R,
  ((r1 - r2) × r = r1 × r - r2 × r)%R.

Lemma Rmult_neq_reg_r :
   r1 r2 r3 : R, (r2 × r1 r3 × r1)%R r2 r3.

Lemma Rmult_neq_compat_r :
   r1 r2 r3 : R,
  (r1 0)%R (r2 r3)%R
  (r2 × r1 r3 × r1)%R.

Theorem Rmult_min_distr_r :
   r r1 r2 : R,
  (0 r)%R
  (Rmin r1 r2 × r)%R = Rmin (r1 × r) (r2 × r).

Theorem Rmult_min_distr_l :
   r r1 r2 : R,
  (0 r)%R
  (r × Rmin r1 r2)%R = Rmin (r × r1) (r × r2).

Lemma Rmin_opp: x y, (Rmin (-x) (-y) = - Rmax x y)%R.

Lemma Rmax_opp: x y, (Rmax (-x) (-y) = - Rmin x y)%R.

Theorem exp_le :
   x y : R,
  (x y)%R (exp x exp y)%R.

Theorem Rinv_lt :
   x y,
  (0 < x)%R (x < y)%R (/y < /x)%R.

Theorem Rinv_le :
   x y,
  (0 < x)%R (x y)%R (/y /x)%R.

Theorem sqrt_ge_0 :
   x : R,
  (0 sqrt x)%R.

Lemma sqrt_neg : x, (x 0)%R (sqrt x = 0)%R.

Theorem Rabs_le :
   x y,
  (-y x y)%R (Rabs x y)%R.

Theorem Rabs_le_inv :
   x y,
  (Rabs x y)%R (-y x y)%R.

Theorem Rabs_ge :
   x y,
  (y -x x y)%R (x Rabs y)%R.

Theorem Rabs_ge_inv :
   x y,
  (x Rabs y)%R (y -x x y)%R.

Theorem Rabs_lt :
   x y,
  (-y < x < y)%R (Rabs x < y)%R.

Theorem Rabs_lt_inv :
   x y,
  (Rabs x < y)%R (-y < x < y)%R.

Theorem Rabs_gt :
   x y,
  (y < -x x < y)%R (x < Rabs y)%R.

Theorem Rabs_gt_inv :
   x y,
  (x < Rabs y)%R (y < -x x < y)%R.

End Rmissing.

Section IZR.

Theorem IZR_le_lt :
   m n p, (m n < p)%Z (IZR m IZR n < IZR p)%R.

Theorem le_lt_IZR :
   m n p, (IZR m IZR n < IZR p)%R (m n < p)%Z.

Theorem neq_IZR :
   m n, (IZR m IZR n)%R (m n)%Z.

End IZR.

Decidable comparison on reals
Section Rcompare.

Definition Rcompare x y :=
  match total_order_T x y with
  | inleft (left _) ⇒ Lt
  | inleft (right _) ⇒ Eq
  | inright _Gt
  end.

Inductive Rcompare_prop (x y : R) : comparison Prop :=
  | Rcompare_Lt_ : (x < y)%R Rcompare_prop x y Lt
  | Rcompare_Eq_ : x = y Rcompare_prop x y Eq
  | Rcompare_Gt_ : (y < x)%R Rcompare_prop x y Gt.

Theorem Rcompare_spec :
   x y, Rcompare_prop x y (Rcompare x y).

Global Opaque Rcompare.

Theorem Rcompare_Lt :
   x y,
  (x < y)%R Rcompare x y = Lt.

Theorem Rcompare_Lt_inv :
   x y,
  Rcompare x y = Lt (x < y)%R.

Theorem Rcompare_not_Lt :
   x y,
  (y x)%R Rcompare x y Lt.

Theorem Rcompare_not_Lt_inv :
   x y,
  Rcompare x y Lt (y x)%R.

Theorem Rcompare_Eq :
   x y,
  x = y Rcompare x y = Eq.

Theorem Rcompare_Eq_inv :
   x y,
  Rcompare x y = Eq x = y.

Theorem Rcompare_Gt :
   x y,
  (y < x)%R Rcompare x y = Gt.

Theorem Rcompare_Gt_inv :
   x y,
  Rcompare x y = Gt (y < x)%R.

Theorem Rcompare_not_Gt :
   x y,
  (x y)%R Rcompare x y Gt.

Theorem Rcompare_not_Gt_inv :
   x y,
  Rcompare x y Gt (x y)%R.

Theorem Rcompare_IZR :
   x y, Rcompare (IZR x) (IZR y) = Zcompare x y.

Theorem Rcompare_sym :
   x y,
  Rcompare x y = CompOpp (Rcompare y x).

Theorem Rcompare_plus_r :
   z x y,
  Rcompare (x + z) (y + z) = Rcompare x y.

Theorem Rcompare_plus_l :
   z x y,
  Rcompare (z + x) (z + y) = Rcompare x y.

Theorem Rcompare_mult_r :
   z x y,
  (0 < z)%R
  Rcompare (x × z) (y × z) = Rcompare x y.

Theorem Rcompare_mult_l :
   z x y,
  (0 < z)%R
  Rcompare (z × x) (z × y) = Rcompare x y.

Theorem Rcompare_middle :
   x d u,
  Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).

Theorem Rcompare_half_l :
   x y, Rcompare (x / 2) y = Rcompare x (2 × y).

Theorem Rcompare_half_r :
   x y, Rcompare x (y / 2) = Rcompare (2 × x) y.

Theorem Rcompare_sqr :
   x y,
  Rcompare (x × x) (y × y) = Rcompare (Rabs x) (Rabs y).

Theorem Rmin_compare :
   x y,
  Rmin x y = match Rcompare x y with Ltx | Eqx | Gty end.

End Rcompare.

Section Rle_bool.

Definition Rle_bool x y :=
  match Rcompare x y with
  | Gtfalse
  | _true
  end.

Inductive Rle_bool_prop (x y : R) : bool Prop :=
  | Rle_bool_true_ : (x y)%R Rle_bool_prop x y true
  | Rle_bool_false_ : (y < x)%R Rle_bool_prop x y false.

Theorem Rle_bool_spec :
   x y, Rle_bool_prop x y (Rle_bool x y).

Theorem Rle_bool_true :
   x y,
  (x y)%R Rle_bool x y = true.

Theorem Rle_bool_false :
   x y,
  (y < x)%R Rle_bool x y = false.

End Rle_bool.

Section Rlt_bool.

Definition Rlt_bool x y :=
  match Rcompare x y with
  | Lttrue
  | _false
  end.

Inductive Rlt_bool_prop (x y : R) : bool Prop :=
  | Rlt_bool_true_ : (x < y)%R Rlt_bool_prop x y true
  | Rlt_bool_false_ : (y x)%R Rlt_bool_prop x y false.

Theorem Rlt_bool_spec :
   x y, Rlt_bool_prop x y (Rlt_bool x y).

Theorem negb_Rlt_bool :
   x y,
  negb (Rle_bool x y) = Rlt_bool y x.

Theorem negb_Rle_bool :
   x y,
  negb (Rlt_bool x y) = Rle_bool y x.

Theorem Rlt_bool_true :
   x y,
  (x < y)%R Rlt_bool x y = true.

Theorem Rlt_bool_false :
   x y,
  (y x)%R Rlt_bool x y = false.

End Rlt_bool.

Section Req_bool.

Definition Req_bool x y :=
  match Rcompare x y with
  | Eqtrue
  | _false
  end.

Inductive Req_bool_prop (x y : R) : bool Prop :=
  | Req_bool_true_ : (x = y)%R Req_bool_prop x y true
  | Req_bool_false_ : (x y)%R Req_bool_prop x y false.

Theorem Req_bool_spec :
   x y, Req_bool_prop x y (Req_bool x y).

Theorem Req_bool_true :
   x y,
  (x = y)%R Req_bool x y = true.

Theorem Req_bool_false :
   x y,
  (x y)%R Req_bool x y = false.

End Req_bool.

Section Floor_Ceil.

Zfloor and Zceil
Definition Zfloor (x : R) := (up x - 1)%Z.

Theorem Zfloor_lb :
   x : R,
  (IZR (Zfloor x) x)%R.

Theorem Zfloor_ub :
   x : R,
  (x < IZR (Zfloor x) + 1)%R.

Theorem Zfloor_lub :
   n x,
  (IZR n x)%R
  (n Zfloor x)%Z.

Theorem Zfloor_imp :
   n x,
  (IZR n x < IZR (n + 1))%R
  Zfloor x = n.

Theorem Zfloor_IZR :
   n,
  Zfloor (IZR n) = n.

Theorem Zfloor_le :
   x y, (x y)%R
  (Zfloor x Zfloor y)%Z.

Definition Zceil (x : R) := (- Zfloor (- x))%Z.

Theorem Zceil_ub :
   x : R,
  (x IZR (Zceil x))%R.

Theorem Zceil_glb :
   n x,
  (x IZR n)%R
  (Zceil x n)%Z.

Theorem Zceil_imp :
   n x,
  (IZR (n - 1) < x IZR n)%R
  Zceil x = n.

Theorem Zceil_IZR :
   n,
  Zceil (IZR n) = n.

Theorem Zceil_le :
   x y, (x y)%R
  (Zceil x Zceil y)%Z.

Theorem Zceil_floor_neq :
   x : R,
  (IZR (Zfloor x) x)%R
  (Zceil x = Zfloor x + 1)%Z.

Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.

Theorem Ztrunc_IZR :
   n,
  Ztrunc (IZR n) = n.

Theorem Ztrunc_floor :
   x,
  (0 x)%R
  Ztrunc x = Zfloor x.

Theorem Ztrunc_ceil :
   x,
  (x 0)%R
  Ztrunc x = Zceil x.

Theorem Ztrunc_le :
   x y, (x y)%R
  (Ztrunc x Ztrunc y)%Z.

Theorem Ztrunc_opp :
   x,
  Ztrunc (- x) = Zopp (Ztrunc x).

Theorem Ztrunc_abs :
   x,
  Ztrunc (Rabs x) = Zabs (Ztrunc x).

Theorem Ztrunc_lub :
   n x,
  (IZR n Rabs x)%R
  (n Zabs (Ztrunc x))%Z.

Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.

Theorem Zaway_IZR :
   n,
  Zaway (IZR n) = n.

Theorem Zaway_ceil :
   x,
  (0 x)%R
  Zaway x = Zceil x.

Theorem Zaway_floor :
   x,
  (x 0)%R
  Zaway x = Zfloor x.

Theorem Zaway_le :
   x y, (x y)%R
  (Zaway x Zaway y)%Z.

Theorem Zaway_opp :
   x,
  Zaway (- x) = Zopp (Zaway x).

Theorem Zaway_abs :
   x,
  Zaway (Rabs x) = Zabs (Zaway x).

End Floor_Ceil.

Theorem Rcompare_floor_ceil_middle :
   x,
  IZR (Zfloor x) x
  Rcompare (x - IZR (Zfloor x)) (/ 2) = Rcompare (x - IZR (Zfloor x)) (IZR (Zceil x) - x).

Theorem Rcompare_ceil_floor_middle :
   x,
  IZR (Zfloor x) x
  Rcompare (IZR (Zceil x) - x) (/ 2) = Rcompare (IZR (Zceil x) - x) (x - IZR (Zfloor x)).

Section Zdiv_Rdiv.

Theorem Zfloor_div :
   x y,
  y Z0
  Zfloor (IZR x / IZR y) = (x / y)%Z.

End Zdiv_Rdiv.

Section pow.

Variable r : radix.

Theorem radix_pos : (0 < IZR r)%R.

Well-used function called bpow for computing the power function β^e
Definition bpow e :=
  match e with
  | Zpos pIZR (Zpower_pos r p)
  | Zneg pRinv (IZR (Zpower_pos r p))
  | Z0 ⇒ 1%R
  end.

Theorem IZR_Zpower_pos :
   n m,
  IZR (Zpower_pos n m) = powerRZ (IZR n) (Zpos m).

Theorem bpow_powerRZ :
   e,
  bpow e = powerRZ (IZR r) e.

Theorem bpow_ge_0 :
   e : Z, (0 bpow e)%R.

Theorem bpow_gt_0 :
   e : Z, (0 < bpow e)%R.

Theorem bpow_plus :
   e1 e2 : Z, (bpow (e1 + e2) = bpow e1 × bpow e2)%R.

Theorem bpow_1 :
  bpow 1 = IZR r.

Theorem bpow_plus_1 :
   e : Z, (bpow (e + 1) = IZR r × bpow e)%R.

Theorem bpow_opp :
   e : Z, (bpow (-e) = /bpow e)%R.

Theorem IZR_Zpower_nat :
   e : nat,
  IZR (Zpower_nat r e) = bpow (Z_of_nat e).

Theorem IZR_Zpower :
   e : Z,
  (0 e)%Z
  IZR (Zpower r e) = bpow e.

Theorem bpow_lt :
   e1 e2 : Z,
  (e1 < e2)%Z (bpow e1 < bpow e2)%R.

Theorem lt_bpow :
   e1 e2 : Z,
  (bpow e1 < bpow e2)%R (e1 < e2)%Z.

Theorem bpow_le :
   e1 e2 : Z,
  (e1 e2)%Z (bpow e1 bpow e2)%R.

Theorem le_bpow :
   e1 e2 : Z,
  (bpow e1 bpow e2)%R (e1 e2)%Z.

Theorem bpow_inj :
   e1 e2 : Z,
  bpow e1 = bpow e2 e1 = e2.

Theorem bpow_exp :
   e : Z,
  bpow e = exp (IZR e × ln (IZR r)).

Another well-used function for having the magnitude of a real number x to the base β
Record mag_prop x := {
  mag_val :> Z ;
  _ : (x 0)%R (bpow (mag_val - 1)%Z Rabs x < bpow mag_val)%R
}.

Definition mag :
   x : R, mag_prop x.

Theorem bpow_lt_bpow :
   e1 e2,
  (bpow (e1 - 1) < bpow e2)%R
  (e1 e2)%Z.

Theorem bpow_unique :
   x e1 e2,
  (bpow (e1 - 1) x < bpow e1)%R
  (bpow (e2 - 1) x < bpow e2)%R
  e1 = e2.

Theorem mag_unique :
   (x : R) (e : Z),
  (bpow (e - 1) Rabs x < bpow e)%R
  mag x = e :> Z.

Theorem mag_opp :
   x,
  mag (-x) = mag x :> Z.

Theorem mag_abs :
   x,
  mag (Rabs x) = mag x :> Z.

Theorem mag_unique_pos :
   (x : R) (e : Z),
  (bpow (e - 1) x < bpow e)%R
  mag x = e :> Z.

Theorem mag_le_abs :
   x y,
  (x 0)%R (Rabs x Rabs y)%R
  (mag x mag y)%Z.

Theorem mag_le :
   x y,
  (0 < x)%R (x y)%R
  (mag x mag y)%Z.

Lemma lt_mag :
   x y,
  (0 < y)%R
  (mag x < mag y)%Z (x < y)%R.

Theorem mag_bpow :
   e, (mag (bpow e) = e + 1 :> Z)%Z.

Theorem mag_mult_bpow :
   x e, x 0%R
  (mag (x × bpow e) = mag x + e :>Z)%Z.

Theorem mag_le_bpow :
   x e,
  x 0%R
  (Rabs x < bpow e)%R
  (mag x e)%Z.

Theorem mag_gt_bpow :
   x e,
  (bpow e Rabs x)%R
  (e < mag x)%Z.

Theorem mag_ge_bpow :
   x e,
  (bpow (e - 1) Rabs x)%R
  (e mag x)%Z.

Theorem bpow_mag_gt :
   x,
  (Rabs x < bpow (mag x))%R.

Theorem bpow_mag_le :
   x, (x 0)%R
    (bpow (mag x-1) Rabs x)%R.

Theorem mag_le_Zpower :
   m e,
  m Z0
  (Zabs m < Zpower r e)%Z
  (mag (IZR m) e)%Z.

Theorem mag_gt_Zpower :
   m e,
  m Z0
  (Zpower r e Zabs m)%Z
  (e < mag (IZR m))%Z.

Lemma mag_mult :
   x y,
  (x 0)%R (y 0)%R
  (mag x + mag y - 1 mag (x × y) mag x + mag y)%Z.

Lemma mag_plus :
   x y,
  (0 < y)%R (y x)%R
  (mag x mag (x + y) mag x + 1)%Z.

Lemma mag_minus :
   x y,
  (0 < y)%R (y < x)%R
  (mag (x - y) mag x)%Z.

Lemma mag_minus_lb :
   x y,
  (0 < x)%R (0 < y)%R
  (mag y mag x - 2)%Z
  (mag x - 1 mag (x - y))%Z.

Lemma mag_div :
   x y : R,
  x 0%R y 0%R
  (mag x - mag y mag (x / y) mag x - mag y + 1)%Z.

Lemma mag_sqrt :
   x,
  (0 < x)%R
  mag (sqrt x) = Zdiv2 (mag x + 1) :> Z.

End pow.

Section Bool.

Theorem eqb_sym :
   x y, Bool.eqb x y = Bool.eqb y x.

Theorem eqb_false :
   x y, x = negb y Bool.eqb x y = false.

Theorem eqb_true :
   x y, x = y Bool.eqb x y = true.

End Bool.

Section cond_Ropp.

Definition cond_Ropp (b : bool) m := if b then Ropp m else m.

Theorem IZR_cond_Zopp :
   b m,
  IZR (cond_Zopp b m) = cond_Ropp b (IZR m).

Theorem abs_cond_Ropp :
   b m,
  Rabs (cond_Ropp b m) = Rabs m.

Theorem cond_Ropp_Rlt_bool :
   m,
  cond_Ropp (Rlt_bool m 0) m = Rabs m.

Theorem cond_Ropp_involutive :
   b x,
  cond_Ropp b (cond_Ropp b x) = x.

Theorem cond_Ropp_inj :
   b x y,
  cond_Ropp b x = cond_Ropp b y x = y.

Theorem cond_Ropp_mult_l :
   b x y,
  cond_Ropp b (x × y) = (cond_Ropp b x × y)%R.

Theorem cond_Ropp_mult_r :
   b x y,
  cond_Ropp b (x × y) = (x × cond_Ropp b y)%R.

Theorem cond_Ropp_plus :
   b x y,
  cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R.

End cond_Ropp.

LPO taken from Coquelicot

Theorem LPO_min :
   P : nat Prop, ( n, P n ¬ P n)
  {n : nat | P n i, (i < n)%nat ¬ P i} + { n, ¬ P n}.

Theorem LPO :
   P : nat Prop, ( n, P n ¬ P n)
  {n : nat | P n} + { n, ¬ P n}.

Lemma LPO_Z : P : Z Prop, ( n, P n ¬P n)
  {n : Z| P n} + { n, ¬ P n}.

A little tactic to simplify terms of the form bpow a × bpow b.
Ltac bpow_simplify :=
  
  repeat
    match goal with
      | |- context [(bpow _ _ × bpow _ _)] ⇒
        rewrite <- bpow_plus
      | |- context [(?X1 × bpow _ _ × bpow _ _)] ⇒
        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
      | |- context [(?X1 × (?X2 × bpow _ _) × bpow _ _)] ⇒
        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
        rewrite <- bpow_plus
    end;
  
  repeat
    match goal with
      | |- context [(bpow _ ?X)] ⇒
        progress ring_simplify X
    end;
  
  change (bpow _ 0) with 1;
  repeat
    match goal with
      | |- context [(_ × 1)] ⇒
        rewrite Rmult_1_r
    end.