LAProof.accuracy_proofs.sum_model

Floating-Point Summation: Functional Models and Equivalences

This file defines and relates several functional models for floating-point summation of lists. It provides both real-valued and floating-point relational specifications of summation, as well as a non-deterministic "any-order" floating-point summation predicate. The key contributions are:

sum_rel: A general inductive relation specifying summation over a list given a default element and a binary operation. Instantiated to both real (sum_rel_R) and floating-point (sum_rel_Ft) arithmetic.
sum_any', sum_any: An inductive predicate capturing floating-point summation in any order and any binary tree structure, modulo permutation. This is useful for reasoning about implementations that reorder or restructure summation for efficiency.
sumR: A fold-based functional definition of real summation, shown equivalent to sum_rel_R.
sumF: A fold-based functional definition of floating-point summation, shown equivalent to sum_rel_Ft.

Key lemmas include:

sum_rel_sum_any: Every sum_rel summation can be realized as a sum_any summation (up to floating-point equality feq).
sum_rel_R_abs, sum_rel_R_Rabs: Bounds on the absolute value of a real sum in terms of the sum of absolute values of its elements.
sum_rel_bound, sum_rel_bound', sum_rel_bound'': Uniform bounds on the magnitude of a real sum given elementwise bounds.
sum_rel_R_permute, sumR_permute: Summation is invariant under permutation of the input list.
subtract_loop_sum_any: The subtraction loop idiom (used in, e.g., Cholesky decomposition implementations) can be related to sum_any, enabling accuracy theorems for sum_rel to transfer to subtraction loops.

From LAProof.accuracy_proofs Require Import preamble common float_acc_lems.
Require Import Permutation.

General Summation Relation

sum_rel default sum_op l s holds when s is the result of folding sum_op over the list l from the right, starting from default . The empty list yields default , and a cons a :: l yields sum_op a s where s is the sum of l .

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).

sum_rel_R is sum_rel instantiated to real-number addition.

Definition sum_rel_R := @sum_rel R 0%R Rplus.

Any-Order Floating-Point Summation

sum_any' h v s captures the idea that a list v of floating-point values can be summed in any binary tree structure of depth at most h , up to reordering. The constructors are:

Sum_Any_1: A singleton list trivially sums to its element.
Sum_Any_split: Two sublists can be summed independently and their results combined with BPLUS.
Sum_Any_perm: The summation result is invariant under permutation of the input list.

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.

sum_any h v s extends sum_any' to handle the empty list, which sums to pos_zero .

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.

Equivalence Between sum_rel and sum_any

Every sum_rel floating-point summation (starting from a zero value) can be realized as a sum_any summation, up to floating-point equality. The height of the sum_any tree is Nat.pred (size v) .

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'.

Bounds via Absolute Value Summation

A real sum is bounded above by the sum of absolute values of its elements.

Lemma sum_rel_R_abs :
  ∀ l s1 s2,
    sum_rel_R l s1 →
    sum_rel_R (map Rabs l) s2 →
    s1 ≤ s2.

The sum of absolute values is non-negative.

Lemma sum_rel_R_Rabs_pos :
  ∀ l s,
    sum_rel_R (map Rabs l) s →
    0 ≤ s.

The sum of absolute values equals its own absolute value (i.e., it is non-negative, so Rabs s = s).

Lemma sum_rel_R_Rabs_eq :
  ∀ l s,
    sum_rel_R (map Rabs l) s →
    Rabs s = s.

The absolute value of any real sum is bounded by the sum of absolute values: Rabs s1 ≤ Rabs s2 when s2 is the sum of Rabs applied elementwise to l .

Lemma sum_rel_R_Rabs :
  ∀ l s1 s2,
    sum_rel_R l s1 →
    sum_rel_R (map Rabs l) s2 →
    Rabs s1 ≤ Rabs s2.

Singleton Summation Lemmas

A sum_rel_R derivation for a singleton list determines the sum uniquely.

Lemma sum_rel_R_single :
  ∀ (a : R) (fs : R),
    sum_rel_R [a] fs →
    fs = a.

A real value is the sum_rel_R of its own singleton list.

Lemma sum_rel_R_single' :
∀ (a : R),
sum_rel_R [a] a.

Permutation Invariance

Inserting an element into an arbitrary position in the middle of a split list preserves the sum_rel_R sum (with the element added).

Lemma sum_rel_R_app_cons :
  ∀ l' l'' a s,
    sum_rel_R (l' ++ l'') s →
    sum_rel_R (l' ++ a :: l'') (a + s).

sum_rel_R is invariant under list permutation.

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.

sum_rel_R over mapped floating-point values is invariant under permutation of the floating-point list.

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.

Uniform Bound on Sum Magnitude

Given a pointwise bound a on the absolute values of list elements, the magnitude of the sum is bounded by INR (size l) * a .

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.

sumR: Functional Real Summation

sumR is a computable fold-right definition of real summation.

Definition sumR := foldr Rplus 0.

The sum of absolute values via sumR is non-negative.

Lemma sumRabs_pos :
∀ x,
0 ≤ sumR (map Rabs x).

The absolute value of sumR of absolute values equals itself.

Lemma sumRabs_Rabs :
∀ x,
Rabs (sumR (map Rabs x)) = sumR (map Rabs x).

Scalar multiplication distributes over sumR.

Lemma sumR_mult :
∀ x a,
sumR x × a = sumR (map (Rmult a) x).

The absolute value of a real sum is bounded by the sum of absolute values.

Lemma sumR_le_sumRabs :
∀ x,
Rabs (sumR x) ≤ Rabs (sumR (map Rabs x)).

Inserting an element at an arbitrary position in a split list preserves the sumR value (with that element added).

Lemma sumR_app_cons :
∀ l' l'' a,
a + sumR (l' ++ l'') = sumR (l' ++ a :: l'').

sumR is invariant under list permutation.

Lemma sumR_permute :
  ∀ x x0
         (Hper : Permutation x x0),
    sumR x = sumR x0.

sumR is invariant under list reversal.

Lemma sumR_rev :
∀ l,
sumR (rev l) = sumR l.

Uniform Bounds on Floating-Point Sums via Real Arithmetic

Bound on sum_rel_R over FT2R-mapped floating-point lists, given a pointwise bound on Rabs (FT2R x).

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.

Bound on the sum of absolute values of FT2R-mapped floating-point list elements, given a pointwise bound.

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.

sum_rel_R and sumR agree: a sum_rel_R derivation yields the same value as sumR.

Lemma sum_rel_R_fold :
  ∀ l rs,
    sum_rel_R l rs →
    rs = sumR l.

Scalar multiplication distributes over sum_rel_R: if l sums to s , then map (Rmult a) l sums to a * s .

Lemma sum_map_Rmult :
  ∀ (l : list R) (s a : R),
    sum_rel_R l s →
    sum_rel_R (map (Rmult a) l) (a × s).

Floating-Point Summation Instances and Properties

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

sum_rel_Ft is sum_rel instantiated to floating-point addition with default value neg_zero .

Definition sum_rel_Ft := @sum_rel (ftype t) neg_zero BPLUS.

For a finite floating-point value fs , a sum_rel_Ft derivation for a singleton list determines the sum uniquely.

Lemma sum_rel_Ft_single :
  ∀ (fs a : ftype t),
    Binary.is_finite fs = true →
    sum_rel_Ft [a] fs →
    fs = a.

For any floating-point list and sum_rel_Ft derivation, there exists a corresponding real-valued sum under sum_rel_R.

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.

For any floating-point list and sum_rel_Ft derivation, there exists a corresponding sum of absolute values under sum_rel_R.

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.

If the result fs of a sum_rel_Ft computation is finite, then every element of the input list is also finite.

Lemma is_finite_in :
  ∀ (l : list (ftype t)) (fs : ftype t),
    sum_rel_Ft l fs →
    Binary.is_finite fs = true →
    ∀ a, In a l → Binary.is_finite a = true.

sumF is a computable fold-left definition of floating-point summation, accumulating with BPLUS from neg_zero .

Definition sumF := foldl (Basics.flip (@BPLUS _ t)) neg_zero.

sum_rel_Ft over a reversed list agrees with sumF on the original list.

Lemma sum_rel_Ft_fold :
  ∀ l fs,
    sum_rel_Ft (rev l) fs →
    fs = sumF l.

Subtraction Loop

The subtraction loop foldl BMINUS c al (used in, e.g., Cholesky decomposition) is floating-point equal to sumF (c :: map BOPP al) , i.e., summing c followed by the negations of al . This enables accuracy theorems for sum_rel to transfer to subtraction-loop implementations.

Lemma subtract_loop_sumR :
∀ (c : ftype t) (al : list (ftype t)),
feq (foldl BMINUS c al) (sumF (c :: map BOPP al)).

Every floating-point list has at least one sum_rel_Ft derivation.

Lemma sum_rel_Ft_exists :
∀ (l : list (ftype t)),
∃ s , sum_rel_Ft l s.

The subtraction loop foldl BMINUS c al can be related to sum_any, establishing that it falls within the framework of any-order summation. The resulting sum_any tree has height size al and input list rev (c :: map BOPP al) .

Lemma subtract_loop_sum_any :
  ∀ (c : ftype t) (al : list (ftype t)),
    ∃ s ,
      feq (foldl BMINUS c al) s ∧
      sum_any (size al) (rev (c :: map BOPP al)) s.

End WithSTD.