Commit 09aac76c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Port i_bisect_diff to the new engine.

parent 0453cff8
......@@ -1623,6 +1623,28 @@ now destruct a.
exact (proj1 (H xi)).
Qed.
Theorem eval_correct :
forall prec prog bounds n xi x,
contains (I.convert xi) (Xreal x) ->
contains (I.convert (eval prec prog (map interval_from_bp bounds) n xi))
(Xreal (nth n (eval_real prog (x :: map real_from_bp bounds)) 0%R)).
Proof.
intros prec prog bounds n xi x Hx.
set (yi := eval prec prog (map interval_from_bp bounds) n xi).
apply (xreal_to_real (fun y => contains (I.convert yi) y) (fun y => contains (I.convert yi) (Xreal y))).
now destruct (I.convert yi).
easy.
simpl.
replace (map Xreal (map real_from_bp bounds)) with (map xreal_from_bp bounds).
apply eval_correct_ext with (1 := Hx).
clear.
induction bounds.
easy.
simpl.
rewrite IHbounds.
now case a.
Qed.
End DiffValuator.
Module TaylorValuator.
......
......@@ -2332,6 +2332,39 @@ rewrite I.lower_correct I.upper_correct.
now destruct I.convert.
Qed.
Definition eval_bisect_diff prec depth hyps prog consts g :=
let bounds := R.merge_hyps prec hyps ++ map (T.eval_bnd prec) consts in
let xi := nth 0 bounds I.nai in
let bounds := tail bounds in
A.bisect_1d (I.lower xi) (I.upper xi) (fun b =>
R.eval_goal_bnd prec g (A.DiffValuator.eval prec prog bounds 0 b)
) depth.
Theorem eval_bisect_diff_correct :
forall prec depth var0 vars hyps prog consts g,
eval_bisect_diff prec depth hyps prog consts g = true ->
eval_hyps hyps (var0 :: vars)
(eval_goal g (nth 0 (eval_real prog ((var0 :: vars) ++ map (fun c => eval c nil) consts)) 0%R)).
Proof.
intros prec depth var0 vars hyps prog consts g H.
apply (R.eval_hyps_bnd_correct prec).
intros H'.
apply A.bisect_1d_correct' with (P := fun x => eval_goal g (nth 0 (eval_real prog ((x :: vars) ++ map (fun c => eval c nil) consts)) 0%R)) (2 := H).
intros x xi Ix.
apply (R.eval_goal_bnd_correct prec).
destruct hyps as [|hx hyps].
easy.
destruct H' as [H1 H2].
simpl.
destruct (app_merge_hyps_eval_bnd _ _ _ consts H2) as [bp [<- <-]].
apply A.DiffValuator.eval_correct with (1 := Ix).
destruct R.merge_hyps as [|vi t].
easy.
simpl in H' |- *.
rewrite I.lower_correct I.upper_correct.
now destruct I.convert.
Qed.
Ltac do_interval' vars prec depth rint_depth rint_prec rint_deg native nocheck eval_tac :=
let prec := eval vm_compute in (prec_of_nat prec) in
massage_goal ;
......@@ -2360,7 +2393,7 @@ Ltac do_interval_bisect' prec depth :=
apply (eval_bisect_correct prec depth).
Ltac do_interval_bisect_diff' prec depth :=
idtac.
apply (eval_bisect_diff_correct prec depth).
Ltac do_interval_bisect_taylor' deg prec depth :=
idtac.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment