Commit c20bfa60 authored by Heiko Becker's avatar Heiko Becker

Draft for negative inversion error

parent 7ad77387
......@@ -265,5 +265,104 @@ qpat_x_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR - nF` ] DISJ_CASES_
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC)))));
DB.match [] `` -1 * (b:real)``
(** FIXME: Proof me
val err_prop_inversion_neg = store_thm ("err_prop_inversion_neg",
``!(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
ehi + err < 0 /\ ehi < 0 /\
abs (nR - nF) <= err /\
elo <= nR /\
nR <= ehi /\
elo - err <= nF /\
nF <= ehi + err /\
0 <= err ==>
abs (inv nR - inv nF) <= err * inv ((ehi + err) * (ehi + err))``,
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 fs [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_INV_1OVER, real_sub, REAL_NEG_ADD] \\
rpt (qpat_x_assum `abs v = v'` kall_tac) \\
`- (1 / nR) = 1 / - nR` by (fs [real_div] \\ ho_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
>- (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 \\ TRY 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 \\ fs [REAL_ADD_RAT] \\
`nR - err + - nR = - err` by REAL_ASM_ARITH_TAC \\
qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL \\
`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 \\ 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)
>- ( (** TODO **) )))
(** FIXME: UNDONE
>- (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 [GSYM 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_INV_1OVER, real_sub, REAL_NEG_ADD] \\
rpt (qpat_x_assum `abs x = y` kall_tac) \\
qspec_then `1 / nR + - (1 / (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP \\
simp [GSYM REAL_INV_1OVER, GSYM REAL_NEG_INV, REAL_LE_NEG] \\
`0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\
conj_tac \\ REAL_ASM_ARITH_TAC)
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\
`- (1 / (nR + err)) = 1 / - (nR + err)` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC) \\
`- (nR + err) <> 0` by REAL_ASM_ARITH_TAC \\
`nR <> 0` by REAL_ASM_ARITH_TAC \\
fs [REAL_ADD_RAT] \\
`- (nR + err) + nR = - err` by REAL_ASM_ARITH_TAC \\
qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL \\
simp [REAL_NEG_RMUL, REAL_NEG_INV] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[] \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC)))));
**)
**)
DB.match [] ``a * (b:real) <= c * d``
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