proposition: Lemma CRsum_correct : forall l, (CRsum_list l == fold_right (fun x y => x + y) 0 l)%CR.
proof: Proof. induction l. apply regFunEq_equiv, regFunEq_e; intros e. apply ball_refl. apply (Qpos_nonneg (e+e)). simpl (fold_right (fun x y : CR => (x + y)%CR) 0%CR (a :: l)). rewrite <- IHl. clear -l. apply regFunEq_equiv, regFunEq_e; intros e. simpl. unfold Cap_raw. simpl. unfold CRsum_list_raw. simpl. destruct l; simpl. rewrite Qplus_0_l, Qplus_0_r. setoid_replace (proj1_sig e+proj1_sig e) with (proj1_sig ((1 # 1) *e + (1 # 2) * e + (1 # 2) * e))%Qpos by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). change (Qball (proj1_sig ((1 # 1) * e + (1 # 2) * e + (1 # 2) * e)%Qpos) (approximate a ((1 # 1) * e)%Qpos) (approximate a ((1 # 2) * e)%Qpos)). apply ball_weak. apply Qpos_nonneg. apply regFun_prf. set (n:= (@length (RegularFunction Qball) l)). cut (forall (z1:Q) (e3 e5 e1 e2 e4 e6:Qpos) (z2 z3:Q), ball (proj1_sig e5) z1 z2 -> (z3 == approximate a e3 + z1) -> (proj1_sig e1*(Z.of_nat n#1) + proj1_sig e2*(Z.of_nat n#1) +proj1_sig e3 + proj1_sig e4 + proj1_sig e5 <= proj1_sig e6) -> Qball (proj1_sig e6) (fold_left Qplus (map (fun x : RegularFunction Qball => approximate x e1) l) z3) (approximate a e4 + fold_left Qplus (map (fun x : RegularFunction Qball => approximate x e2) l) z2)). { intros H. apply (H (approximate m ((1 # Pos.succ (P_of_succ_nat n)) * e)%Qpos) ((1 # Pos.succ (P_of_succ_nat n)) * e)%Qpos ((1 # Pos.succ (P_of_succ_nat n)) * e + (1 # P_of_succ_nat n) * ((1 # 2) * e))%Qpos _ _ _ (e+e)%Qpos). 2: rewrite Qplus_0_l; reflexivity. pose proof (Qplus_0_l (approximate m ((1 # Pos.of_succ_nat n) * ((1 # 2) * e))%Qpos)). apply Qball_0 in H0. rewrite H0. apply regFun_prf. simpl. apply (Qle_trans _ ((1 # Pos.succ (P_of_succ_nat n)) * ((2#1)+(Z.of_nat n#1)) *proj1_sig e + ((1 # P_of_succ_nat n) * ((1#1) + (Z.of_nat n#1)) * ((1 # 2) * proj1_sig e) + (1 # 2) * proj1_sig e))). ring_simplify; apply Qle_refl. setoid_replace ((1 # Pos.succ (Pos.of_succ_nat n)) * ((2#1) + (Z.of_nat n#1))) with (1#1)%Q. setoid_replace ((1 # Pos.of_succ_nat n) * ((1#1) + (Z.of_nat n#1))) with (1#1)%Q. field_simplify. setoid_replace (8 # 4) with (2#1) by reflexivity. apply Qle_refl. unfold Qmult, inject_Z, Qplus, Qeq, Qnum, Qden. ring_simplify. rewrite Pos.mul_1_r. unfold canonical_names.equiv, stdlib_rationals.Q_eq. rewrite Z.mul_1_l, Z.mul_1_l, Z.mul_1_r, Z.add_comm. rewrite <- Z.P_of_succ_nat_Zplus. unfold Qeq; simpl. rewrite Pos.mul_1_r. reflexivity. unfold canonical_names.equiv, stdlib_rationals.Q_eq. unfold Qmult, inject_Z, Qplus, Qeq, Qnum, Qden. ring_simplify. rewrite Pos.mul_1_r. rewrite <- SuccNat2Pos.inj_succ. rewrite Z.P_of_succ_nat_Zplus. replace (S n) with (1+n)%nat by reflexivity. rewrite Nat2Z.inj_add. rewrite (Z.add_comm 1). rewrite <- Z.add_assoc. reflexivity. } unfold n. clear n. induction l; intros z1 e3 e5 e1 e2 e4 e6 z2 z3 Hz H0 H. simpl in *. ring_simplify in H. ring_simplify. apply Qball_0 in H0. rewrite -> H0. unfold Qball. unfold QAbsSmall. setoid_replace (approximate a e3 + z1 - (approximate a e4 + z2)) with ((approximate a e3 - approximate a e4) + (z1 - z2)) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). pose proof (@ball_weak_le Q_as_MetricSpace (proj1_sig e3 + proj1_sig e4 + proj1_sig e5) (proj1_sig e6) (approximate a e3 - approximate a e4 + (z1 - z2)) 0). simpl in H1. unfold Qball, QAbsSmall, Qminus in H1. rewrite Qplus_0_r in H1. apply H1. exact H. apply QAbsSmall_plus; auto. apply (regFun_prf a). simpl. apply (IHl (z1 + approximate a0 e1) e3 (e5 + (e1 + e2))%Qpos). simpl. unfold Qball. unfold QAbsSmall. setoid_replace (z1 + approximate a0 e1 - (z2 + approximate a0 e2)) with ((z1 - z2) + (approximate a0 e1 - approximate a0 e2)) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; simpl; ring). apply QAbsSmall_plus. auto. apply (regFun_prf a0). rewrite -> H0. simpl; ring. simpl. simpl in H. set (n:= (@length (RegularFunction Qball) l)) in *. change (Zpos (P_of_succ_nat n)) with (Z_of_nat (1+n)) in H. rewrite inj_plus in H. refine (Qle_trans _ _ _ _ H). clear H. setoid_replace (Z.of_nat 1 + Z.of_nat n # 1)%Q with ((1#1) + (Z.of_nat n # 1)). ring_simplify. apply Qle_refl. unfold canonical_names.equiv, stdlib_rationals.Q_eq. unfold Qeq, Qplus, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r, Z.mul_1_r, Z.mul_1_r. reflexivity. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.reals.fast.CRArith CoRN.stdlib_omissions.List CoRN.model.metric2.Qmetric