Commit c39aa028 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Prove variants of Eval theorems on real numbers.

parent 487dec35
...@@ -678,13 +678,24 @@ Theorem eval_correct_ext : ...@@ -678,13 +678,24 @@ Theorem eval_correct_ext :
(fun b => nth n (eval prec prog (b :: map interval_from_bp bounds)) I.nai). (fun b => nth n (eval prec prog (b :: map interval_from_bp bounds)) I.nai).
Proof. Proof.
intros prec prog bounds n xi x Hx. intros prec prog bounds n xi x Hx.
generalize n. clear n. revert n.
apply eval_correct_aux. apply eval_correct_aux.
intros [|n]. intros [|n].
exact Hx. exact Hx.
apply iterated_bnd_nth. apply iterated_bnd_nth.
Qed. Qed.
Theorem eval_correct_ext' :
forall prec prog bounds n xi x,
contains (I.convert xi) (Xreal x) ->
contains
(I.convert (nth n (eval prec prog (xi :: map interval_from_bp bounds)) I.nai))
(Xreal (nth n (eval_real prog (x :: map real_from_bp bounds)) 0%R)).
Proof.
intros prec prog bounds n xi x Hx.
apply (eval_correct' prec prog (Bproof _ _ Hx :: bounds)).
Qed.
Lemma continuous_eval : Lemma continuous_eval :
forall prec prog bounds m i x, forall prec prog bounds m i x,
no_floor_prog prog = true -> no_floor_prog prog = true ->
...@@ -1772,6 +1783,56 @@ induction (rev prog) as [|t l]. ...@@ -1772,6 +1783,56 @@ induction (rev prog) as [|t l].
apply TM.div_correct. apply TM.div_correct.
Qed. Qed.
Theorem eval_correct_aux' :
forall prec deg prog bounds n xi,
TM.approximates xi
(nth n (eval prec deg xi prog (TM.var :: map (fun b => TM.const (interval_from_bp b)) bounds)) TM.dummy)
(fun x => Xreal (nth n (eval_real prog (x :: map real_from_bp bounds)) 0)).
Proof.
intros prec deg prog bounds n xi.
generalize (eval_correct_aux prec deg prog bounds n xi).
set (t := nth n _ _).
destruct (nth n _ _) as [c| |].
- destruct (I.convert c) as [|cl cu] eqn: Hc.
now left.
intros [Hf|[y H1 H2]].
now left.
destruct y as [|y].
now rewrite Hc in H1.
right.
exists (Xreal y).
exact H1.
intros x Hx.
apply (xreal_to_real (fun x => x = Xreal y) (fun x => Xreal x = Xreal y)) ; try easy.
simpl.
rewrite map_Xreal_map_real_from_bp.
now apply H2.
- intros H y Hy.
apply (xreal_to_real (fun x => x = Xreal y) (fun x => Xreal x = Xreal y)) ; try easy.
simpl.
rewrite map_Xreal_map_real_from_bp.
now apply H.
- intros H Hn.
destruct (H Hn) as [H1 H2 H3 H4 H5].
split ; try easy.
intros x0 Hx0.
destruct (H5 x0 Hx0) as [Q H6 H7].
exists Q.
exact H6.
intros x Hx.
simpl.
apply (xreal_to_real (fun v => (v = Xnan -> I.convert (Taylor_model_sharp.error r) = Inan) /\ contains (I.convert (Taylor_model_sharp.error r)) (Xreal (proj_val v - Datatypes.PolR.horner tt Q (x - x0)))) (fun v => contains (I.convert (Taylor_model_sharp.error r)) (Xreal (v - Datatypes.PolR.horner tt Q (x - x0))))).
+ intros [Ha _].
now rewrite Ha.
+ intros a Ha.
apply Ha.
+ simpl.
rewrite map_Xreal_map_real_from_bp.
split.
now apply H1.
now apply H7.
Qed.
Theorem eval_correct_ext : Theorem eval_correct_ext :
forall prec deg prog bounds n yi, forall prec deg prog bounds n yi,
I.extension I.extension
......
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