proposition: Theorem sum_invariant : forall prec p f, invariant f p -> valid f IBu IBv (sum prec p).
proof: Proof. intros prec p f. unfold sum, invariant, valid. rewrite ptree_fold_correct. generalize (ptree_to_list p). clear p. intros p. assert (H: (I.convert I.zero <> Inan -> all (fun r => match r with | Piece ur vr _ => ex_RInt_gen f (convert ur) (convert vr) end) nil) /\ contains (I.convert I.zero) (Xreal (exact_sum f nil))). simpl. apply (conj (fun _ => I)). rewrite I.zero_correct. split ; apply Rle_refl. change p with (nil ++ p) at 1 2. intros [Hp [qh [qt [Hq Iq]]]]. revert Hq Hp H. generalize (@nil piece) I.zero. induction p as [|h t IH] ; simpl ; intros l s Hq Hl [H1 H2]. - clear Hl. rewrite app_nil_r in Hq. unfold exact_sum in H2. rewrite fold_right_permut with (2 := Hq) in H2 by (intros ; ring). case_eq (I.convert s) ; [intros Hs | intros sl su Hs]. easy. cut (ex_RInt_gen f uf vf /\ RInt_gen f uf vf = exact_sum f (qh :: qt)). intros [H3 H4]. split. intros _. apply H3. rewrite H4. now rewrite <- Hs. assert (H1': all (fun r => match r with | Piece ur vr _ => ex_RInt_gen f (convert ur) (convert vr) end) (qh :: qt)). apply all_permut with (2 := Hq). apply H1. now rewrite Hs. clear -Iq H1' Fuf Fvf. revert qh Iq H1'. change uf with (convert IBu). generalize IBu. induction qt as [|qh qt IH] ; simpl. intros x [u v _] [-> ->] [H _]. apply (conj H). apply eq_sym, Rplus_0_l. intros x [u v _] [-> H6] [H1 H2]. destruct v as [| |x] ; try easy. destruct (IH _ _ H6 H2) as [H7 H8]. assert (H9 := ex_RInt_gen_Chasles _ _ H1 H7). assert (H5 := RInt_gen_Chasles _ _ H1 H7). clear IH H1 H2 H6 H7. apply (conj H9). simpl in H8. rewrite <- H5, <- H8. apply Rplus_comm. - eapply permut_trans in Hq. 2: apply permut_insert. destruct h as [ur' vr' i]. eapply all_permut in Hl. 2: apply permut_sym, permut_insert. apply (IH (_ :: l) (I.add prec s i) Hq Hl). destruct Hl as [H3 _]. clear -H1 H2 H3. split. intros H'. split. apply H3. contradict H'. now apply I.add_propagate_r. apply H1. contradict H'. now apply I.add_propagate_l. simpl. apply J.add_correct. apply H2. apply H3. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority