From 58de5a60d856197e2d926c24101f2c8e8f67fade Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Fri, 5 Mar 2021 16:02:46 +0100
Subject: [PATCH] Rework an error bound proof
---
hol4/ErrorBoundsScript.sml | 251 +++++++------------------------------
1 file changed, 47 insertions(+), 204 deletions(-)
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index 18aa186b..f9b2a3ac 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -441,7 +441,7 @@ Proof
QED
Theorem nonzerop_EQ1_I'[simp]:
- 0 < r ==> (nonzerop r = 1)
+ 0 < r ⇒ (nonzerop r = 1)
Proof
rw[nonzerop_def]
QED
@@ -449,93 +449,34 @@ QED
Theorem err_prop_inversion_pos:
∀ (nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
0 < elo - err ∧ 0 < elo ∧
- abs (nR - nF) <= err ∧
- elo <= nR ∧ nR <= ehi ∧
- elo - err <= nF ∧ nF <= ehi + err ∧
- 0 <= err ⇒
- abs (inv nR - inv nF) <= err * inv ((elo - err) * (elo - err))
+ abs (nR - nF) ≤ err ∧
+ elo ≤ nR ∧ nR ≤ ehi ∧
+ elo - err ≤ nF ∧ nF ≤ ehi + err ∧
+ 0 ≤ err ⇒
+ abs (inv nR - inv nF) ≤ err * inv ((elo - err) * (elo - err))
Proof
rpt strip_tac
- \\ `! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)`
- by (REAL_ASM_ARITH_TAC)
- \\ qpat_x_assum `!x. (A /\ B) \/ C` (qspecl_then [`nR - nF` ] assume_tac)
- \\ fs[]
- >- (
- `nF <= nR` by REAL_ASM_ARITH_TAC
- \\ `0 < nF` by REAL_ASM_ARITH_TAC
- \\ `0 < nR` by REAL_ASM_ARITH_TAC
- \\ `inv nR <= inv nF` by fs [REAL_INV_LE_ANTIMONO]
- \\ `inv nR - inv nF <= 0` by REAL_ASM_ARITH_TAC
- \\ `0 <= - (inv nR - inv nF) ` by REAL_ASM_ARITH_TAC
- \\ `abs (- (inv nR - inv nF)) = - (inv nR - inv nF)` by fs [ABS_REFL]
- \\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by metis_tac[ABS_NEG]
- \\ simp[real_sub, REAL_NEG_ADD]
- \\ rpt (qpat_x_assum `abs v = v'` kall_tac)
- \\ `- (inv nR) = inv (- nR)`
- by (fs [real_div] \\ irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
- \\ simp[]
- \\ qspec_then `inv (-nR) + inv (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
- >- (match_mp_tac REAL_LE_LADD_IMP
- \\ ‘0 < nR - err ∧ nR - err ≤ nF’ by REAL_ASM_ARITH_TAC
- \\ simp[])
- \\ `- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
- \\ ‘(nR - err + -nR) / (-nR * (nR - err)) ≤ err * (1 / (elo + -err) pow 2)’
- suffices_by (rewrite_tac[REAL_INV_1OVER] \\ fs[REAL_ADD_RAT])
- \\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
- \\ pop_assum (rewrite_tac o single)
- \\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
- \\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
- \\ ‘err * inv (nR * (nR − err)) ≤ err * inv ((elo + -err) pow 2)’
- by (
- match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
- \\ rpt (qpat_x_assum `T` kall_tac)
- \\ `0 < elo + - err` by REAL_ASM_ARITH_TAC
- \\ `0 < (elo + - err) * (elo + - err)` by fs[REAL_LT_MUL]
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- >- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
- \\ conj_tac
- >- (fs[POW_2])
- \\ once_rewrite_tac [POW_2] \\ irule REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC)
- \\ fs[REAL_INV_MUL'] \\ pop_assum mp_tac \\ fs[])
- >- (fs[]
- \\ `nR <= nF` by REAL_ASM_ARITH_TAC
- \\ `0 < nF` by REAL_ASM_ARITH_TAC
- \\ `0 < nR` by REAL_ASM_ARITH_TAC
- \\ `inv nF <= inv nR` by fs [REAL_INV_LE_ANTIMONO]
- \\ `0 <= inv nR - inv nF` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `inv nF <= inv nR` kall_tac
- \\ `abs (inv nR - inv nF) = inv nR - inv nF` by fs[ABS_REFL] \\ qpat_x_assum `0 <= inv a - b` kall_tac
- \\ simp [real_sub, REAL_NEG_ADD]
- \\ rpt (qpat_x_assum `abs x = y` kall_tac)
- \\ qspec_then `inv nR + - (inv (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
- >- (match_mp_tac REAL_LE_LADD_IMP
- \\ `0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
- \\ fs[GSYM REAL_INV_1OVER, REAL_INV_LE_ANTIMONO])
- >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
- \\ `- (inv (nR + err)) = inv (- (nR + err))`
- by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
- \\ pop_assum (rewrite_tac o single)
- \\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
- \\ `nR <> 0` by REAL_ASM_ARITH_TAC
- \\ rewrite_tac[REAL_INV_1OVER]
- \\ ‘1 / - (nR + err) = -1 / (nR + err)’ by (fs[neg_rat])
- \\ pop_assum (rewrite_tac o single)
- \\ ‘1 / nR + -1 / (nR + err) = (-(nR + err) + nR) / (nR * -(nR + err))’
- by (fs[REAL_ADD_RAT, real_div, REAL_MUL_LNEG, REAL_MUL_RNEG]
- \\ rewrite_tac[GSYM REAL_MUL_RNEG, REAL_NEG_ADD, REAL_NEG_NEG])
- \\ pop_assum (rewrite_tac o single)
- (* Goal: (-(nR + err) + nR) / (nR * -(nR + err)) ≤ err * (1 / (elo + -err) pow 2) *)
- \\ `- (nR + err) + nR = - err` by REAL_ASM_ARITH_TAC
- \\ pop_assum (rewrite_tac o single)
- \\ rewrite_tac[real_div, GSYM REAL_NEG_LMUL, REAL_NEG_RMUL]
- \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
- \\ fs [REAL_NEG_INV, REAL_NEG_RMUL, REAL_NEG_NEG]
- (* Goal: inv (nR * (nR + err)) ≤ inv ((elo + -err) pow 2)) *)
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- >- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
- \\ conj_tac \\ once_rewrite_tac [POW_2]
- >- (match_mp_tac REAL_LT_MUL
- \\ REAL_ASM_ARITH_TAC)
- \\ match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))
+ \\ ‘nR ≠0’ by REAL_ASM_ARITH_TAC
+ \\ ‘-nF ≠0’ by REAL_ASM_ARITH_TAC
+ \\ ‘inv nR - inv nF = - ((nR - nF) / (nR * nF))’
+ by (gs[real_div, real_sub] \\ rewrite_tac[realTheory.REAL_LDISTRIB, REAL_NEG_ADD]
+ \\ rewrite_tac [GSYM REAL_MUL_ASSOC]
+ \\ gs[REAL_MUL_LINV] \\ REAL_ASM_ARITH_TAC)
+ \\ pop_assum $ gs o single
+ \\ gs[real_div, Once REAL_ABS_MUL]
+ \\ irule REAL_LE_TRANS \\ qexists_tac ‘abs (inv nF * inv nR) * err’
+ \\ conj_tac \\ gs[] \\ irule REAL_LE_LMUL_IMP \\ gs[]
+ \\ ‘abs (inv nF * inv nR) = inv (abs (nF * nR))’ by gs[GSYM REAL_INV_MUL, ABS_INV]
+ \\ pop_assum $ rewrite_tac o single
+ \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ rewrite_tac [POW_2] \\ rpt conj_tac
+ >- gs[]
+ >- (irule REAL_LT_MUL \\ gs[])
+ \\ rewrite_tac [ABS_MUL]
+ \\ irule REAL_LE_MUL2 \\ gs[]
+ \\ rpt conj_tac
+ >- (irule REAL_LE_TRANS \\ qexists_tac ‘nF’ \\ gs[ABS_LE])
+ >- (irule REAL_LE_TRANS \\ qexists_tac ‘elo’ \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+ \\ REAL_ASM_ARITH_TAC
QED
Theorem err_prop_inversion_neg:
@@ -550,124 +491,26 @@ Theorem err_prop_inversion_neg:
abs (inv nR - inv nF) <= err * inv ((ehi + err) * (ehi + err))
Proof
rpt strip_tac
- \\ `! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)` by REAL_ASM_ARITH_TAC
- \\ qpat_x_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR - nF` ] DISJ_CASES_TAC thm)
- >- (fs []
- \\ `nF <= nR` by REAL_ASM_ARITH_TAC
- \\ `0 < -nF /\ nF <> 0` by REAL_ASM_ARITH_TAC
- \\ `0 < -nR /\ nR <> 0` by REAL_ASM_ARITH_TAC
- \\ `inv (- nF) <= inv (- nR)`
- by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- \\ REAL_ASM_ARITH_TAC)
- \\ `inv (- nF) - inv (- nR) <= 0` by REAL_ASM_ARITH_TAC
- \\ `0 <= - (inv (- nF) - inv (-nR)) ` by REAL_ASM_ARITH_TAC
- \\ `abs (- (inv (- nF) - inv (- nR))) = - (inv (- nF) - inv (- nR))` by fs [ABS_REFL]
- \\ `abs (inv (- nF) - inv (- nR)) = - (inv (- nF) - inv (- nR))` by metis_tac[ABS_NEG]
- \\ `inv (- nF) - inv (- nR) = inv nR - inv nF`
- by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
- \\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[]
- \\ simp[real_sub, REAL_NEG_ADD]
- \\ rpt (qpat_x_assum `abs v = v'` kall_tac)
- \\ `- (1 / nR) = 1 / - nR`
- by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
- \\ simp[]
- \\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
- >- (once_rewrite_tac [REAL_INV_1OVER]
- \\ pop_assum (rewrite_tac o single)
- \\ match_mp_tac REAL_LE_LADD_IMP
- \\ simp[GSYM REAL_INV_1OVER]
- \\ `nR - err <= nF` by REAL_ASM_ARITH_TAC
- \\ `- nF <= - (nR - err)` by REAL_ASM_ARITH_TAC
- \\ `inv (- (nR - err)) <= inv (- nF)` by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac \\ REAL_ASM_ARITH_TAC)
- \\ `0 <> nR - err` by REAL_ASM_ARITH_TAC
- \\ qpat_abbrev_tac `nRerr = nR - err`
- \\ once_rewrite_tac [GSYM REAL_LE_NEG]
- \\ `- inv (nRerr) = inv (- nRerr)` by (match_mp_tac REAL_NEG_INV \\ simp[])
- \\ `- inv (nF) = inv (- nF)` by (match_mp_tac REAL_NEG_INV \\ simp [])
- \\ qpat_x_assum `-(inv nRerr) = v` (fn thm => once_rewrite_tac [thm])
- \\ qpat_x_assum `-(inv nF) = v` (fn thm => once_rewrite_tac [thm])
- \\ simp[])
- >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
- \\ ‘1 / -nR + 1 / (nR - err) = (1 * (nR - err) + -nR * 1) / (-nR * (nR - err))’
- by (fs [REAL_ADD_RAT])
- \\ pop_assum (rewrite_tac o single)
- \\ rewrite_tac [REAL_MUL_LID, REAL_MUL_RID]
- \\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
- \\ pop_assum (rewrite_tac o single)
- \\ rewrite_tac [GSYM REAL_NEG_LMUL, real_div]
- \\ `nR <> 0` by REAL_ASM_ARITH_TAC
- \\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
- \\ fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
- \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
- \\ rpt (qpat_x_assum `T` kall_tac)
- \\ `0 < - (ehi + err)` by REAL_ASM_ARITH_TAC
- \\ `0 < - (ehi + err) * -(ehi + err)` by (match_mp_tac REAL_LT_MUL \\ fs[])
- \\ `0 < (ehi + err) * (ehi + err)` by REAL_ASM_ARITH_TAC
- \\ `0 < - nR * - (nR - err)` by (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
- \\ `0 < nR * (nR - err)` by REAL_ASM_ARITH_TAC
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac \\ TRY (REAL_ASM_ARITH_TAC)
- \\ conj_tac \\ once_rewrite_tac [POW_2] \\ TRY (REAL_ASM_ARITH_TAC)
- \\ qspec_then `(ehi + err) * (nR - err)` match_mp_tac real_le_trans2
- \\ conj_tac
- >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC)
- >- (`- (nR * (nR - err)) <= - ((ehi + err) * (nR - err))`
- by (once_rewrite_tac [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC)
- \\ REAL_ASM_ARITH_TAC)))
- \\ fs []
- \\ `nR <= nF` by REAL_ASM_ARITH_TAC
- \\ `0 < -nF /\ nF <> 0` by REAL_ASM_ARITH_TAC
- \\ `0 < -nR /\ nR <> 0` by REAL_ASM_ARITH_TAC
- \\ `inv (- nR) <= inv (- nF)`
- by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- \\ REAL_ASM_ARITH_TAC)
- \\ `inv (- nR) - inv (- nF) <= 0` by REAL_ASM_ARITH_TAC
- \\ `0 <= - (inv (- nR) - inv (-nR)) ` by REAL_ASM_ARITH_TAC
- \\ `abs (- (inv (- nR) - inv (- nF))) = - (inv (- nR) - inv (- nF))` by fs [ABS_REFL]
- \\ `abs (inv (- nR) - inv (- nF)) = - (inv (- nR) - inv (- nF))` by metis_tac[ABS_NEG]
- \\ `inv (- nR) - inv (- nF) = inv nF - inv nR` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
- \\ `abs (inv nF - inv nR) = - (inv (- nR) - inv (- nF))` by fs[]
- \\ `abs (inv nR - inv nF) = - (inv (- nR) - inv (- nF))` by fs[ABS_SUB]
- \\ simp[real_sub, REAL_NEG_ADD]
- \\ rpt (qpat_x_assum `abs v = v'` kall_tac)
- \\ `- (1 / nF) = 1 / - nF` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
- \\ simp[]
- \\ qspec_then `1 / -(nR + err) + 1 / nR` match_mp_tac real_le_trans2 \\ conj_tac
- >- (once_rewrite_tac [REAL_ADD_COMM] \\ rewrite_tac [REAL_INV_1OVER]
- \\ pop_assum (rewrite_tac o single)
- \\ match_mp_tac REAL_LE_LADD_IMP
- \\ `0 < - (nR + err) /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
- \\ simp [REAL_LE_NEG, REAL_INV_LE_ANTIMONO, REAL_MUL_LNEG])
- >- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
- \\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
- \\ ‘1 / - (nR + err) + 1 / nR = (1 * nR + - (nR + err) * 1) / (- (nR + err) * nR)’
- by (fs[REAL_ADD_RAT])
- \\ pop_assum (rewrite_tac o single)
- \\ rewrite_tac [REAL_MUL_RID, REAL_MUL_LID, real_div, GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
- \\ `nR + - (nR + err) = - err` by REAL_ASM_ARITH_TAC
- \\ pop_assum (rewrite_tac o single)
- \\ `inv (- ((nR + err) * nR)) = - (inv ((nR + err) * nR))`
- by (match_mp_tac (GSYM REAL_NEG_INV) \\ fs[] \\ REAL_ASM_ARITH_TAC)
- \\ pop_assum (rewrite_tac o single)
- \\ simp[GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL, REAL_NEG_NEG]
- \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
- \\ `0 < - (ehi + err)` by REAL_ASM_ARITH_TAC
- \\ `0 < - (ehi + err) * -(ehi + err)` by (match_mp_tac REAL_LT_MUL \\ fs[])
- \\ `0 < (ehi + err) * (ehi + err)` by REAL_ASM_ARITH_TAC
- \\ `0 < - nR * - (nR + err)` by (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
- \\ `0 < nR * (nR + err)` by REAL_ASM_ARITH_TAC
- \\ asm_rewrite_tac[GSYM REAL_NEG_RMUL]
- \\ once_rewrite_tac [REAL_MUL_COMM]
- \\ asm_rewrite_tac[REAL_NEG_INV, REAL_NEGNEG, GSYM REAL_INV_1OVER]
- \\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
- \\ once_rewrite_tac [POW_2] \\ TRY (REAL_ASM_ARITH_TAC)
- \\ conj_tac \\ TRY(REAL_ASM_ARITH_TAC)
- \\ qspec_then `(nR + err) * (ehi + err)` match_mp_tac real_le_trans2
- \\ conj_tac
- >- (once_rewrite_tac [REAL_MUL_COMM]
- \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC)
- \\ `- (nR * (nR + err)) <= - ((ehi + err) * (nR + err))`
- by (once_rewrite_tac [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC)
- \\ REAL_ASM_ARITH_TAC)
+ \\ ‘0 < (-ehi) + -err’ by REAL_ASM_ARITH_TAC
+ \\ qspecl_then [‘-nF’, ‘-nR’, ‘err’, ‘-ehi’, ‘-elo’] mp_tac err_prop_inversion_pos
+ \\ impl_tac
+ >- (
+ rpt conj_tac \\ TRY (gs[real_sub] \\ NO_TAC)
+ >- (gs[real_sub] \\ REAL_ASM_ARITH_TAC)
+ \\ REAL_ASM_ARITH_TAC)
+ \\ strip_tac
+ \\ ‘nR ≠0 ∧ nF ≠0’ by REAL_ASM_ARITH_TAC
+ \\ ‘abs (inv nR - inv nF) = abs (inv (-nR) - inv (- nF))’
+ by (gs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
+ \\ pop_assum $ rewrite_tac o single
+ \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ gs[]
+ \\ irule REAL_LE_LMUL_IMP \\ gs[]
+ \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ rpt conj_tac
+ >- (rewrite_tac[REAL_POW_POS] \\ DISJ2_TAC \\ DISJ1_TAC \\ gs[real_sub])
+ >- (rewrite_tac[REAL_POW_POS] \\ DISJ2_TAC \\ DISJ2_TAC \\ gs[])
+ \\ ‘-ehi - err = -1 * (ehi + err)’ by REAL_ASM_ARITH_TAC
+ \\ pop_assum $ rewrite_tac o single
+ \\ rewrite_tac [POW_MUL] \\ gs[POW_MINUS1]
QED
val _ = export_theory();
--
GitLab