LAProof.accuracy_proofs.sum_model
From LAProof.accuracy_proofs Require Import preamble common.
Require Import Permutation.
Inductive sum_rel {A : Type} (default: A) (sum_op : A → A → A) : list A → A → Prop :=
| sum_rel_nil : sum_rel default sum_op [] default
| sum_rel_cons : ∀ l a s,
sum_rel default sum_op l s →
sum_rel default sum_op (a::l) (sum_op a s).
Definition sum_rel_R := @sum_rel R 0%R Rplus.
Inductive sum_any' {NAN: FPCore.Nans} {t}: ∀ (h: nat) (v: list (ftype t)) (s: ftype t), Prop :=
| Sum_Any_1: ∀ x, sum_any' O [x] x
| Sum_Any_split: ∀ n1 n2 al bl a b,
sum_any' n1 al a → sum_any' n2 bl b → sum_any' (S (Nat.max n1 n2)) (al++bl) (BPLUS a b)
| Sum_Any_perm: ∀ n al bl s, Permutation al bl → sum_any' n al s → sum_any' n bl s.
Inductive sum_any {NAN: FPCore.Nans} {t:type}: ∀ (h: nat) (v: list (ftype t)) (s: ftype t), Prop :=
| Sum_Any_None: sum_any O nil pos_zero
| Sum_Any_Some: ∀ n v s, sum_any' n v s → sum_any n v s.
Lemma sum_rel_sum_any: ∀ {NAN: FPCore.Nans} {t} z (v: list (ftype t)) s (Hz: iszero z),
sum_rel z BPLUS v s →
∃ s', feq s s' ∧ sum_any (Nat.pred (size v)) v s'.
Lemma sum_rel_R_abs :
∀ l s1 s2,
sum_rel_R l s1 → sum_rel_R (map Rabs l) s2 → s1 ≤ s2.
Lemma sum_rel_R_Rabs_pos :
∀ l s,
sum_rel_R (map Rabs l) s → 0 ≤ s.
Lemma sum_rel_R_Rabs_eq :
∀ l s,
sum_rel_R (map Rabs l) s → Rabs s = s.
Lemma sum_rel_R_Rabs :
∀ l s1 s2,
sum_rel_R l s1 → sum_rel_R (map Rabs l) s2 → Rabs s1 ≤ Rabs s2.
Lemma sum_rel_R_single :
∀ (a : R) (fs : R), sum_rel_R [a] fs → fs = a.
Lemma sum_rel_R_single' :
∀ (a : R) , sum_rel_R [a] a.
Lemma sum_rel_R_app_cons :
∀ l' l'' a s,
sum_rel_R (l' ++ l'') s →
sum_rel_R (l' ++ a :: l'') (a + s).
Lemma sum_rel_bound :
∀ (l : list R) (rs a: R)
(Hrs : sum_rel_R l rs)
(Hin : ∀ x, In x l → Rabs x ≤ a),
Rabs rs ≤ INR (size l) × a.
Lemma sum_rel_R_permute :
∀ (l l0: list R)
(Hper: Permutation l l0) (rs: R)
(Hrs: sum_rel_R l rs),
sum_rel_R l0 rs.
Lemma sum_rel_R_permute_t :
∀ (t: type) (l l0: list (ftype t))
(Hper: Permutation l l0) (rs: R)
(Hrs: sum_rel_R (map FT2R l) rs),
sum_rel_R (map FT2R l0) rs.
Definition sumR := foldr Rplus 0.
Lemma sumRabs_pos x :
0 ≤ sumR (map Rabs x).
Lemma sumRabs_Rabs x :
Rabs (sumR (map Rabs x)) = sumR (map Rabs x).
Lemma sumR_mult x a :
sumR x × a = sumR (map (Rmult a) x).
Lemma sumR_le_sumRabs x :
Rabs (sumR x) ≤ Rabs (sumR (map Rabs x)).
Lemma sumR_app_cons l' l'' a:
a + sumR (l' ++ l'') = sumR (l' ++ a :: l'').
Lemma sumR_permute :
∀ x x0 (Hper: Permutation x x0) ,
sumR x = sumR x0.
Lemma sumR_rev: ∀ l, sumR (rev l) = sumR l.
Lemma sum_rel_bound' :
∀ (t : type) (l : list (ftype t)) (rs a: R)
(Hrs : sum_rel_R (map FT2R l) rs)
(Hin : ∀ x, In x l → Rabs (FT2R x) ≤ a),
Rabs rs ≤ INR (size l) × a.
Lemma sum_rel_bound'' :
∀ (t : type) (l : list (ftype t)) (rs_abs a: R)
(Hrs : sum_rel_R (map Rabs (map FT2R l)) rs_abs)
(Hin : ∀ x, In x l → Rabs (FT2R x) ≤ a),
rs_abs ≤ INR (size l) × a.
Lemma sum_rel_R_fold : ∀ l rs,
sum_rel_R l rs → rs = sumR l.
Lemma sum_map_Rmult (l : list R) (s a: R):
sum_rel_R l s →
sum_rel_R (map (Rmult a) l) (a × s).
Section WithSTD.
Context {NAN: FPCore.Nans} {t : type}.
Definition sum_rel_Ft := @sum_rel (ftype t) neg_zero (BPLUS ).
Lemma sum_rel_Ft_single fs a:
Binary.is_finite fs = true →
sum_rel_Ft [a] fs → fs = a.
Lemma sum_rel_R_exists :
∀ (l : list (ftype t)) (fs : ftype t)
(Hfs : sum_rel_Ft l fs),
∃ rs, sum_rel_R (map FT2R l) rs.
Lemma sum_rel_R_abs_exists:
∀ (l : list (ftype t)) (fs : ftype t)
(Hfs : sum_rel_Ft l fs),
∃ rs, sum_rel_R (map Rabs (map FT2R l)) rs.
Lemma is_finite_in :
∀ (l : list (ftype t)) fs,
sum_rel_Ft l fs →
let e := @default_abs t in
let d := @default_rel t in
let ov := powerRZ 2 (femax t) in
Binary.is_finite fs = true →
∀ a, In a l → Binary.is_finite a = true.
Definition sumF := foldl(Basics.flip (@BPLUS _ t)) neg_zero.
Lemma sum_rel_Ft_fold : ∀ l fs,
sum_rel_Ft (rev l) fs → fs = sumF l.
subtract_loop is a variant on summation used in some implementations of Cholesky decomposition,
among other things. We should be able to prove an equivalence, of sorts, with sum_rel,
so that the accuracy theorem for sum_rel can apply here as well.
Definition subtract_loop: ∀ (c: ftype t) (al: list (ftype t)), ftype t := foldl BMINUS.
Lemma BMINUS_neg_zero: ∀ (c: ftype t), feq (BMINUS neg_zero (BOPP c)) c.
Lemma subtract_loop_congr1: ∀ (u v: ftype t) al,
feq u v → feq (subtract_loop u al) (subtract_loop v al).
Lemma BPLUS_neg_zero: ∀ (c: ftype t), feq (BPLUS c neg_zero) c.
Lemma BPLUS_comm: ∀ (x y: ftype t), feq (BPLUS x y) (BPLUS y x).
Lemma MINUS_PLUS_BOPP: ∀ x y: ftype t, feq (BMINUS x y) (BPLUS x (BOPP y)).
Lemma subtract_loop_sumR: ∀ (c: ftype t) (al: list (ftype t)),
feq (subtract_loop c al) (sumF (c :: map BOPP al)).
Lemma sum_rel_Ft_exists: ∀ (l: list (ftype t)), ∃ s, sum_rel_Ft l s.
Lemma subtract_loop_sum_any: ∀ (c: ftype t) (al: list (ftype t)),
∃ s, feq (subtract_loop c al) s ∧ sum_any (size al) (rev (c::map BOPP al)) s.
End WithSTD.
Lemma BMINUS_neg_zero: ∀ (c: ftype t), feq (BMINUS neg_zero (BOPP c)) c.
Lemma subtract_loop_congr1: ∀ (u v: ftype t) al,
feq u v → feq (subtract_loop u al) (subtract_loop v al).
Lemma BPLUS_neg_zero: ∀ (c: ftype t), feq (BPLUS c neg_zero) c.
Lemma BPLUS_comm: ∀ (x y: ftype t), feq (BPLUS x y) (BPLUS y x).
Lemma MINUS_PLUS_BOPP: ∀ x y: ftype t, feq (BMINUS x y) (BPLUS x (BOPP y)).
Lemma subtract_loop_sumR: ∀ (c: ftype t) (al: list (ftype t)),
feq (subtract_loop c al) (sumF (c :: map BOPP al)).
Lemma sum_rel_Ft_exists: ∀ (l: list (ftype t)), ∃ s, sum_rel_Ft l s.
Lemma subtract_loop_sum_any: ∀ (c: ftype t) (al: list (ftype t)),
∃ s, feq (subtract_loop c al) s ∧ sum_any (size al) (rev (c::map BOPP al)) s.
End WithSTD.