LAProof.accuracy_proofs.float_acc_lems

From LAProof.accuracy_proofs Require Import preamble common.

Section GenFloat.
Context {NAN: FPCore.Nans} {t : type} .

Lemma Bmult_0R (a f: ftype t) :
Binary.is_finite (BMULT a f) →
FT2R a = 0 →
(BMULT a f) = neg_zero ∨ (BMULT a f) = pos_zero.

Lemma Bplus_0R (a f: ftype t) :
Binary.is_finite (BPLUS a f) →
FT2R f = 0 →
FT2R (BPLUS a f) = FT2R a.

Lemma Bfma_mult_0R (a f s : ftype t):
Binary.is_finite (BFMA a f s) →
FT2R a = 0 →
FT2R (BFMA a f s) = FT2R s.

Fact neg_zero_is_finite: Binary.is_finite (@neg_zero t).

Fact FT2R_neg_zero : FT2R (@neg_zero t) = 0.

Fact FT2R_pos_zero : FT2R (@pos_zero t) = 0.

Fact FT2R_Zconst_0 : FT2R (Zconst t 0) = 0.

Definition fma_no_overflow (x y z: R) : Prop :=
  (Rabs (rounded t (x × y + z)) < Raux.bpow Zaux.radix2 (femax t))%R.

Definition Bmult_no_overflow (x y: R) : Prop :=
  (Rabs (rounded t (x × y)) < Raux.bpow Zaux.radix2 (femax t))%R.

Notation D := (@default_rel t).
Notation E := (@default_abs t).

Lemma generic_round_property:
  ∀ (x: R),
∃ delta epsilon : R,
   delta × epsilon = 0 ∧
  (Rabs delta ≤ D)%R ∧
  (Rabs epsilon ≤ E)%R ∧
   Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode BinarySingleNaN.mode_NE)
               x = (x × (1+delta)+epsilon)%Re.

Lemma fma_accurate :
   ∀ (x: ftype t) (FINx: Binary.is_finite x)
          (y: ftype t) (FINy: Binary.is_finite y)
          (z: ftype t) (FINz: Binary.is_finite z)
          (FIN: fma_no_overflow (FT2R x) (FT2R y) (FT2R z)),
  ∃ delta, ∃ epsilon,
   delta × epsilon = 0 ∧
   Rabs delta ≤ D ∧
   Rabs epsilon ≤ E ∧
   (FT2R (BFMA x y z) = (FT2R x × FT2R y + FT2R z) × (1+delta) + epsilon)%Re.

Lemma is_finite_fma_no_overflow :
  ∀ (x y z: ftype t)
  (HFINb : Binary.is_finite (BFMA x y z)),
  fma_no_overflow (FT2R x) (FT2R y) (FT2R z).

Lemma BFMA_finite_e :
 ∀ (a f u : ftype t)
 (Hfin : Binary.is_finite (BFMA a f u)),
 Binary.is_finite a ∧
 Binary.is_finite f ∧
 Binary.is_finite u.

Lemma fma_accurate' :
   ∀ (x y z : ftype t)
          (FIN: Binary.is_finite (BFMA x y z)),
  ∃ delta, ∃ epsilon,
   delta × epsilon = 0 ∧
   Rabs delta ≤ @default_rel t ∧
   Rabs epsilon ≤ @default_abs t ∧
   (FT2R (BFMA x y z) = (FT2R x × FT2R y + FT2R z) × (1+delta) + epsilon)%Re.

Lemma BMULT_accurate :
  ∀ (x y : ftype t) (FIN: Bmult_no_overflow (FT2R x) (FT2R y)),
  ∃ delta, ∃ epsilon,
   delta × epsilon = 0 ∧
   Rabs delta ≤ @default_rel t ∧
   Rabs epsilon ≤ @default_abs t ∧
   (FT2R (BMULT x y) = (FT2R x × FT2R y) × (1+delta) + epsilon)%Re.

Lemma is_finite_BMULT_no_overflow :
 ∀ (x y : ftype t)
  (HFINb : Binary.is_finite (BMULT x y) ),
  Bmult_no_overflow (FT2R x) (FT2R y).

Lemma BMULT_accurate' :
  ∀
  (x y : ftype t)
  (FIN: Binary.is_finite (BMULT x y)),
  ∃ delta, ∃ epsilon,
   delta × epsilon = 0 ∧
   Rabs delta ≤ @default_rel t ∧
   Rabs epsilon ≤ @default_abs t ∧
   (FT2R (BMULT x y) = (FT2R x × FT2R y) × (1+delta) + epsilon)%Re.

Lemma BMULT_finite_e :
 ∀ (a b : ftype t) (Hfin : Binary.is_finite (BMULT a b)),
 Binary.is_finite a ∧ Binary.is_finite b.

Lemma BPLUS_finite_e :
 ∀ (a b : ftype t) (Hfin : Binary.is_finite (BPLUS a b)),
 Binary.is_finite a ∧ Binary.is_finite b.

Lemma BMINUS_finite_sub :
 ∀ (a b : ftype t) (Hfin : Binary.is_finite (BMINUS a b)),
 Binary.is_finite a ∧ Binary.is_finite b.

Definition Bplus_no_overflow (x y: R) : Prop :=
  (Rabs ( Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode
                 BinarySingleNaN.mode_NE) (x + y )) < Raux.bpow Zaux.radix2 (femax t))%R.

Lemma BPLUS_B2R_zero (a : ftype t):
  Binary.is_finite a →
  FT2R (BPLUS a (Zconst t 0)) = FT2R a.

Lemma BPLUS_accurate :
 ∀ (x : ftype t) (FINx: Binary.is_finite x)
             (y : ftype t) (FINy: Binary.is_finite y)
          (FIN: Bplus_no_overflow (FT2R x) (FT2R y)),
  ∃ delta,
   Rabs delta ≤ @default_rel t ∧
   (FT2R (BPLUS x y ) = (FT2R x + FT2R y) × (1+delta))%Re.

Lemma is_finite_sum_no_overflow :
  ∀ (x y: ftype t)
  (HFINb : Binary.is_finite (BPLUS x y)),
  Bplus_no_overflow (FT2R x) (FT2R y).

Lemma no_overflow_sum_is_finite :
  ∀ (x y: ftype t)
  (H1 : Binary.is_finite x)
  (H2 : Binary.is_finite y)
  (Hov : Bplus_no_overflow (FT2R x) (FT2R y)),
  Binary.is_finite (BPLUS x y).

Lemma BPLUS_accurate' :
  ∀ (x y : ftype t)
  (FIN: Binary.is_finite (BPLUS x y)),
  ∃ delta,
   Rabs delta ≤ @default_rel t ∧
   (FT2R (BPLUS x y ) = (FT2R x + FT2R y) × (1+delta))%Re.

Definition Bminus_no_overflow (x y: R) : Prop :=
  (Rabs ( Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode
                 BinarySingleNaN.mode_NE) (x - y )) < Raux.bpow Zaux.radix2 (femax t))%R.

Lemma is_finite_minus_no_overflow :
  ∀ (x y: ftype t)
  (HFINb : Binary.is_finite (BMINUS x y)),
  Bminus_no_overflow (FT2R x) (FT2R y).

Lemma no_overflow_minus_is_finite :
  ∀ (x y: ftype t)
  (H1 : Binary.is_finite x)
  (H2 : Binary.is_finite y)
  (Hov : Bminus_no_overflow (FT2R x) (FT2R y)),
  Binary.is_finite (BMINUS x y).

Lemma BMINUS_accurate :
 ∀ (x : ftype t) (FINx: Binary.is_finite x)
             (y : ftype t) (FINy: Binary.is_finite y)
          (FIN: Bminus_no_overflow (FT2R x) (FT2R y)),
  ∃ delta,
   Rabs delta ≤ @default_rel t ∧
   (FT2R (BMINUS x y ) = (FT2R x - FT2R y) × (1+delta))%Re.

Lemma BMINUS_accurate' :
  ∀ (x y : ftype t)
  (FIN: Binary.is_finite (BMINUS x y)),
  ∃ delta,
   Rabs delta ≤ @default_rel t ∧
   (FT2R (BMINUS x y ) = (FT2R x - FT2R y) × (1+delta))%Re.

Lemma BPLUS_correct (a b: ftype t):
  Binary.is_finite (BPLUS a b)→
  (Binary.is_finite a ∧ Binary.is_finite b) ∧
  FT2R (BPLUS a b) =
    Generic_fmt.round Zaux.radix2 (SpecFloat.fexp (fprec t) (femax t))
      (BinarySingleNaN.round_mode BinarySingleNaN.mode_NE)
      (FT2R a + FT2R b).

Lemma BMULT_correct (a b: ftype t):
  Binary.is_finite (BMULT a b) →
  (Binary.is_finite a ∧
  Binary.is_finite b) ∧
  FT2R (BMULT a b) =
  Generic_fmt.round Zaux.radix2 (SpecFloat.fexp (fprec t) (femax t))
  (BinarySingleNaN.round_mode BinarySingleNaN.mode_NE)
  (FT2R a × FT2R b).

Lemma BFMA_correct (a b s: ftype t) :
  Binary.is_finite (BFMA a b s) →
 (Binary.is_finite a ∧ Binary.is_finite b ∧ Binary.is_finite s) ∧
  FT2R (BFMA a b s) =
    Generic_fmt.round Zaux.radix2 (SpecFloat.fexp (fprec t) (femax t))
    (BinarySingleNaN.round_mode BinarySingleNaN.mode_NE)
    (FT2R a × FT2R b + FT2R s).

End GenFloat.