Commit c2327db4 authored by Nikita Zyuzin's avatar Nikita Zyuzin
Browse files

Complete `validErrorboundCorrectFma` proof

parent 1c6d6820
......@@ -2039,18 +2039,31 @@ Proof.
subst.
apply RmaxAbs; subst; simpl in *.
unfold RmaxAbsFun.
+ clear H6.
+ rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus.
rewrite Q2R_max4.
rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus; eauto.
repeat rewrite Q2R_minus.
assumption.
+ rewrite Q2R_max4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
rewrite <- maxAbs_impl_RmaxAbs.
Admitted.
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus.
rewrite Q2R_max4.
rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus;
repeat rewrite Q2R_minus.
assumption.
Qed.
Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 ->
......
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