LAProof.accuracy_proofs.dot_acc_lemmas

From LAProof.accuracy_proofs Require Import preamble common
                                            dotprod_model
                                            float_acc_lems.

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

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

Lemma dotprod_forward_error_rel:
 ∀ (vF: seq (ftype t × ftype t))
            (fp : ftype t)
            (Hfp : dot_prod_rel vF fp)
            (Hfin: Binary.is_finite fp = true)
           (rp rp_abs : R)
           (Hrp : R_dot_prod_rel (map FR2 vF) rp)
           (Hra : R_dot_prod_rel (map Rabsp (map FR2 vF)) rp_abs),
  Rabs (FT2R fp - rp) ≤ g (size vF) × rp_abs + g1 (size vF) (size vF - 1).

End ForwardErrorRel1.

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

Variable (vF : list (ftype t × ftype t)).
Notation vR := (map FR2 vF).
Notation vR' := (map Rabsp (map FR2 vF)).

Variable (fp : ftype t).
Hypothesis Hfp : fma_dot_prod_rel vF fp.
Hypothesis Hfin: Binary.is_finite fp = true.

Variable (rp rp_abs : R).
Hypothesis Hrp : R_dot_prod_rel vR rp.
Hypothesis Hra : R_dot_prod_rel vR' rp_abs.

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

Lemma fma_dotprod_forward_error_rel:
  Rabs (FT2R fp - rp) ≤ g (size vF) × rp_abs + g1 (size vF) (size vF - 1).

End ForwardErrorRel2.

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

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

Variables (v1 v2 : list (ftype t)).
Hypothesis Hlen : size v1 = size v2.
Notation vF := (zip v1 v2).

Variable (fp : ftype t).
Hypothesis Hfp : dot_prod_rel vF fp.
Hypothesis Hfin: Binary.is_finite fp = true.

Notation neg_zero := (@common.neg_zero t).

Lemma dotprod_mixed_error_rel:
  ∃ (u : list R) (eta : R),
    size u = size v2 ∧
    R_dot_prod_rel (zip u (map FT2R v2)) (FT2R fp - eta) ∧
    (∀ n, (n < size v2)%nat → ∃ delta,
      nth 0 u n = FT2R (nth neg_zero v1 n) × (1 + delta) ∧ Rabs delta ≤ g (size v2)) ∧
    Rabs eta ≤ g1 (size v2) (size v2).

End MixedErrorRel1.

Section MixedErrorRel2.

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

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

Variables (v1 v2 : list (ftype t)).
Hypothesis Hlen : size v1 = size v2.
Notation vF := (zip v1 v2).

Variable (fp : ftype t).
Hypothesis Hfp : fma_dot_prod_rel vF fp.
Hypothesis Hfin: Binary.is_finite fp = true.

Notation neg_zero := (@common.neg_zero t).

Lemma fma_dotprod_mixed_error_rel:
  ∃ (u : list R) (eta : R),
    size u = size v1 ∧
    R_dot_prod_rel (zip u (map FT2R v2)) (FT2R fp - eta) ∧
    (∀ n, (n < size v2)%nat → ∃ delta,
      nth 0 u n = FT2R (nth neg_zero v1 n) × (1 + delta) ∧ Rabs delta ≤ g (size v2)) ∧
    Rabs eta ≤ g1 (size v2) (size v2 - 1).

End MixedErrorRel2.

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

Variables (v1 v2 : list (ftype t)).
Hypothesis (Hlen : size v1 = size v2).

Variable (fp : ftype t).
Hypothesis Hfp : dot_prod_rel (zip v1 v2) fp.
Hypothesis Hfin: Binary.is_finite fp = true.

Notation v1R := (map FT2R v1).

Variable (rp rp_abs : R).
Hypothesis Hrp : R_dot_prod_rel (map FR2 (zip v1 v2)) rp.
Hypothesis Hra : R_dot_prod_rel (map Rabsp (map FR2 (zip v1 v2))) rp_abs.

Notation g := (@common.g t).
Notation g1 := (@common.g1 t).
Notation nnzR := (nnzR v1R).

Lemma sparse_dotprod_forward_error_rel:
  Rabs (FT2R fp - rp) ≤ g nnzR × rp_abs + g1 nnzR (nnzR - 1).

End SparseErrorRel1.

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

Variables (v1 v2 : list (ftype t)).
Hypothesis (Hlen : size v1 = size v2).

Variable (fp : ftype t).
Hypothesis Hfp : fma_dot_prod_rel (zip v1 v2) fp.
Hypothesis Hfin: Binary.is_finite fp = true.

Notation v1R := (map FT2R v1).
Notation vR := (map FR2 (zip v1 v2)).
Notation vR' := (map Rabsp (map FR2 (zip v1 v2))).

Variable (rp rp_abs : R).
Hypothesis Hrp : R_dot_prod_rel vR rp.
Hypothesis Hra : R_dot_prod_rel vR' rp_abs.

Notation g := (@common.g t).
Notation g1 := (@common.g1 t).
Notation D := (@default_rel t).
Notation E := (@default_abs t).
Notation nnzR := (nnzR v1R).

Lemma sparse_fma_dotprod_forward_error:
  Rabs (FT2R fp - rp) ≤ g nnzR × rp_abs + g1 nnzR (nnzR - 1).

End SparseErrorRel2.