LAProof.accuracy_proofs.dotprod_model
From LAProof.accuracy_proofs Require Import preamble common float_acc_lems.
Require Import FunctionalExtensionality.
Require Import Permutation.
Definition dotprod {A} (mult plus: A → A → A) (zero : A) (v1 v2: list A):A :=
foldl (Basics.flip plus) zero (map (uncurry mult) (zip v1 v2)).
Lemma dotprod_nil_l :
∀ A (l : list A)
(mult plus : A → A → A) (zero : A), dotprod mult plus zero nil l = zero.
Lemma dotprod_nil_r :
∀ A (l : list A)
(mult plus : A → A → A) (zero : A), dotprod mult plus zero l nil = zero.
Lemma dotprod_single :
∀ A (l : list A)
(mult plus : A → A → A) (zero a2: A)
(Hpz : ∀ y, plus y zero = y)
(Hmz : ∀ y, mult zero y = zero),
let a1 := nth zero l 0 in
dotprod mult plus zero l [a2] = mult a1 a2.
Section DotProdFloat.
Context {NAN : FPCore.Nans} {t : type}.
Definition dotprodF : list (ftype t) → list (ftype t) → ftype t :=
dotprod BMULT BPLUS pos_zero.
Inductive dot_prod_rel :
list (ftype t × ftype t) → ftype t → Prop :=
| dot_prod_rel_nil : dot_prod_rel nil pos_zero
| dot_prod_rel_cons : ∀ l (xy : ftype t × ftype t) s,
dot_prod_rel l s →
dot_prod_rel (xy::l) (BPLUS (BMULT (fst xy) (snd xy)) s).
Inductive dotprod_any' : ∀ (h: nat) (v: list (ftype t × ftype t)) (s: ftype t), Prop :=
| Dotprod_Any_1: ∀ x, dotprod_any' O [x] (BMULT (fst x) (snd x))
| Dotprod_Any_split: ∀ n1 n2 al bl a b,
dotprod_any' n1 al a → dotprod_any' n2 bl b → dotprod_any' (S (Nat.max n1 n2)) (al++bl) (BPLUS a b)
| Dotprod_Any_perm: ∀ n al bl s, Permutation al bl → dotprod_any' n al s → dotprod_any' n bl s.
Inductive dotprod_any : ∀ (h: nat) (v: list (ftype t × ftype t)) (s: ftype t), Prop :=
| Dotprod_Any_None: dotprod_any O nil pos_zero
| Dotprod_Any_Some: ∀ n v s, dotprod_any' n v s → dotprod_any n v s.
Lemma dotprod_rel_dotprod_any: ∀ (z: ftype t) (v: list (ftype t × ftype t)) s (Hz: iszero z),
Forall (fun xy ⇒ Binary.is_finite (BMULT (fst xy) (snd xy))) v →
dot_prod_rel v s →
∃ s', feq s s' ∧ dotprod_any (Nat.pred (size v)) v s'.
Lemma dotprodF_rel_fold_right :
∀ (v1 v2: list (ftype t)),
dot_prod_rel (rev (zip v1 v2)) (dotprodF v1 v2).
End DotProdFloat.
Section DotProdFMA.
Context {NAN : FPCore.Nans} {t : type}.
Definition fma_dotprod (v1 v2: list (ftype t)) : ftype t :=
foldl (fun s x12 ⇒ BFMA (fst x12) (snd x12) s) pos_zero (zip v1 v2).
Inductive fma_dot_prod_rel :
list (ftype t × ftype t) → ftype t → Prop :=
| fma_dot_prod_rel_nil : fma_dot_prod_rel nil (Zconst t 0)
| fma_dot_prod_rel_cons : ∀ l (xy : ftype t × ftype t) s,
fma_dot_prod_rel l s →
fma_dot_prod_rel (xy::l) (BFMA (fst xy) (snd xy) s).
Lemma fma_dot_prod_rel_fold_right :
∀ (v1 v2: list (ftype t)),
fma_dot_prod_rel (rev (zip v1 v2)) (fma_dotprod v1 v2).
End DotProdFMA.
Section RealDotProd.
Definition dotprodR: ∀ l1 l2 : seq R, R:=
dotprod Rmult Rplus 0%R.
Inductive R_dot_prod_rel : list (R × R) → R → Prop :=
| R_dot_prod_rel_nil : R_dot_prod_rel nil 0%R
| R_dot_prod_rel_cons : ∀ l xy s,
R_dot_prod_rel l s →
R_dot_prod_rel (xy::l) (fst xy × snd xy + s).
Lemma R_dot_prod_rel_eq :
∀ l a b
(Ha: R_dot_prod_rel l a)
(Hb: R_dot_prod_rel l b), a = b.
Definition Rabsp p : R × R := (Rabs (fst p), Rabs (snd p)).
Definition FR2 {t: type} (x12: ftype t × ftype t) := (FT2R (fst x12), FT2R (snd x12)).
Lemma FT2R_FR2 t :
∀ a a0 : ftype t, (FT2R a, FT2R a0) = FR2 (a, a0).
Definition sum_fold: list R → R := foldr Rplus 0%R.
Lemma dotprodR_nil_l u:
dotprodR nil u = 0.
Lemma dotprodR_nil_r u:
dotprodR u nil = 0.
Lemma flip_Rplus: Basics.flip Rplus = Rplus.
Lemma Rplus_rewrite : (fun x y ⇒ x + y)%Re = Rplus.
Lemma sum_rev l: sum_fold l = sum_fold (rev l).
Lemma dotprodR_rel :
∀ (v1 v2: list R) ,
R_dot_prod_rel (zip v1 v2) (dotprodR v1 v2).
Lemma dotprodR_rel_inj: ∀ l s1 s2,
R_dot_prod_rel l s1 → R_dot_prod_rel l s2 → s1=s2.
Lemma dotprodR_rev : ∀ (v1 v2: list R) ,
size v1 = size v2 →
dotprodR v1 (rev v2) = dotprodR (rev v1) v2.
Lemma map_FR2_zip: ∀ {t} (v1 v2: seq (ftype t)),
map FR2 (zip v1 v2) = zip (map FT2R v1) (map FT2R v2).
Lemma map_Rabsp_zip: ∀ (v1 v2: seq R),
map Rabsp (zip v1 v2) = zip (map Rabs v1) (map Rabs v2).
Lemma R_dot_prod_rel_fold_right t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map FR2 (zip v1 v2)) in
R_dot_prod_rel (rev (map FR2 (zip v1 v2))) (sum_fold prods).
Lemma R_dot_prod_rel_fold_right' t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map FR2 (zip v1 v2)) in
R_dot_prod_rel (rev (map FR2 (zip v1 v2))) (dotprodR (map FT2R v1) (map FT2R v2)).
Lemma R_dot_prod_rel_fold_right_Rabs t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map Rabsp (map FR2 (zip v1 v2))) in
R_dot_prod_rel (rev (map Rabsp (map FR2 (zip v1 v2)))) (sum_fold prods).
Lemma R_dot_prod_rel_fold_right_Rabs' t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map Rabsp (map FR2 (zip v1 v2))) in
R_dot_prod_rel (rev (map Rabsp (map FR2 (zip v1 v2)))) (dotprodR (map Rabs (map FT2R v1)) (map Rabs (map FT2R v2))).
Lemma R_dot_prod_rel_single rs a:
R_dot_prod_rel [::a] rs → rs = (fst a × snd a).
Lemma R_dot_prod_rel_single' a:
R_dot_prod_rel [::a] (fst a × snd a).
Lemma R_dot_prod_rel_Rabs_eq :
∀ l s,
R_dot_prod_rel (map Rabsp l) s → Rabs s = s.
Lemma dot_prod_sum_rel_R_Rabs :
∀ l s1 s2,
R_dot_prod_rel l s1 → R_dot_prod_rel (map Rabsp l) s2 → Rabs s1 ≤ Rabs s2.
Lemma dot_prod_zip_map_Rmult a u v r:
size u = size v →
R_dot_prod_rel (zip u v) r →
R_dot_prod_rel (zip (map (Rmult a) u) v) (a × r).
Lemma dotprod_rel_R_exists {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t)
(Hfp : dot_prod_rel l fp),
∃ rp, R_dot_prod_rel (map FR2 l) rp.
Lemma dotprod_rel_R_exists_fma {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t)
(Hfp : fma_dot_prod_rel l fp),
∃ rp, R_dot_prod_rel (map FR2 l) rp.
Lemma sum_rel_R_abs_exists_fma {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t)
(Hfp : fma_dot_prod_rel l fp),
∃ rp, R_dot_prod_rel (map Rabsp (map FR2 l)) rp.
Lemma dotprodR_rel_bound' :
∀ (t : type) (l : list (ftype t × ftype t)) (rp a: R)
(Ha : 0 ≤ a)
(Hrp : R_dot_prod_rel (map FR2 l) rp)
(Hin : ∀ x, In x l → Rabs (FT2R (fst x)) ≤ sqrt a ∧ Rabs (FT2R (snd x)) ≤ sqrt a),
Rabs rp ≤ INR (length l) × a.
Lemma dotprodR_rel_bound'' :
∀ (t : type) (l : list (ftype t × ftype t)) (rs_abs a: R)
(Ha : 0 ≤ a)
(Hrp : R_dot_prod_rel (map Rabsp (map FR2 l)) rs_abs)
(Hin : ∀ x, In x l → Rabs (FT2R (fst x)) ≤ sqrt a ∧ Rabs (FT2R (snd x)) ≤ sqrt a),
rs_abs ≤ INR (length l) × a.
End RealDotProd.
Section NonZeroDP.
Context {NAN: FPCore.Nans} {t : type}.
Variables (v1 v2 : list (ftype t)).
Hypothesis (Hlen : size v1 = size v2).
Notation v1R := (map FT2R v1).
Lemma Req_eq: ∀ x y, Req_bool x y = eq_op x y.
Lemma dot_prod_rel_nnzR :
∀
(fp : ftype t)
(Hfp : dot_prod_rel (zip v1 v2) fp)
(Hfin: Binary.is_finite fp = true),
nnzR v1R == 0%nat → FT2R fp = 0.
Lemma fma_dot_prod_rel_nnzR :
∀
(fp : ftype t)
(Hfp : fma_dot_prod_rel (zip v1 v2) fp)
(Hfin: Binary.is_finite fp = true),
nnzR v1R == 0%nat → FT2R fp = 0.
Lemma R_dot_prod_rel_nnzR :
∀
(rp : R)
(Hrp : R_dot_prod_rel (map FR2 (zip v1 v2)) rp),
nnzR v1R == 0%nat → rp = 0.
Lemma R_dot_prod_rel_nnzR_abs :
∀
(rp_abs : R)
(Hra : R_dot_prod_rel (map Rabsp (map FR2 (zip v1 v2))) rp_abs),
nnzR v1R == 0%nat → rp_abs = 0.
End NonZeroDP.
Require Import FunctionalExtensionality.
Require Import Permutation.
Definition dotprod {A} (mult plus: A → A → A) (zero : A) (v1 v2: list A):A :=
foldl (Basics.flip plus) zero (map (uncurry mult) (zip v1 v2)).
Lemma dotprod_nil_l :
∀ A (l : list A)
(mult plus : A → A → A) (zero : A), dotprod mult plus zero nil l = zero.
Lemma dotprod_nil_r :
∀ A (l : list A)
(mult plus : A → A → A) (zero : A), dotprod mult plus zero l nil = zero.
Lemma dotprod_single :
∀ A (l : list A)
(mult plus : A → A → A) (zero a2: A)
(Hpz : ∀ y, plus y zero = y)
(Hmz : ∀ y, mult zero y = zero),
let a1 := nth zero l 0 in
dotprod mult plus zero l [a2] = mult a1 a2.
Section DotProdFloat.
Context {NAN : FPCore.Nans} {t : type}.
Definition dotprodF : list (ftype t) → list (ftype t) → ftype t :=
dotprod BMULT BPLUS pos_zero.
Inductive dot_prod_rel :
list (ftype t × ftype t) → ftype t → Prop :=
| dot_prod_rel_nil : dot_prod_rel nil pos_zero
| dot_prod_rel_cons : ∀ l (xy : ftype t × ftype t) s,
dot_prod_rel l s →
dot_prod_rel (xy::l) (BPLUS (BMULT (fst xy) (snd xy)) s).
Inductive dotprod_any' : ∀ (h: nat) (v: list (ftype t × ftype t)) (s: ftype t), Prop :=
| Dotprod_Any_1: ∀ x, dotprod_any' O [x] (BMULT (fst x) (snd x))
| Dotprod_Any_split: ∀ n1 n2 al bl a b,
dotprod_any' n1 al a → dotprod_any' n2 bl b → dotprod_any' (S (Nat.max n1 n2)) (al++bl) (BPLUS a b)
| Dotprod_Any_perm: ∀ n al bl s, Permutation al bl → dotprod_any' n al s → dotprod_any' n bl s.
Inductive dotprod_any : ∀ (h: nat) (v: list (ftype t × ftype t)) (s: ftype t), Prop :=
| Dotprod_Any_None: dotprod_any O nil pos_zero
| Dotprod_Any_Some: ∀ n v s, dotprod_any' n v s → dotprod_any n v s.
Lemma dotprod_rel_dotprod_any: ∀ (z: ftype t) (v: list (ftype t × ftype t)) s (Hz: iszero z),
Forall (fun xy ⇒ Binary.is_finite (BMULT (fst xy) (snd xy))) v →
dot_prod_rel v s →
∃ s', feq s s' ∧ dotprod_any (Nat.pred (size v)) v s'.
Lemma dotprodF_rel_fold_right :
∀ (v1 v2: list (ftype t)),
dot_prod_rel (rev (zip v1 v2)) (dotprodF v1 v2).
End DotProdFloat.
Section DotProdFMA.
Context {NAN : FPCore.Nans} {t : type}.
Definition fma_dotprod (v1 v2: list (ftype t)) : ftype t :=
foldl (fun s x12 ⇒ BFMA (fst x12) (snd x12) s) pos_zero (zip v1 v2).
Inductive fma_dot_prod_rel :
list (ftype t × ftype t) → ftype t → Prop :=
| fma_dot_prod_rel_nil : fma_dot_prod_rel nil (Zconst t 0)
| fma_dot_prod_rel_cons : ∀ l (xy : ftype t × ftype t) s,
fma_dot_prod_rel l s →
fma_dot_prod_rel (xy::l) (BFMA (fst xy) (snd xy) s).
Lemma fma_dot_prod_rel_fold_right :
∀ (v1 v2: list (ftype t)),
fma_dot_prod_rel (rev (zip v1 v2)) (fma_dotprod v1 v2).
End DotProdFMA.
Section RealDotProd.
Definition dotprodR: ∀ l1 l2 : seq R, R:=
dotprod Rmult Rplus 0%R.
Inductive R_dot_prod_rel : list (R × R) → R → Prop :=
| R_dot_prod_rel_nil : R_dot_prod_rel nil 0%R
| R_dot_prod_rel_cons : ∀ l xy s,
R_dot_prod_rel l s →
R_dot_prod_rel (xy::l) (fst xy × snd xy + s).
Lemma R_dot_prod_rel_eq :
∀ l a b
(Ha: R_dot_prod_rel l a)
(Hb: R_dot_prod_rel l b), a = b.
Definition Rabsp p : R × R := (Rabs (fst p), Rabs (snd p)).
Definition FR2 {t: type} (x12: ftype t × ftype t) := (FT2R (fst x12), FT2R (snd x12)).
Lemma FT2R_FR2 t :
∀ a a0 : ftype t, (FT2R a, FT2R a0) = FR2 (a, a0).
Definition sum_fold: list R → R := foldr Rplus 0%R.
Lemma dotprodR_nil_l u:
dotprodR nil u = 0.
Lemma dotprodR_nil_r u:
dotprodR u nil = 0.
Lemma flip_Rplus: Basics.flip Rplus = Rplus.
Lemma Rplus_rewrite : (fun x y ⇒ x + y)%Re = Rplus.
Lemma sum_rev l: sum_fold l = sum_fold (rev l).
Lemma dotprodR_rel :
∀ (v1 v2: list R) ,
R_dot_prod_rel (zip v1 v2) (dotprodR v1 v2).
Lemma dotprodR_rel_inj: ∀ l s1 s2,
R_dot_prod_rel l s1 → R_dot_prod_rel l s2 → s1=s2.
Lemma dotprodR_rev : ∀ (v1 v2: list R) ,
size v1 = size v2 →
dotprodR v1 (rev v2) = dotprodR (rev v1) v2.
Lemma map_FR2_zip: ∀ {t} (v1 v2: seq (ftype t)),
map FR2 (zip v1 v2) = zip (map FT2R v1) (map FT2R v2).
Lemma map_Rabsp_zip: ∀ (v1 v2: seq R),
map Rabsp (zip v1 v2) = zip (map Rabs v1) (map Rabs v2).
Lemma R_dot_prod_rel_fold_right t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map FR2 (zip v1 v2)) in
R_dot_prod_rel (rev (map FR2 (zip v1 v2))) (sum_fold prods).
Lemma R_dot_prod_rel_fold_right' t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map FR2 (zip v1 v2)) in
R_dot_prod_rel (rev (map FR2 (zip v1 v2))) (dotprodR (map FT2R v1) (map FT2R v2)).
Lemma R_dot_prod_rel_fold_right_Rabs t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map Rabsp (map FR2 (zip v1 v2))) in
R_dot_prod_rel (rev (map Rabsp (map FR2 (zip v1 v2)))) (sum_fold prods).
Lemma R_dot_prod_rel_fold_right_Rabs' t :
∀ (v1 v2: list (ftype t)) ,
size v1 = size v2 →
let prods := map (uncurry Rmult) (map Rabsp (map FR2 (zip v1 v2))) in
R_dot_prod_rel (rev (map Rabsp (map FR2 (zip v1 v2)))) (dotprodR (map Rabs (map FT2R v1)) (map Rabs (map FT2R v2))).
Lemma R_dot_prod_rel_single rs a:
R_dot_prod_rel [::a] rs → rs = (fst a × snd a).
Lemma R_dot_prod_rel_single' a:
R_dot_prod_rel [::a] (fst a × snd a).
Lemma R_dot_prod_rel_Rabs_eq :
∀ l s,
R_dot_prod_rel (map Rabsp l) s → Rabs s = s.
Lemma dot_prod_sum_rel_R_Rabs :
∀ l s1 s2,
R_dot_prod_rel l s1 → R_dot_prod_rel (map Rabsp l) s2 → Rabs s1 ≤ Rabs s2.
Lemma dot_prod_zip_map_Rmult a u v r:
size u = size v →
R_dot_prod_rel (zip u v) r →
R_dot_prod_rel (zip (map (Rmult a) u) v) (a × r).
Lemma dotprod_rel_R_exists {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t)
(Hfp : dot_prod_rel l fp),
∃ rp, R_dot_prod_rel (map FR2 l) rp.
Lemma dotprod_rel_R_exists_fma {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t)
(Hfp : fma_dot_prod_rel l fp),
∃ rp, R_dot_prod_rel (map FR2 l) rp.
Lemma sum_rel_R_abs_exists_fma {NAN : FPCore.Nans} {t : type} :
∀ (l : list (ftype t × ftype t)) (fp : ftype t)
(Hfp : fma_dot_prod_rel l fp),
∃ rp, R_dot_prod_rel (map Rabsp (map FR2 l)) rp.
Lemma dotprodR_rel_bound' :
∀ (t : type) (l : list (ftype t × ftype t)) (rp a: R)
(Ha : 0 ≤ a)
(Hrp : R_dot_prod_rel (map FR2 l) rp)
(Hin : ∀ x, In x l → Rabs (FT2R (fst x)) ≤ sqrt a ∧ Rabs (FT2R (snd x)) ≤ sqrt a),
Rabs rp ≤ INR (length l) × a.
Lemma dotprodR_rel_bound'' :
∀ (t : type) (l : list (ftype t × ftype t)) (rs_abs a: R)
(Ha : 0 ≤ a)
(Hrp : R_dot_prod_rel (map Rabsp (map FR2 l)) rs_abs)
(Hin : ∀ x, In x l → Rabs (FT2R (fst x)) ≤ sqrt a ∧ Rabs (FT2R (snd x)) ≤ sqrt a),
rs_abs ≤ INR (length l) × a.
End RealDotProd.
Section NonZeroDP.
Context {NAN: FPCore.Nans} {t : type}.
Variables (v1 v2 : list (ftype t)).
Hypothesis (Hlen : size v1 = size v2).
Notation v1R := (map FT2R v1).
Lemma Req_eq: ∀ x y, Req_bool x y = eq_op x y.
Lemma dot_prod_rel_nnzR :
∀
(fp : ftype t)
(Hfp : dot_prod_rel (zip v1 v2) fp)
(Hfin: Binary.is_finite fp = true),
nnzR v1R == 0%nat → FT2R fp = 0.
Lemma fma_dot_prod_rel_nnzR :
∀
(fp : ftype t)
(Hfp : fma_dot_prod_rel (zip v1 v2) fp)
(Hfin: Binary.is_finite fp = true),
nnzR v1R == 0%nat → FT2R fp = 0.
Lemma R_dot_prod_rel_nnzR :
∀
(rp : R)
(Hrp : R_dot_prod_rel (map FR2 (zip v1 v2)) rp),
nnzR v1R == 0%nat → rp = 0.
Lemma R_dot_prod_rel_nnzR_abs :
∀
(rp_abs : R)
(Hra : R_dot_prod_rel (map Rabsp (map FR2 (zip v1 v2))) rp_abs),
nnzR v1R == 0%nat → rp_abs = 0.
End NonZeroDP.