proposition: Theorem diff_refining_correct : forall prec f f' fi fi', I.extension f fi -> I.extension f' fi' -> Xderive f f' -> I.extension f (fun b => diff_refining prec b (fi b) (fi' b) fi).
proof: Proof. intros prec f f' fi fi' Hf Hf' Hd xi x Hx. unfold diff_refining. case_eq (I.convert xi) ; intros. assert (contains (I.convert (fi' xi)) Xnan). replace Xnan with (f' Xnan). apply Hf'. now rewrite H. generalize (Hd Xnan). now case (f' Xnan) ; intros. generalize (I.sign_large_correct (fi' xi)). case (I.sign_large (fi' xi)) ; intro. now assert (H2 := H1 _ H0). now assert (H2 := proj1 (H1 _ H0)). now assert (H2 := proj1 (H1 _ H0)). clear H1. generalize (I.bounded_correct (fi' xi)). case (I.bounded (fi' xi)). intro H1. generalize (I.lower_bounded_correct _ (proj1 (H1 (refl_equal _)))). clear H1. intros (_, H1). unfold I.bounded_prop in H1. { destruct (I.convert (fi' xi)). have Hex : exists v : R, contains Inan (Xreal v) by exists R0. by move/(_ Hex) in H1. by case: H0. } intros _. now apply Hf. apply diff_refining_points_correct with (1 := Hd) (7 := Hx). apply Hf. apply Hf'. apply Hf. apply (convert_bnd l u). rewrite <- H. apply I.midpoint_correct. apply not_empty_contains with (1 := Hx). generalize (I.lower_bounded_correct xi). case (I.lower_bounded xi). refine (fun H0 => _ (H0 (refl_equal true))). clear H0. intros (H0, H1). apply Hf. apply (convert_bnd l l). rewrite -> H1, H0 in H. rewrite H0. inversion_clear H. split; exact: Rle_refl. apply not_empty_contains with (1 := Hx). now intros _. generalize (I.upper_bounded_correct xi). case (I.upper_bounded xi). refine (fun H0 => _ (H0 (refl_equal true))). clear H0. intros (H0, H1). apply Hf. apply (convert_bnd u u). rewrite -> H1, H0 in H. rewrite H0. inversion H. split ; apply Rle_refl. apply not_empty_contains with (1 := Hx). now intros _. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog