Library Interval.Float.Generic_proof

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/

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: http://www.cecill.info/

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 ZArith Psatz.
From Flocq Require Import Core Digits Bracket Round Operations.
From mathcomp.ssreflect Require Import ssrbool.

Require Import Stdlib.
Require Import Xreal.
Require Import Basic.
Require Import Generic.

Local Existing Instance zpos_gt_0.
Local Existing Instance valid_rnd_of_mode.

Lemma FtoR_Rpos :
  ∀ beta m e,
  (0 < FtoR beta false m e)%R.

Lemma FtoR_neg :
  ∀ beta s m e,
  (- FtoR beta s m e = FtoR beta (negb s) m e)%R.

Lemma FtoR_Rneg :
  ∀ beta m e,
  (FtoR beta true m e < 0)%R.

Lemma FtoR_non_neg :
  ∀ beta s m e,
  (FtoR beta s m e ≠ 0)%R.

Lemma FtoR_abs :
  ∀ beta s m e,
  (Rabs (FtoR beta s m e) = FtoR beta false m e)%R.

Lemma FtoR_add :
  ∀ beta s m1 m2 e,
  (FtoR beta s m1 e + FtoR beta s m2 e)%R = FtoR beta s (m1 + m2) e.

Lemma FtoR_sub :
  ∀ beta s m1 m2 e,
  (Zpos m2 < Zpos m1)%Z →
  (FtoR beta s m1 e + FtoR beta (negb s) m2 e)%R = FtoR beta s (m1 - m2) e.

Lemma FtoR_mul :
  ∀ beta s1 s2 m1 m2 e1 e2,
  (FtoR beta s1 m1 e1 × FtoR beta s2 m2 e2)%R =
  FtoR beta (xorb s1 s2) (m1 × m2) (e1 + e2).

Lemma shift_correct :
  ∀ beta m e,
  Zpos (shift beta m e) = (Zpos m × Zpower_pos beta e)%Z.

Lemma FtoR_shift :
  ∀ beta s m e p,
  FtoR beta s m (e + Zpos p) = FtoR beta s (shift beta m p) e.

Lemma digits_conversion :
  ∀ beta p,
  Zdigits beta (Zpos p) = Zpos (count_digits beta p).

Theorem Fneg_correct :
  ∀ beta (f : float beta),
  FtoX (Fneg f) = Xneg (FtoX f).

Theorem Fabs_correct :
  ∀ beta (f : float beta),
  FtoX (Fabs f) = Xabs (FtoX f).

Lemma cond_Zopp_mult :
  ∀ s u v,
  cond_Zopp s (u × v) = (cond_Zopp s u × v)%Z.

Theorem Fscale2_correct :
  ∀ beta (f : float beta) d,
  match radix_val beta with Zpos (xO _) ⇒ true | _ ⇒ false end = true →
  FtoX (Fscale2 f d) = Xmul (FtoX f) (Xreal (bpow radix2 d)).

Lemma Fcmp_aux2_correct :
  ∀ beta m1 m2 e1 e2,
  Fcmp_aux2 beta m1 e1 m2 e2 =
  Xcmp (Xreal (FtoR beta false m1 e1)) (Xreal (FtoR beta false m2 e2)).

Theorem Fcmp_correct :
  ∀ beta (x y : float beta),
  Fcmp x y = Xcmp (FtoX x) (FtoX y).

Theorem Fmin_correct :
  ∀ beta (x y : float beta),
  FtoX (Fmin x y) = Xmin (FtoX x) (FtoX y).

Theorem Fmax_correct :
  ∀ beta (x y : float beta),
  FtoX (Fmax x y) = Xmax (FtoX x) (FtoX y).

Ltac refl_exists :=
  repeat match goal with
  | |- ex ?P ⇒ eapply ex_intro
  end ;
  repeat split.

Definition convert_location_inv l :=
  match l with
  | pos_Eq ⇒ loc_Exact
  | pos_Lo ⇒ loc_Inexact Lt
  | pos_Mi ⇒ loc_Inexact Eq
  | pos_Up ⇒ loc_Inexact Gt
  end.

Lemma convert_location_bij :
  ∀ l, convert_location_inv (convert_location l) = l.

Definition mode_choice mode s m l :=
  match mode with
  | rnd_UP ⇒ cond_incr (round_sign_UP s l) m
  | rnd_DN ⇒ cond_incr (round_sign_DN s l) m
  | rnd_ZR ⇒ m
  | rnd_NE ⇒ cond_incr (round_N (negb (Z.even m)) l) m
  end.

Lemma adjust_mantissa_correct :
  ∀ mode s m pos,
  Zpos (adjust_mantissa mode m pos s) = mode_choice mode s (Zpos m) (convert_location_inv pos).

Lemma adjust_pos_correct :
  ∀ q r pos,
  (1 < Zpos q)%Z →
  (0 ≤ r < Zpos q)%Z →
  convert_location_inv (adjust_pos r q pos) = new_location (Zpos q) r (convert_location_inv pos).

Lemma even_radix_correct :
  ∀ beta,
  match radix_val beta with Zpos (xO _) ⇒ true | _ ⇒ false end = Z.even beta.

Lemma Fround_at_prec_correct :
  ∀ beta mode prec s m1 e1 pos x,
  (0 < x)%R →
  inbetween_float beta (Zpos m1) e1 x (convert_location_inv pos) →
  ( (Zpos (count_digits beta m1) < Zpos prec)%Z → pos = pos_Eq ) →
  FtoX (Fround_at_prec mode prec (@Ufloat beta s m1 e1 pos)) =
    Xreal (round beta mode prec (if s then Ropp x else x)).

Definition ufloat_pos_Eq beta (x : ufloat beta) :=
  match x with Ufloat _ _ _ pos_Eq ⇒ True | Ufloat _ _ _ _ ⇒ False | _ ⇒ True end.

Lemma UtoX_pos_Eq :
  ∀ beta (x : ufloat beta),
  (UtoX x = Xnan → x = Unan ) →
  ufloat_pos_Eq beta x.

Lemma Fround_at_prec_pos_Eq :
  ∀ beta mode prec (x : ufloat beta),
  ufloat_pos_Eq beta x →
  FtoX (Fround_at_prec mode prec x) = Xround beta mode prec (UtoX x).

Lemma Rdiv_lt_mult_pos a b c :
(0 < b → a × b < c → a < c / b)%R.

Lemma Rdiv_le_mult_pos a b c :
(0 < b → a × b ≤ c → a ≤ c / b)%R.

Lemma Rdiv_gt_mult_pos a b c :
(0 < b → a < b × c → a / b < c)%R.

Lemma Rdiv_ge_mult_pos a b c :
(0 < b → a ≤ b × c → a / b ≤ c)%R.

Lemma Znearest_IZR c z : Znearest c (IZR z) = z.

Lemma Rnearbyint_IZR mode z : Rnearbyint mode (IZR z) = IZR z.

Lemma adjust_mantissa_Eq mode b p : adjust_mantissa mode p pos_Eq b = p.

Lemma radix_to_pos (r : radix) : Z.pos (Z.to_pos r) = r.

Lemma shift1_correct r e :
  shift r 1 e = (Z.to_pos r ^ e)%positive.

Lemma Rcompare_div_l x y z :
  (0 < y)%R → Rcompare (x / y) z = Rcompare x (y × z).

Lemma Rcompare_div_r x y z :
  (0 < z)%R → Rcompare x (y / z) = Rcompare (z × x) y.

Lemma Rlt_bool_float beta b m e : Rlt_bool (FtoR beta b m e) 0 = b.

Lemma Fnearbyint_exact_correct :
  ∀ beta mode (x : float beta),
  FtoX (Fnearbyint_exact mode x) = Xnearbyint mode (FtoX x).

Lemma Fadd_slow_aux1_correct :
  ∀ beta sx sy mx my e,
  UtoX (Fadd_slow_aux1 beta sx sy mx my e pos_Eq) =
  Xadd (FtoX (@Float beta sx mx e)) (FtoX (@Float beta sy my e)).

Lemma Fadd_slow_aux2_correct :
  ∀ beta sx sy mx my ex ey,
  UtoX (Fadd_slow_aux2 beta sx sy mx my ex ey pos_Eq) =
  Xadd (FtoX (@Float beta sx mx ex)) (FtoX (@Float beta sy my ey)).

Theorem Fadd_slow_aux_correct :
  ∀ beta (x y : float beta),
  UtoX (Fadd_slow_aux x y) = Xadd (FtoX x) (FtoX y).

Theorem Fadd_slow_correct :
  ∀ beta mode prec (x y : float beta),
  FtoX (Fadd_slow mode prec x y) = Xround beta mode prec (Xadd (FtoX x) (FtoX y)).

Definition Fadd_correct := Fadd_slow_correct.

Theorem Fadd_exact_correct :
  ∀ beta (x y : float beta),
  FtoX (Fadd_exact x y) = Xadd (FtoX x) (FtoX y).

Lemma Fsub_split :
  ∀ beta mode prec (x y : float beta),
  FtoX (Fsub mode prec x y) = (FtoX (Fadd mode prec x (Fneg y))).

Theorem Fsub_correct :
  ∀ beta mode prec (x y : float beta),
  FtoX (Fsub mode prec x y) = Xround beta mode prec (Xsub (FtoX x) (FtoX y)).

Theorem Fmul_aux_correct :
  ∀ beta (x y : float beta),
  UtoX (Fmul_aux x y) = Xmul (FtoX x) (FtoX y).

Theorem Fmul_correct :
  ∀ beta mode prec (x y : float beta),
  FtoX (Fmul mode prec x y) = Xround beta mode prec (Xmul (FtoX x) (FtoX y)).

Theorem Fdiv_correct :
  ∀ beta mode prec (x y : float beta),
  FtoX (Fdiv mode prec x y) = Xround beta mode prec (Xdiv (FtoX x) (FtoX y)).

Lemma Fsqrt_correct :
  ∀ beta mode prec (x : float beta),
  FtoX (Fsqrt mode prec x) = Xround beta mode prec (Xsqrt_nan (FtoX x)).