Commit 58de5a60 authored by Heiko Becker's avatar Heiko Becker
Browse files

Rework an error bound proof

parent 39362c71
......@@ -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();
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