Commit 0453cff8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Port i_bisect to the new engine.

parent f46c83f5
......@@ -414,6 +414,39 @@ apply IHsteps with (1 := Hr).
now rewrite <- I.bnd_correct.
Qed.
Theorem bisect_1d_correct' :
forall steps inpl inpu f P,
(forall y yi, contains (I.convert yi) (Xreal y) -> f yi = true -> P y) ->
bisect_1d inpl inpu f steps = true ->
forall x,
contains (I.convert (I.bnd inpl inpu)) (Xreal x) -> P x.
Proof.
intros steps inpl inpu f P Hf.
revert inpl inpu.
induction steps.
intros inpl inpu Hb.
discriminate Hb.
intros inpl inpu.
simpl.
unfold bisect_1d_step.
case_eq (f (I.bnd inpl inpu)).
intros Hb _ x Hx.
now apply Hf with (2 := Hb).
intros _.
set (inpm := I.midpoint (I.bnd inpl inpu)).
case_eq (bisect_1d inpl inpm f steps) ; try easy.
intros Hl Hr x Hx.
change x with (proj_val (Xreal x)).
apply (bisect' P (I.convert_bound inpl) (I.convert_bound inpm) (I.convert_bound inpu)).
unfold domain'.
rewrite <- I.bnd_correct.
apply IHsteps with (1 := Hl).
unfold domain'.
rewrite <- I.bnd_correct.
apply IHsteps with (1 := Hr).
now rewrite <- I.bnd_correct.
Qed.
Definition lookup_1d_step fi l u output cont :=
if I.subset (fi (I.bnd l u)) output then output
else
......
......@@ -213,6 +213,37 @@ auto with real.
exact (proj2 (contains_le _ _ _ H)).
Qed.
Definition domain' P b :=
forall x, contains b (Xreal x) -> P x.
Theorem bisect' :
forall P xl xm xu,
domain' P (Ibnd xl xm) ->
domain' P (Ibnd xm xu) ->
domain' P (Ibnd xl xu).
Proof.
intros P xl xm xu Hl Hu x H.
elim H.
case_eq xm ; intros.
apply Hu.
rewrite H0.
exact (conj I (proj2 H)).
case (Rle_dec x r) ; intros Hr.
apply Hl.
apply le_contains.
exact (proj1 (contains_le _ _ _ H)).
rewrite H0.
exact Hr.
apply Hu.
apply le_contains.
rewrite H0.
unfold le_lower.
simpl.
apply Ropp_le_contravar.
auto with real.
exact (proj2 (contains_le _ _ _ H)).
Qed.
Definition not_empty xi :=
exists v, contains xi (Xreal v).
......
......@@ -2299,6 +2299,38 @@ destruct (app_merge_hyps_eval_bnd _ _ _ consts H') as [bp [<- <-]].
apply contains_eval.
Qed.
Definition eval_bisect 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 (nth 0 (A.BndValuator.eval prec prog (b :: bounds)) I.nai)
) depth.
Theorem eval_bisect_correct :
forall prec depth var0 vars hyps prog consts g,
eval_bisect 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 y yi Iy.
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 (contains_eval _ _ (A.Bproof _ _ Iy :: bp)).
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
......@@ -2325,7 +2357,7 @@ Ltac do_interval_eval' prec depth :=
apply (eval_bnd_correct prec).
Ltac do_interval_bisect' prec depth :=
idtac.
apply (eval_bisect_correct prec depth).
Ltac do_interval_bisect_diff' 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