Commit 112d9e19 authored by Heiko Becker's avatar Heiko Becker

Fix typo in Coq script and add draft of division proof

parent 945abf48
......@@ -793,7 +793,7 @@ Proof.
rewrite Rmult_comm.
eapply Rmult_le_compat_neg_l.
lra.
` assert (nR1 - Q2R err1 <= nF1)%R by lra.
assert (nR1 - Q2R err1 <= nF1)%R by lra.
apply H1.
lra.
}
......@@ -858,51 +858,6 @@ Proof.
repeat rewrite Q2R_plus; auto.
Qed.
Lemma err_prop_inversion_pos_down nF2 nR2 err2 (e2lo e2hi :Q)
(float_iv_pos : (Q2R 0 < Q2R (e2lo - err2))%R)
(real_iv_pos : (Q2R 0 < Q2R e2lo)%R)
(r0 : (nR2 - nF2 < 0)%R)
(err2_bounded : (- nR2 + nF2 <= Q2R err2)%R)
(valid_bounds_e2 : (Q2R e2lo <= nR2 <= Q2R e2hi)%R)
(valid_bounds_e2_err : (Q2R e2lo - Q2R err2 <= nF2 <= Q2R e2hi + Q2R err2)%R)
(err2_pos : (0 <= Q2R err2)%R):
( - Q2R err2 * / ((Q2R e2lo - Q2R err2) * (Q2R e2lo - Q2R err2)) <= / nF2 - / nR2)%R.
Proof.
assert (nF2 <= Q2R err2 + nR2)%R by lra.
assert (nR2 - Q2R err2 <= nF2)%R by lra.
assert (0 < nR2 - Q2R err2)%R.
- rewrite <- Q2R0_is_0.
eapply Rlt_le_trans.
apply float_iv_pos.
rewrite Q2R_minus; lra.
- assert (0 < nF2)%R by (rewrite <- Q2R0_is_0; lra).
apply Rinv_le_contravar in H; try auto.
apply Rinv_le_contravar in H0; try auto.
repeat rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
Focus 2.
eapply Rplus_le_compat_r.
apply H.
rewrite Ropp_inv_permute; try lra.
rewrite equal_naming_inv; try lra.
assert (Q2R err2 + nR2 + - nR2 = Q2R err2)%R by lra.
rewrite H3.
unfold Rdiv.
rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
rewrite <- Ropp_inv_permute.
+ rewrite <- Ropp_mult_distr_r. apply Ropp_le_contravar.
apply Rmult_le_compat_l; try auto.
apply Rinv_le_contravar.
* rewrite <- Rsub_eq_Ropp_Rplus.
apply Rmult_0_lt_preserving; rewrite <- Q2R_minus; rewrite <- Q2R0_is_0; try lra.
* eapply Rmult_le_compat; try lra;
rewrite <- Rsub_eq_Ropp_Rplus;
rewrite <- Q2R_minus, <- Q2R0_is_0; lra.
+ assert (0 < (Q2R err2 + nR2) * nR2)%R.
* apply Rmult_0_lt_preserving; lra.
* lra.
Qed.
Lemma validErrorboundCorrectDiv cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
eval_exp 0%R cenv P (toRExp e1) nR1 ->
eval_exp 0%R cenv P (toRExp e2) nR2 ->
......
......@@ -854,17 +854,15 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
once_rewrite_tac [validErrorbound_def] \\
rpt (strip_tac) \\ fs[] \\
rpt (strip_tac) \\
qpat_x_assum `validIntervalbounds _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm)) \\
qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
fs [] \\
qpat_x_assum `absenv e1 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
qpat_x_assum `absenv e2 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
fs [] \\
`FST (FST (absenv e1 )) <= nR1 /\ nR1 <= SND (FST (absenv e1))`
by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ simp[]) \\
by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ fs[]) \\
`FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2))`
by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ simp[]) \\
by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ fs[]) \\
qpat_x_assum `absenv e1 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
qpat_x_assum `absenv e2 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
`0 <= err1`
......@@ -874,21 +872,28 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
by (match_mp_tac err_always_positive \\
qexists_tac `e2` \\ qexists_tac `absenv` \\ qexists_tac `(e2lo,e2hi)` \\ fs[]) \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * machineEpsilon` \\
qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + abs (nF1 / nF2) * machineEpsilon` \\
conj_tac
>- (match_mp_tac mult_abs_err_bounded \\
>- (match_mp_tac div_abs_err_bounded \\
qexists_tac `e1` \\ qexists_tac `e2` \\ qexists_tac `cenv` \\ qexists_tac `P` \\
qexists_tac `err1` \\ qexists_tac `err2` \\
fs [])
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `maxAbsFun (e1lo,e1hi) * err2 + maxAbsFun (e2lo,e2hi) * err1 +
err1 * err2 +
maxAbsFun (multInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon` \\
conj_tac \\ TRY(simp[]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac \\
>- (cheat)
>- (simp[maxAbsFun_def] \\
qexists_tac
`maxAbsFun (e1lo,e1hi) * (1 / (minAbsFun (widenInterval (e2lo,e2hi) err2) *
minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
maxAbsFun (invertInterval (e2lo,e2hi)) * err1 +
err1 *
(1 /
(minAbsFun (widenInterval (e2lo,e2hi) err2) *
minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
maxAbsFun
(divideInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon` \\
conj_tac \\
>- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\
>- (cheat)
>- (simp[maxAbsFun_def] \\
once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\
conj_tac \\ simp[mEps_geq_zero] \\
match_mp_tac maxAbs \\
......@@ -898,10 +903,12 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
`contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv \\
qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\
`contained (nF1 * nF2) (multInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac interval_multiplication_valid \\
conj_tac \\ simp[]) \\
`contained (nF1 / nF2) (divideInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac interval_division_valid \\
conj_tac \\ fs[]) \\
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[])));
simp[]))
>- (fs[]) \\
));
val _ = export_theory();
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