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

Add some doc with proofgoal shape to proofs

parent 06486055
......@@ -434,12 +434,15 @@ Proof
\\ 0 < nR - err nR - err nF by REAL_ASM_ARITH_TAC
\\ simp[GSYM REAL_INV_1OVER])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ fs [REAL_ADD_RAT]
\\ fs [REAL_ADD_RAT] (* 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)
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
(* Goal: -(err * inv (-(nR * (nR − err)))) ≤ err * inv ((elo + -err)pow 2) *)
\\ `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]
(* Goal: err * inv (nR * (nR − err)) ≤ err * inv ((elo + -err) pow 2) *)
\\ 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
......@@ -466,10 +469,11 @@ Proof
\\ `- (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]
\\ fs [REAL_ADD_RAT] (* Goal: (-(nR + err) + nR) / (nR * -(nR + err)) ≤ err * (1 / (elo + -err) pow 2) *)
\\ `- (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]
(* Goal: err * inv (nR * (nR + err)) ≤ err * inv ((elo + -err) pow 2) *)
\\ 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)
......
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