Commit 9b427ee4 authored by Heiko Becker's avatar Heiko Becker

More work on toy example, AbsErrExp part of goal is fully proven

parent 1ced9183
......@@ -35,7 +35,7 @@ Definition valCstAddVarU:exp R := Binop Plus valCst varU.
(** Error values **)
Definition errCst1 := realFromNum 7358558207215537 15 14.
Definition errVaru := realFromNum 2220446049250313 15 14.
Definition lowerBoundAddUCst:R := - (1157) / 5.
Definition lowerBoundAddUCst:R := 1157 / 5.
Definition upperBoundAddUCst:R := 2157 / 5.
Definition errAddUCst := realFromNum 19158008512931703 16 13.
......@@ -75,41 +75,44 @@ Proof.
[ exfalso; apply Rlt_not_le in lt_plus; apply lt_plus; apply Rge_le in H; auto | ].
rewrite Rmax_left; [ | apply Req_le; auto].
unfold realFromNum, negPow.
field_simplify.
interval.
assert (1657 / 5 - realFromNum 11102230246251565 16 16 >= 0)%R by (unfold realFromNum, negPow; interval).
assert (1657 / 5 + realFromNum 11102230246251565 16 16 >= 0)%R by (unfold realFromNum, negPow; interval).
unfold Rabs. destruct Rcase_abs.
* exfalso.
apply Rlt_not_le in r.
apply r; apply Rge_le in H; auto.
* destruct Rcase_abs as [lt_plus | ge_plus];
[ exfalso; apply Rlt_not_le in lt_plus; apply lt_plus; apply Rge_le in H0; auto | ].
assert ((1657 / 5 + realFromNum 11102230246251565 16 16) > (1657 / 5 - realFromNum 11102230246251565 16 16))%R by (unfold realFromNum, negPow; interval).
erewrite Rmax_left; auto.
unfold realFromNum.
unfold negPow.
interval.
unfold Rabs.
assert (1657 / 5 >= 0)%R by interval.
destruct Rcase_abs.
* exfalso.
apply Rlt_not_le in r.
apply r.
apply Rge_le in H0; auto.
field_simplify.
interval.
(** TODO: Flaw in computation. Wolfram Alpha says that this inequation is simply false **)
admit.
+ apply (AbsErrVar u (mkInterval (- 100) (100)) errVaru); [constructor | ].
unfold isSoundErr; simpl.
unfold machineEpsilon, errVaru.
unfold realFromNum.
unfold negPow.
simpl.
field_simplify.
admit. (** Same as const case *)
+ simpl. admit.
assert (Rabs (-100) = 100%R) by (unfold Rabs; destruct Rcase_abs; lra).
rewrite H.
assert (Rabs 100 = 100)%R by (unfold Rabs; destruct Rcase_abs; lra).
rewrite H0.
rewrite Rmax_left; [ | apply Req_le; auto].
interval.
+ unfold isSoundErrBin, valCst; split; try split; simpl; [unfold min4| unfold max4| ].
* assert (Rmin (cst1 + - 100) (cst1 + 100) = (cst1 + - 100))%R by (unfold cst1; apply Rmin_left; interval).
rewrite H.
rewrite Rmin_comm in H.
rewrite H.
rewrite Rmin_left; [ | apply Req_le; auto].
unfold cst1, lowerBoundAddUCst.
field_simplify.
apply Req_le; auto. (* FIXME: Why does interval not work here? *)
* assert (Rmax (cst1 + - 100) (cst1 + 100) = (cst1 + 100))%R by (unfold cst1; apply Rmax_right; interval).
assert (Rmax (cst1 + 100) (cst1 + 100) = cst1 + 100)%R by (apply Rmax_left; apply Req_le; auto). (* TODO: lemma *)
rewrite H.
rewrite H0.
rewrite H.
unfold cst1, upperBoundAddUCst.
field_simplify.
apply Req_le; auto.
* unfold isSoundErr; simpl.
unfold lowerBoundAddUCst, upperBoundAddUCst, errAddUCst.
unfold machineEpsilon, realFromNum, negPow.
assert (0 <= (1157/5))%R by interval.
assert (0 <= (2157/5))%R by interval.
repeat rewrite Rabs_pos_eq; auto.
rewrite Rmax_right; [ | interval].
interval.
(* Semantic judgement *)
- inversion eval_real; subst.
inversion H4; subst.
inversion H5; subst.
......
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