Commit d313ddeb authored by Heiko Becker's avatar Heiko Becker
Browse files

Add some comments to Coq dev

parent 4aeb41a8
...@@ -402,6 +402,8 @@ Proof. ...@@ -402,6 +402,8 @@ Proof.
assert (0 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as zero_up_nR1 by lra. assert (0 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as zero_up_nR1 by lra.
assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R as nR1_to_sum by lra. assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1)%R as nR1_to_sum by lra.
assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R as sum_to_errsum by lra. assert (RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2 + RmaxAbsFun (Q2R e2lo, Q2R e2hi) * Q2R err1 + Q2R err1 * Q2R err2)%R as sum_to_errsum by lra.
clear e1_real e1_float e2_real e2_float eval_real eval_float valid_error
absenv_e1 absenv_e2.
(* Large case distinction for (* Large case distinction for
a) different cases of the value of Rabs (...) and a) different cases of the value of Rabs (...) and
b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *) b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
...@@ -722,6 +724,7 @@ Proof. ...@@ -722,6 +724,7 @@ Proof.
apply H. apply H.
lra. lra.
} }
(* All positive *)
+ assert (nF1 <= Q2R err1 + nR1)%R by lra. + assert (nF1 <= Q2R err1 + nR1)%R by lra.
assert (nF2 <= Q2R err2 + nR2)%R by lra. assert (nF2 <= Q2R err2 + nR2)%R by lra.
unfold Rabs. unfold Rabs.
...@@ -790,7 +793,7 @@ Proof. ...@@ -790,7 +793,7 @@ Proof.
rewrite Rmult_comm. rewrite Rmult_comm.
eapply Rmult_le_compat_neg_l. eapply Rmult_le_compat_neg_l.
lra. lra.
assert (nR1 - Q2R err1 <= nF1)%R by lra. ` assert (nR1 - Q2R err1 <= nF1)%R by lra.
apply H1. apply H1.
lra. lra.
} }
......
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