Commit b65d4c4e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add some syntactic sugar around Prog.eval_real.

This commit also makes Prog.extract detect one-instruction program.
parent 4f44319a
......@@ -398,24 +398,32 @@ Definition extract (e : expr) (vars : nat) :=
match split_expr e nil nil with
| Sconst => Eprog (cons (Forward vars) nil) (cons e nil)
| Scomposed lp lc =>
match decompose vars nil (e :: lp) lc with
let lp' :=
match lp with
| cons h t => if expr_beq e h then lp else e :: lp
| nil => e :: lp
end in
match decompose vars nil lp' lc with
| Some p => if max_arity e vars then Eprog p lc else Eabort
| None => Eabort
end
end.
Definition eval_real' prog vars consts :=
nth 0 (eval_real prog (vars ++ map (fun c => eval c nil) consts)) 0%R.
Theorem extract_correct :
forall e vars,
match extract e (length vars) with
| Eabort => True
| Eprog lp lc =>
nth 0 (eval_real lp (vars ++ map (fun c => eval c nil) lc)) 0%R = eval e vars
| Eprog lp lc => eval_real' lp vars lc = eval e vars
end.
Proof.
intros e vars.
unfold extract.
generalize (fun v => split_expr_correct v e nil nil).
destruct split_expr as [|lp lc].
unfold eval_real'.
simpl.
intros H.
rewrite app_nth2 by apply le_refl.
......@@ -423,10 +431,26 @@ destruct split_expr as [|lp lc].
apply sym_eq, H.
now intros [|n].
intros H.
assert (exists lp',
match lp with
| cons h t => if expr_beq e h then lp else e :: lp
| nil => e :: lp
end = e :: lp') as [lp' ->].
destruct lp as [|h t].
now exists nil.
generalize (internal_expr_dec_bl e h).
destruct expr_beq.
intros ->.
now exists t.
apply eq_refl.
intros _.
now exists (h :: t).
simpl in H.
generalize (decompose_correct vars nil (e :: lp) lc).
generalize (decompose_correct vars nil (e :: lp') lc).
destruct decompose as [p|] ; try easy.
case_eq (max_arity e (length vars)).
2: easy.
unfold eval_real'.
intros H' ->.
simpl.
clear -H'.
......@@ -443,5 +467,4 @@ now apply IHe2.
intros v.
apply H.
now intros [|n].
easy.
Qed.
......@@ -2289,19 +2289,20 @@ Theorem eval_bisect_aux :
let bounds := tail bounds in
A.bisect_1d (I.lower xi) (I.upper xi) (fun b => R.eval_goal_bnd prec g (fi b bounds)) depth = 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)).
(eval_goal g (eval_real' prog (var0 :: vars) consts)).
Proof.
intros prec depth var0 vars hyps prog consts g fi Hfi.
simpl.
intros 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).
apply A.bisect_1d_correct' with (P := fun x => eval_goal g (eval_real' prog (x :: vars) consts)) (2 := H).
intros x xi Ix.
apply (R.eval_goal_bnd_correct prec).
destruct hyps as [|hx hyps].
easy.
destruct H' as [H1 H2].
unfold eval_real'.
simpl.
destruct (app_merge_hyps_eval_bnd _ _ _ consts H2) as [bp [<- <-]].
now apply Hfi.
......@@ -2324,7 +2325,7 @@ 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)).
(eval_goal g (eval_real' prog (var0 :: vars) consts)).
Proof.
intros prec depth var0 vars hyps prog consts g H.
apply (eval_bisect_aux prec depth) with (fi := fun b bounds => nth 0 (A.BndValuator.eval prec prog (b :: bounds)) I.nai) (2 := H).
......@@ -2344,7 +2345,7 @@ 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)).
(eval_goal g (eval_real' prog (var0 :: vars) consts)).
Proof.
intros prec depth var0 vars hyps prog consts g H.
apply (eval_bisect_aux prec depth) with (fi := fun b bounds => A.DiffValuator.eval prec prog bounds 0 b) (2 := H).
......@@ -2355,18 +2356,17 @@ Qed.
Definition eval_bisect_taylor prec deg 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
let bounds := A.TaylorValuator.TM.var :: map A.TaylorValuator.TM.const (tail bounds) in
A.bisect_1d (I.lower xi) (I.upper xi) (fun b =>
R.eval_goal_bnd prec g (A.TaylorValuator.TM.eval (prec, deg)
(nth 0 (A.TaylorValuator.eval prec deg b prog (A.TaylorValuator.TM.var ::
map A.TaylorValuator.TM.const bounds)) A.TaylorValuator.TM.dummy) b b)
(nth 0 (A.TaylorValuator.eval prec deg b prog bounds) A.TaylorValuator.TM.dummy) b b)
) depth.
Theorem eval_bisect_taylor_correct :
forall prec deg depth var0 vars hyps prog consts g,
eval_bisect_taylor prec deg 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)).
(eval_goal g (eval_real' prog (var0 :: vars) consts)).
Proof.
intros prec deg depth var0 vars hyps prog consts g H.
apply (eval_bisect_aux prec depth) with (fi := fun b bounds =>
......
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