LAProof.accuracy_proofs.fma_is_finite

From LAProof.accuracy_proofs Require Import preamble common dotprod_model sum_model
                                            float_acc_lems dot_acc_lemmas sum_acc.

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

Definition fmax := bpow Zaux.radix2 (femax t).

Lemma is_finite_fma_no_overflow' :
  ∀ (x y z: ftype t)
  (Hfinx:Binary.is_finite x = true)
  (Hfiny:Binary.is_finite y = true)
  (Hfinz:Binary.is_finite z = true)
  (Hov : @fma_no_overflow t (FT2R x) (FT2R y) (FT2R z)),
Binary.is_finite (BFMA x y z) = true.

Definition fun_bnd (t : type) (n : nat) :=
let x := (fmax - @default_abs t) / (1 + @default_rel t) - @g1 t n (n-1) in
let y := 1 / (1 + INR n × (@g t (n - 1) + 1)) in x × y.

Lemma rdiv_lt (a b: R) :
  0 < b → 0 < a → b < a → / a < / b.

Lemma rdiv_le (a b: R) :
  0 < b → 0 < a → b ≤ a → / a ≤ / b.

Lemma rdiv_mult_eq :
∀ a b, b ≠ 0 → a/b = a × (1/b) .

Lemma Rminus_le_minus a b c :
 b ≤ c → a - c ≤ a - b.

Lemma Rminus_lt_minus a b c :
 b < c → a - c < a - b.

Lemma defualt_abs_le_fmax :
@default_abs t ≤ fmax.

Lemma bpow_femax_lb :
4 ≤ bpow Zaux.radix2 (femax t).

Lemma bpow_fprec_lb :
2 ≤ bpow Zaux.radix2 (fprec t).

Lemma default_abs_ub :
@default_abs t ≤ 1.

Lemma default_rel_ub :
@default_rel t ≤ 1.

Lemma fun_bnd_pos_1 :
∀ n
(Hn : @g1 t (n + 1) n ≤ fmax ),
0 ≤ (fmax - @default_abs t) / (1 + @default_rel t) - @g1 t n (n-1).

Lemma fun_bnd_le (n : nat) :
∀ (Hn : @g1 t (S n + 1) (S n) ≤ fmax),
fun_bnd t (S n) ≤ fun_bnd t n.

Lemma length_split {A : Type} (l : list (A × A)) :
length (fst (List.split l)) = length (snd (List.split l)).

Lemma fun_bound_pos n :
∀ (Hn : @g1 t (n + 1) n ≤ fmax),
0 ≤ fun_bnd t n.

Lemma combine_split {A : Type} (l : list (A × A)) :
combine (fst (List.split l)) (snd (List.split l)) = l.

Lemma finite_sum_from_bounded :
  ∀ (v1 v2: list (ftype t))
  (fp : ftype t)
  (Hfp: fma_dot_prod_rel (List.combine v1 v2) fp)
  (Hn : @g1 t (S (length (List.combine v1 v2)) + 1) (S (length (List.combine v1 v2))) ≤ fmax ),
  (∀ x, In x (List.combine v1 v2) →
    Binary.is_finite (fst x) = true ∧
    Binary.is_finite (snd x) = true ∧
    Rabs (FT2R (fst x)) < sqrt (fun_bnd t (length (List.combine v1 v2))) ∧
    Rabs (FT2R (snd x)) < sqrt (fun_bnd t (length (List.combine v1 v2))))->
  Binary.is_finite fp = true.
End NAN.