proposition: Lemma sample_plot_correct : forall prec deg check vars hyps pf cf oxi dxi ox dx nb l, contains (I.convert oxi) (Xreal ox) -> contains (I.convert dxi) (Xreal dx) -> sample_plot prec deg check hyps pf cf oxi dxi (Zpos nb) = l -> eval_hyps hyps vars ( plot1 (fun t => eval_real' pf (t :: vars) cf) ox dx l).
proof: Proof. intros prec deg check vars hyps pf cf oxi dxi ox dx nb l Box Bdx <-. apply (R.eval_hyps_bnd_correct prec). intros H'. unfold sample_plot, eval_real'. set (bounds' := R.merge_hyps prec hyps ++ _). set (bounds := A.TaylorValuator.TM.var :: _). set (ui := I.add prec oxi (I.mul prec dxi (I.fromZ prec 0))). set (vi := I.add prec oxi (I.mul prec dxi (I.fromZ prec (Zpos nb)))). set (gi := fun yi => let zi := nth 0 (A.BndValuator.eval prec pf (yi :: bounds')) I.nai in let fi := nth 0 (A.TaylorValuator.eval prec deg yi pf bounds) A.TaylorValuator.TM.dummy in fun xi => let zi' := A.TaylorValuator.TM.eval (prec, deg) fi yi xi in if I.subset xi yi then I.meet zi zi' else zi'). set (f x := nth 0 (eval_real pf ((x :: vars) ++ map (fun c : expr => eval c nil) cf)) 0%R). fold (gi (I.join ui vi)). assert (Hg: forall ti xi x, contains (I.convert xi) (Xreal x) -> contains (I.convert (gi ti xi)) (Xreal (f x))). { intros ti xi x Hx. unfold gi. destruct I.subset eqn:Hs. apply I.meet_correct. apply A.BndValuator.eval_correct_ext'. now apply app_merge_hyps_eval_bnd. now apply I.subset_correct with (2 := Hs). apply A.TaylorValuator.eval_correct with (2 := Hx). now apply app_merge_hyps_eval_bnd. apply A.TaylorValuator.eval_correct with (2 := Hx). now apply app_merge_hyps_eval_bnd. } rewrite <- (Z2Nat.id (Zpos nb)) at 2 by easy. set (i := Z.to_nat (Zpos nb)). cut (plot1 f (ox + dx * INR i) dx nil). 2: intros [|j] x _ ; apply J.nai_correct. generalize (@nil I.type). generalize I.whole (I.join ui vi) 0%Z (Z.pos nb). clearbody f gi i. clear -Box Bdx Hg. induction i as [|n IH]. { simpl. intros _ _ _ _ l. now rewrite Rmult_0_r, Rplus_0_r. } intros zi2 gxi mz rz acc Hacc. cbn beta iota zeta delta [sample_plot_aux]. rewrite <- Nat2Z.inj_pred by apply Nat.lt_0_succ. simpl (Nat.pred (S n)). set (xi1 := I.add prec oxi (I.mul prec dxi (I.fromZ prec (Z.of_nat n)))). set (xi2 := I.add prec oxi (I.mul prec dxi (I.fromZ prec (Z.of_nat (S n))))). set (xi := I.join xi1 xi2). set (zi1 := gi gxi xi1). set (yi := gi gxi xi). set (c := andb (orb (check (I.meet yi (I.lower_extent zi1))) (check (I.meet yi (I.upper_extent zi1)))) (orb (check (I.meet yi (I.lower_extent zi2))) (check (I.meet yi (I.upper_extent zi2))))). clearbody c. set (yizi := if c then (yi, zi1) else (gi xi xi, gi xi xi1)). set (mz' := if Z.eqb mz (Z.of_nat n) then (mz - Z.div2 (3 * rz))%Z else if c then mz else (Z.of_nat n - 1 - Z.div2 rz)%Z). set (mz'' := if Z.ltb mz' 0%Z then 0%Z else mz'). clearbody mz' mz''. set (gxi' := I.join (I.add prec oxi (I.mul prec dxi (I.fromZ prec mz''))) xi1). clearbody gxi'. cut (plot1 f (ox + dx * INR n) dx (fst yizi :: acc)). { destruct Z.eqb ; apply IH. } clear -Box Bdx Hg Hacc. intros [|i] x Hx. 2: { apply Hacc. revert Hx. clear. rewrite !S_INR. replace (ox + dx * INR n + dx * (INR i + 1))%R with (ox + dx * (INR n + 1) + dx * INR i)%R by ring. replace (ox + dx * INR n + dx * (INR i + 1 + 1))%R with (ox + dx * (INR n + 1) + dx * (INR i + 1))%R by ring. easy. } assert (Hxi: contains (I.convert xi) (Xreal x)). { apply J.join_correct with (u := (ox + dx * (IZR (Z.of_nat n)))%R) (v := (ox + dx * (IZR (Z.of_nat (S n))))%R). apply J.add_correct with (1 := Box). apply J.mul_correct with (1 := Bdx). apply I.fromZ_correct. apply J.add_correct with (1 := Box). apply J.mul_correct with (1 := Bdx). apply I.fromZ_correct. rewrite Nat2Z.inj_succ, succ_IZR, <- INR_IZR_INZ. revert Hx. clear. now rewrite Rmult_0_r, Rplus_0_r, Rmult_plus_distr_l, Rplus_assoc. } now destruct c ; simpl ; apply Hg. Qed.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog