From eadccab4e8b648d47f38cc59daed4ca1f4140781 Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Tue, 12 Jan 2021 16:53:10 +0100
Subject: [PATCH] Add some doc with proofgoal shape to proofs

---
 hol4/ErrorBoundsScript.sml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index f488aa05..4d8597d9 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -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)
-- 
GitLab