Commit 9790dfdd authored by Heiko Becker's avatar Heiko Becker

Remove admits from attic files

parent ee0c7601
......@@ -176,7 +176,7 @@ Proof.
pose proof (const_abs_err_bounded _ _ _ _ eval_cst1 H4).
pose proof (param_abs_err_bounded _ _ _ _ eval_param_u H5).
assert (eval_exp machineEpsilon (updEnv 2 (perturb (cenv u) delta1) (updEnv 1 (perturb cst1 delta0) cenv))
(Binop Plus (Var R 1) (Var R 2)) (perturb (eval_binop Plus (perturb cst1 delta0) (perturb (cenv u) delta1)) delta)) by admit.
(Binop Plus (Var R 1) (Var R 2)) (perturb (eval_binop Plus (perturb cst1 delta0) (perturb (cenv u) delta1)) delta)) by .
pose proof (add_abs_err_bounded _ _ _ _ _ _ _ _ _ _ _ eval_cst1 H4 eval_param_u H5 eval_real H6 H H3).
eapply Rle_trans.
apply H7.
......@@ -384,4 +384,4 @@ Qed.
unfold cst1, errAddUCst, machineEpsilon; prove_constant.
}
Qed. *)
*)
\ No newline at end of file
*)
......@@ -123,7 +123,7 @@ Proof.
rewrite Rmax_left; [ |apply Req_le; auto].
assert (Rabs 100 = 100)%R by (unfold Rabs; destruct Rcase_abs; lra).
rewrite H.
(* TODO: What about vlaues that are actually floats ? *) admit.
(* TODO: What about vlaues that are actually floats ? *) .
+ apply (AbsErrParam u (mkInterval (- 100) (100)) errVaru); [constructor | ].
unfold isSoundErr; simpl.
unfold Expressions.machineEpsilon, errVaru.
......@@ -311,4 +311,4 @@ Proof.
Qed. *)
Admitted.
*)
\ No newline at end of file
*)
......@@ -271,11 +271,11 @@ Proof.
rewrite (Rmult_comm a b).
apply (Rge_trans _ (ivlo1 * ivlo2) _); auto.
apply Rle_ge, Rmax_l.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
**)
\ No newline at end of file
- .
- .
- .
- .
- .
- .
- .
**)
......@@ -56,12 +56,12 @@ Proof.
rewrite Rabs_Ropp.
erewrite Rmax_eq.
unfold machineEpsilon.
admit.
.
- apply AbsErrVar.
unfold isValidErr.
simpl.
(* There is a flaw on how we handle variable errors currently as far as it seems *)
admit.
.
- split.
+ unfold isValidIntv.
split.
......@@ -122,4 +122,4 @@ Proof.
inversion H5 as [ | | op c d e].
(* float valued eval *)
Qed.
\ No newline at end of file
Qed.
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