proposition: Theorem diff_refining_points_correct : forall prec f f' xi yi yi' ym yl yu, Xderive f f' -> (forall x, contains (I.convert xi) x -> contains (I.convert yi) (f x)) -> (forall x, contains (I.convert xi) x -> contains (I.convert yi') (f' x)) -> contains (I.convert ym) (f (I.F.convert (I.midpoint xi))) -> (if I.lower_bounded xi then contains (I.convert yl) (f (I.F.convert (I.lower xi))) else True) -> (if I.upper_bounded xi then contains (I.convert yu) (f (I.F.convert (I.upper xi))) else True) -> forall x, contains (I.convert xi) x -> contains (I.convert (diff_refining_points prec xi (I.sub prec xi (J.midpoint xi)) yi yi' ym yl yu)) (f x).
proof: Proof. intros prec f f' xi yi yi' ym yl yu Hd Hyi Hyi' Hym Hyl Hyu x Hx. unfold diff_refining_points. generalize (I.sign_large_correct yi'). assert (Hnexi : not_empty (I.convert xi)). { apply not_empty_contains with (1 := Hx). } case_eq (I.sign_large yi') ; intros Hs1 Hs2. eapply diff_refining_aux_2 with (1 := Hd) (5 := Hx). apply J.subset_midpoint with (1 := Hnexi). now apply J.contains_midpoint. now destruct (I.midpoint_correct xi Hnexi) as [<- _]. intros. rewrite (Hs2 (f' x0)). split ; apply Rle_refl. now apply Hyi'. assert (I.sign_large yi' <> Xund). now rewrite Hs1. clear Hs1. rename H into Hs1. assert (forall x, contains (I.convert xi) x -> forall v, f x = Xreal (proj_fun v f (proj_val x)) /\ f' x = Xreal (proj_fun v f' (proj_val x)) /\ (proj_fun v f' (proj_val x) <= 0)%R). intros a Ha v. destruct (Hs2 _ (Hyi' _ Ha)) as (Ha1, Ha2). destruct (diff_refining_aux_0 _ _ _ _ Hd Hs1 Hyi' _ Ha) as (Ha3, Ha4). destruct (Ha4 v) as (Ha5, Ha6). split. exact Ha5. split. exact Ha6. rewrite Ha1 in Ha6. inversion Ha6. exact Ha2. clear Hs2. rename H into Hs2. apply I.meet_correct. case_eq (I.lower_bounded xi). intros H. destruct (I.lower_bounded_correct xi H) as (Hxl, Hxi). rewrite H in Hyl. clear Hym Hyu H. assert (Hl: contains (I.convert xi) (I.F.convert (I.lower xi))). rewrite (Hxi Hnexi) Hxl. apply contains_lower with x. now rewrite <- Hxl, <- Hxi. rewrite (proj1 (Hs2 _ Hx R0)). apply I.lower_extent_correct with (proj_fun 0 f (proj_val (I.F.convert (I.lower xi)))). now rewrite <- (proj1 (Hs2 _ Hl 0)). destruct (diff_refining_aux_0 _ _ _ _ Hd Hs1 Hyi' _ Hx) as (Hx1, _). eapply (derivable_neg_imp_decreasing (proj_fun R0 f) (proj_fun R0 f')). apply (contains_connected (I.convert xi)). intros a Ha. simpl in Ha. destruct (Hs2 _ Ha R0) as (Ha1, (Ha2, Ha3)). split. generalize (Hd (Xreal a)). unfold Xderive_pt. rewrite Ha2 Ha1. intro H. exact (H R0). exact Ha3. simpl. now rewrite <- Hxl. simpl. now rewrite <- Hx1. rewrite -> Hxi, Hx1, Hxl in Hx. exact (proj1 Hx). exact Hnexi. intros _. rewrite (proj1 (Hs2 x Hx R0)). apply I.whole_correct. case_eq (I.upper_bounded xi). intros H. destruct (I.upper_bounded_correct xi H) as (Hxu, Hxi). rewrite H in Hyu. clear H. assert (Hu: contains (I.convert xi) (I.F.convert (I.upper xi))). rewrite (Hxi Hnexi) Hxu. apply contains_upper with x. now rewrite <- Hxu, <- Hxi. rewrite (proj1 (Hs2 _ Hx R0)). apply I.upper_extent_correct with (proj_fun 0 f (proj_val (I.F.convert (I.upper xi)))). now rewrite <- (proj1 (Hs2 _ Hu 0)). destruct (diff_refining_aux_0 _ _ _ _ Hd Hs1 Hyi' _ Hx) as (Hx1, _). eapply (derivable_neg_imp_decreasing (proj_fun R0 f) (proj_fun R0 f')). apply (contains_connected (I.convert xi)). intros a Ha. simpl in Ha. destruct (Hs2 _ Ha R0) as (Ha1, (Ha2, Ha3)). split. generalize (Hd (Xreal a)). unfold Xderive_pt. rewrite Ha2 Ha1. intro H. exact (H R0). exact Ha3. simpl. now rewrite <- Hx1. simpl. now rewrite <- Hxu. rewrite -> Hxi, Hx1, Hxu in Hx. exact (proj2 Hx). exact Hnexi. intros _. rewrite (proj1 (Hs2 x Hx R0)). apply I.whole_correct. assert (I.sign_large yi' <> Xund). now rewrite Hs1. clear Hs1. rename H into Hs1. assert (forall x, contains (I.convert xi) x -> forall v, f x = Xreal (proj_fun v f (proj_val x)) /\ f' x = Xreal (proj_fun v f' (proj_val x)) /\ (0 <= proj_fun v f' (proj_val x))%R). intros a Ha v. destruct (Hs2 _ (Hyi' _ Ha)) as (Ha1, Ha2). destruct (diff_refining_aux_0 _ _ _ _ Hd Hs1 Hyi' _ Ha) as (Ha3, Ha4). destruct (Ha4 v) as (Ha5, Ha6). split. exact Ha5. split. exact Ha6. rewrite Ha1 in Ha6. inversion Ha6. exact Ha2. clear Hs2. rename H into Hs2. apply I.meet_correct. case_eq (I.lower_bounded xi). intros H. destruct (I.lower_bounded_correct xi H) as (Hxl, Hxi). rewrite H in Hyl. clear H. assert (Hl: contains (I.convert xi) (I.F.convert (I.lower xi))). rewrite (Hxi Hnexi) Hxl. apply contains_lower with x. now rewrite <- Hxl, <- Hxi. rewrite (proj1 (Hs2 _ Hx R0)). apply I.upper_extent_correct with (proj_fun 0 f (proj_val (I.F.convert (I.lower xi)))). now rewrite <- (proj1 (Hs2 _ Hl 0)). destruct (diff_refining_aux_0 _ _ _ _ Hd Hs1 Hyi' _ Hx) as (Hx1, _). eapply (derivable_pos_imp_increasing (proj_fun 0 f) (proj_fun 0 f')). apply (contains_connected (I.convert xi)). intros a Ha. simpl in Ha. destruct (Hs2 _ Ha R0) as (Ha1, (Ha2, Ha3)). split. generalize (Hd (Xreal a)). unfold Xderive_pt. rewrite Ha2 Ha1. intro H. exact (H R0). exact Ha3. simpl. now rewrite <- Hxl. simpl. now rewrite <- Hx1. rewrite -> Hxi, Hx1, Hxl in Hx. exact (proj1 Hx). exact Hnexi. intros _. rewrite (proj1 (Hs2 x Hx R0)). apply I.whole_correct. case_eq (I.upper_bounded xi). intros H. destruct (I.upper_bounded_correct xi H) as (Hxu, Hxi). rewrite H in Hyu. clear H. assert (Hu: contains (I.convert xi) (I.F.convert (I.upper xi))). rewrite (Hxi Hnexi) Hxu. apply contains_upper with x. now rewrite <- Hxu, <- Hxi. rewrite (proj1 (Hs2 _ Hx R0)). apply I.lower_extent_correct with (proj_fun 0 f (proj_val (I.F.convert (I.upper xi)))). now rewrite <- (proj1 (Hs2 _ Hu 0)). destruct (diff_refining_aux_0 _ _ _ _ Hd Hs1 Hyi' _ Hx) as (Hx1, _). eapply (derivable_pos_imp_increasing (proj_fun 0 f) (proj_fun 0 f')). apply (contains_connected (I.convert xi)). intros a Ha. simpl in Ha. destruct (Hs2 _ Ha R0) as (Ha1, (Ha2, Ha3)). split. generalize (Hd (Xreal a)). unfold Xderive_pt. rewrite Ha2 Ha1. intro H. exact (H R0). exact Ha3. simpl. now rewrite <- Hx1. simpl. now rewrite <- Hxu. rewrite -> Hxi, Hx1, Hxu in Hx. exact (proj2 Hx). exact Hnexi. intros _. rewrite (proj1 (Hs2 x Hx R0)). apply I.whole_correct. clear Hs1 Hs2. case_eq (I.bounded yi') ; intro Hb. apply I.meet_correct. now apply Hyi. destruct (I.midpoint_correct xi Hnexi) as (Hm1, Hm2). eapply diff_refining_aux_1 with (1 := Hd). now apply J.contains_midpoint. now rewrite <- Hm1. now rewrite <- Hm1. exact Hyi'. exact Hx. now apply Hyi. 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