proposition: Lemma clamp_plot_correct : forall prec oyi dyi f ox dx oy dy h l1 l2, (0 < dy)%R -> contains (I.convert oyi) (Xreal oy) -> contains (I.convert dyi) (Xreal (/dy)) -> clamp_plot prec oyi dyi h l1 = l2 -> plot1 f ox dx l1 -> plot2 f ox dx oy dy h l2.
proof: Proof. intros prec oyi dyi f ox dx oy dy h l l2 Hdy Boy Bdy <-. intros H i x Hx Hy. specialize (H i x Hx). revert i ox H Hx. induction l as [|yi l IH] ; intros [|i] ox Hl Hx. - now simpl ; rewrite Rmult_0_r, Rplus_0_r. - now simpl ; rewrite Rmult_0_r, Rplus_0_r. - assert (By: contains (I.convert (I.mul prec (I.sub prec yi oyi) dyi)) (Xreal ((f x - oy) / dy))). { apply J.mul_correct with (2 := Bdy). apply J.sub_correct with (2 := Boy). now apply Hl. } simpl nth. generalize (clamp_correct (I.mul prec (I.sub prec yi oyi) dyi) h ((f x - oy) / dy)%R By). destruct clamp as [y1 y2]. clear -Hdy Hy. intros H. apply affine_transf with (1 := Hdy). apply H. apply affine_transf with (1 := Hdy). now rewrite Rmult_0_r, Rplus_0_r. - apply (IH i (ox + dx * INR 1)%R Hl). now rewrite 2!Rplus_assoc, <- 2!Rmult_plus_distr_l, 2!(Rplus_comm 1), <- 2!S_INR. Qed.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog