CoRN.reals.fast.CRsum

Require Import CRArith.
Require Import List.
Require Import Qmetric.
Require Import Qring.
Require Import Qauto.
Require Import CornTac.

Open Local Scope Q_scope.

Definition CRsum_list_raw (l:list CR) (e:QposInf) : Q :=
fold_left Qplus
match l with
| nil => nil
| cons h t =>
  let e' := QposInf_mult (1#(P_of_succ_nat (length t)))%Qpos e in
   (map (fun x => approximate x e') l)
end
0.

Lemma CRsum_list_prf : forall l, is_RegularFunction (CRsum_list_raw l).

Definition CRsum_list (l:list CR) : CR := Build_RegularFunction (CRsum_list_prf l).

Lemma CRsum_correct : forall l, (CRsum_list l == fold_right (fun x y => x + y) 0 l)%CR.