Library Flocq.Core.Fcore_Raux

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 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 Export Reals.
Require Export ZArith.
Require Export Fcore_Zaux.

Section Rmissing.

About R
Theorem Rle_0_minus :
  forall x y, (x <= y)%R -> (0 <= y - x)%R.

Theorem Rabs_eq_Rabs :
  forall x y : R,
  Rabs x = Rabs y -> x = y \/ x = Ropp y.

Theorem Rabs_minus_le:
  forall x y : R,
  (0 <= y)%R -> (y <= 2*x)%R ->
  (Rabs (x-y) <= x)%R.

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

Theorem Rplus_le_reg_r :
  forall r r1 r2 : R,
  (r1 + r <= r2 + r)%R -> (r1 <= r2)%R.

Theorem Rmult_lt_reg_r :
  forall r r1 r2 : R, (0 < r)%R ->
  (r1 * r < r2 * r)%R -> (r1 < r2)%R.

Theorem Rmult_le_reg_r :
  forall r r1 r2 : R, (0 < r)%R ->
  (r1 * r <= r2 * r)%R -> (r1 <= r2)%R.

Theorem Rmult_eq_reg_r :
  forall r r1 r2 : R, (r1 * r)%R = (r2 * r)%R ->
  r <> 0%R -> r1 = r2.

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

Theorem Rmult_min_distr_r :
  forall r r1 r2 : R,
  (0 <= r)%R ->
  (Rmin r1 r2 * r)%R = Rmin (r1 * r) (r2 * r).

Theorem Rmult_min_distr_l :
  forall r r1 r2 : R,
  (0 <= r)%R ->
  (r * Rmin r1 r2)%R = Rmin (r * r1) (r * r2).

Theorem exp_le :
  forall x y : R,
  (x <= y)%R -> (exp x <= exp y)%R.

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

Theorem Rinv_le :
  forall x y,
  (0 < x)%R -> (x <= y)%R -> (/y <= /x)%R.

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

Theorem Rabs_le :
  forall x y,
  (-y <= x <= y)%R -> (Rabs x <= y)%R.

Theorem Rabs_le_inv :
  forall x y,
  (Rabs x <= y)%R -> (-y <= x <= y)%R.

Theorem Rabs_ge :
  forall x y,
  (y <= -x \/ x <= y)%R -> (x <= Rabs y)%R.

Theorem Rabs_ge_inv :
  forall x y,
  (x <= Rabs y)%R -> (y <= -x \/ x <= y)%R.

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

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

Theorem Rabs_gt :
  forall x y,
  (y < -x \/ x < y)%R -> (x < Rabs y)%R.

Theorem Rabs_gt_inv :
  forall x y,
  (x < Rabs y)%R -> (y < -x \/ x < y)%R.

End Rmissing.

Section Z2R.

Z2R function (Z -> R)
Fixpoint P2R (p : positive) :=
  match p with
  | xH => 1%R
  | xO xH => 2%R
  | xO t => (2 * P2R t)%R
  | xI xH => 3%R
  | xI t => (1 + 2 * P2R t)%R
  end.

Definition Z2R n :=
  match n with
  | Zpos p => P2R p
  | Zneg p => Ropp (P2R p)
  | Z0 => R0
  end.

Theorem P2R_INR :
  forall n, P2R n = INR (nat_of_P n).

Theorem Z2R_IZR :
  forall n, Z2R n = IZR n.

Theorem Z2R_opp :
  forall n, Z2R (-n) = (- Z2R n)%R.

Theorem Z2R_plus :
  forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R.

Theorem minus_IZR :
  forall n m : Z,
  IZR (n - m) = (IZR n - IZR m)%R.

Theorem Z2R_minus :
  forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R.

Theorem Z2R_mult :
  forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R.

Theorem le_Z2R :
  forall m n, (Z2R m <= Z2R n)%R -> (m <= n)%Z.

Theorem Z2R_le :
  forall m n, (m <= n)%Z -> (Z2R m <= Z2R n)%R.

Theorem lt_Z2R :
  forall m n, (Z2R m < Z2R n)%R -> (m < n)%Z.

Theorem Z2R_lt :
  forall m n, (m < n)%Z -> (Z2R m < Z2R n)%R.

Theorem Z2R_le_lt :
  forall m n p, (m <= n < p)%Z -> (Z2R m <= Z2R n < Z2R p)%R.

Theorem le_lt_Z2R :
  forall m n p, (Z2R m <= Z2R n < Z2R p)%R -> (m <= n < p)%Z.

Theorem eq_Z2R :
  forall m n, (Z2R m = Z2R n)%R -> (m = n)%Z.

Theorem neq_Z2R :
  forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z.

Theorem Z2R_neq :
  forall m n, (m <> n)%Z -> (Z2R m <> Z2R n)%R.

Theorem Z2R_abs :
  forall z, Z2R (Zabs z) = Rabs (Z2R z).

End Z2R.

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 :
  forall x y, Rcompare_prop x y (Rcompare x y).

Global Opaque Rcompare.

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

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

Theorem Rcompare_not_Lt :
  forall x y,
  (y <= x)%R -> Rcompare x y <> Lt.

Theorem Rcompare_not_Lt_inv :
  forall x y,
  Rcompare x y <> Lt -> (y <= x)%R.

Theorem Rcompare_Eq :
  forall x y,
  x = y -> Rcompare x y = Eq.

Theorem Rcompare_Eq_inv :
  forall x y,
  Rcompare x y = Eq -> x = y.

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

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

Theorem Rcompare_not_Gt :
  forall x y,
  (x <= y)%R -> Rcompare x y <> Gt.

Theorem Rcompare_not_Gt_inv :
  forall x y,
  Rcompare x y <> Gt -> (x <= y)%R.

Theorem Rcompare_Z2R :
  forall x y, Rcompare (Z2R x) (Z2R y) = Zcompare x y.

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

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

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

Theorem Rcompare_mult_r :
  forall z x y,
  (0 < z)%R ->
  Rcompare (x * z) (y * z) = Rcompare x y.

Theorem Rcompare_mult_l :
  forall z x y,
  (0 < z)%R ->
  Rcompare (z * x) (z * y) = Rcompare x y.

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

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

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

Theorem Rcompare_sqr :
  forall x y,
  (0 <= x)%R -> (0 <= y)%R ->
  Rcompare (x * x) (y * y) = Rcompare x y.

Theorem Rmin_compare :
  forall x y,
  Rmin x y = match Rcompare x y with Lt => x | Eq => x | Gt => y end.

End Rcompare.

Section Rle_bool.

Definition Rle_bool x y :=
  match Rcompare x y with
  | Gt => false
  | _ => 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 :
  forall x y, Rle_bool_prop x y (Rle_bool x y).

Theorem Rle_bool_true :
  forall x y,
  (x <= y)%R -> Rle_bool x y = true.

Theorem Rle_bool_false :
  forall 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
  | Lt => true
  | _ => 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 :
  forall x y, Rlt_bool_prop x y (Rlt_bool x y).

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

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

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

Theorem Rlt_bool_false :
  forall 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
  | Eq => true
  | _ => 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 :
  forall x y, Req_bool_prop x y (Req_bool x y).

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

Theorem Req_bool_false :
  forall 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 :
  forall x : R,
  (Z2R (Zfloor x) <= x)%R.

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

Theorem Zfloor_lub :
  forall n x,
  (Z2R n <= x)%R ->
  (n <= Zfloor x)%Z.

Theorem Zfloor_imp :
  forall n x,
  (Z2R n <= x < Z2R (n + 1))%R ->
  Zfloor x = n.

Theorem Zfloor_Z2R :
  forall n,
  Zfloor (Z2R n) = n.

Theorem Zfloor_le :
  forall x y, (x <= y)%R ->
  (Zfloor x <= Zfloor y)%Z.

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

Theorem Zceil_ub :
  forall x : R,
  (x <= Z2R (Zceil x))%R.

Theorem Zceil_glb :
  forall n x,
  (x <= Z2R n)%R ->
  (Zceil x <= n)%Z.

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

Theorem Zceil_Z2R :
  forall n,
  Zceil (Z2R n) = n.

Theorem Zceil_le :
  forall x y, (x <= y)%R ->
  (Zceil x <= Zceil y)%Z.

Theorem Zceil_floor_neq :
  forall x : R,
  (Z2R (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_Z2R :
  forall n,
  Ztrunc (Z2R n) = n.

Theorem Ztrunc_floor :
  forall x,
  (0 <= x)%R ->
  Ztrunc x = Zfloor x.

Theorem Ztrunc_ceil :
  forall x,
  (x <= 0)%R ->
  Ztrunc x = Zceil x.

Theorem Ztrunc_le :
  forall x y, (x <= y)%R ->
  (Ztrunc x <= Ztrunc y)%Z.

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

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

Theorem Ztrunc_lub :
  forall n x,
  (Z2R 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_Z2R :
  forall n,
  Zaway (Z2R n) = n.

Theorem Zaway_ceil :
  forall x,
  (0 <= x)%R ->
  Zaway x = Zceil x.

Theorem Zaway_floor :
  forall x,
  (x <= 0)%R ->
  Zaway x = Zfloor x.

Theorem Zaway_le :
  forall x y, (x <= y)%R ->
  (Zaway x <= Zaway y)%Z.

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

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

End Floor_Ceil.

Section Zdiv_Rdiv.

Theorem Zfloor_div :
  forall x y,
  y <> Z0 ->
  Zfloor (Z2R x / Z2R y) = (x / y)%Z.

End Zdiv_Rdiv.

Section pow.

Variable r : radix.

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

Well-used function called bpow for computing the power function β^e
Definition bpow e :=
  match e with
  | Zpos p => Z2R (Zpower_pos r p)
  | Zneg p => Rinv (Z2R (Zpower_pos r p))
  | Z0 => R1
  end.

Theorem Z2R_Zpower_pos :
  forall n m,
  Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m).

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

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

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

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

Theorem bpow_1 :
  bpow 1 = Z2R r.

Theorem bpow_plus1 :
  forall e : Z, (bpow (e + 1) = Z2R r * bpow e)%R.

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

Theorem Z2R_Zpower_nat :
  forall e : nat,
  Z2R (Zpower_nat r e) = bpow (Z_of_nat e).

Theorem Z2R_Zpower :
  forall e : Z,
  (0 <= e)%Z ->
  Z2R (Zpower r e) = bpow e.

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

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

Theorem bpow_le :
  forall e1 e2 : Z,
  (e1 <= e2)%Z -> (bpow e1 <= bpow e2)%R.

Theorem le_bpow :
  forall e1 e2 : Z,
  (bpow e1 <= bpow e2)%R -> (e1 <= e2)%Z.

Theorem bpow_inj :
  forall e1 e2 : Z,
  bpow e1 = bpow e2 -> e1 = e2.

Theorem bpow_exp :
  forall e : Z,
  bpow e = exp (Z2R e * ln (Z2R r)).

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

Definition ln_beta :
  forall x : R, ln_beta_prop x.

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

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

Theorem ln_beta_unique :
  forall (x : R) (e : Z),
  (bpow (e - 1) <= Rabs x < bpow e)%R ->
  ln_beta x = e :> Z.

Theorem ln_beta_opp :
  forall x,
  ln_beta (-x) = ln_beta x :> Z.

Theorem ln_beta_abs :
  forall x,
  ln_beta (Rabs x) = ln_beta x :> Z.

Theorem ln_beta_le_abs :
  forall x y,
  (x <> 0)%R -> (Rabs x <= Rabs y)%R ->
  (ln_beta x <= ln_beta y)%Z.

Theorem ln_beta_le :
  forall x y,
  (0 < x)%R -> (x <= y)%R ->
  (ln_beta x <= ln_beta y)%Z.

Theorem ln_beta_bpow :
  forall e, (ln_beta (bpow e) = e + 1 :> Z)%Z.

Theorem ln_beta_le_bpow :
  forall x e,
  x <> R0 ->
  (Rabs x < bpow e)%R ->
  (ln_beta x <= e)%Z.

Theorem ln_beta_gt_bpow :
  forall x e,
  (bpow e <= Rabs x)%R ->
  (e < ln_beta x)%Z.

Theorem ln_beta_le_Zpower :
  forall m e,
  m <> Z0 ->
  (Zabs m < Zpower r e)%Z->
  (ln_beta (Z2R m) <= e)%Z.

Theorem ln_beta_gt_Zpower :
  forall m e,
  m <> Z0 ->
  (Zpower r e <= Zabs m)%Z ->
  (e < ln_beta (Z2R m))%Z.

End pow.

Section Bool.

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

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

Theorem eqb_true :
  forall x y, x = y -> Bool.eqb x y = true.

End Bool.

Section cond_opp.

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

Theorem Z2R_cond_Zopp :
  forall b m,
  Z2R (cond_Zopp b m) = cond_Ropp b (Z2R m).

Theorem abs_cond_Zopp :
  forall b m,
  Zabs (cond_Zopp b m) = Zabs m.

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

Theorem cond_Zopp_Zlt_bool :
  forall m,
  cond_Zopp (Zlt_bool m 0) m = Zabs m.

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

End cond_opp.