proposition: Theorem bisect_correct : forall steps bounds idx check (P : _ -> Prop), ( forall xi x, contains_all xi x -> check xi = true -> P x ) -> bisect bounds idx check steps = true -> forall x, contains_all bounds x -> P x.
proof: Proof. intros steps bounds idx check P HP. revert idx bounds. induction steps as [|steps IH]. intros idx bounds Hc x H. apply HP with (1 := H) (2 := Hc). intros [|i idx] bounds Hc x H. apply HP with (1 := H) (2 := Hc). revert Hc. simpl. unfold bisect_step. case_eq (check bounds). intros Hc _ . apply HP with (1 := H) (2 := Hc). intros _. generalize (IH (app idx (i :: nil)) (change_nth i bounds (fun xi => fst (I.bisect xi)))). case bisect. 2: easy. intros H1 Hc. specialize (H1 eq_refl x). assert (H2 := IH _ _ Hc x). clear -H H1 H2. destruct (I.bisect_correct (nth i bounds I.nai) (Xreal (nth i x 0))) as [Hi|Hi]. - apply H. - apply H1. clear -H Hi. split. rewrite length_change_nth. apply H. intros n. generalize (change_nth_correct n i bounds I.nai (fun xi => fst (I.bisect xi))). intros [[_ [<- ->]] | ->]. exact Hi. apply H. - apply H2. clear -H Hi. split. rewrite length_change_nth. apply H. intros n. generalize (change_nth_correct n i bounds I.nai (fun xi => snd (I.bisect xi))). intros [[_ [<- ->]] | ->]. exact Hi. apply H. 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