Implement a first version of checker with a complete soundness proof

checkerScript.sml

@@ -2,35 +2,48 @@
   CheckerScript: Define a Certificate Checker and a certificate structure for
   Dandelion
 **)
-open realTheory realLib RealArith stringTheory polyTheory;
+open realTheory realLib RealArith stringTheory polyTheory transcTheory;
 open renameTheory realPolyTheory transcLangTheory sturmComputeTheory sturmTheory
-     drangTheory checkerDefsTheory pointCheckerTheory;
+     drangTheory checkerDefsTheory pointCheckerTheory mcLaurinApproxTheory
+     realPolyProofsTheory;
 open preamble;
 
 val _ = new_theory "checker";
 
+Definition exp_steps_def[simp]:
+  exp_steps:num = 10
+End
+
+Definition exp_err_def:
+  exp_err = ^(EVAL “inv (&FACT exp_steps * 2 pow (exp_steps - 1))” |> concl |> rhs)
+End
+
+Definition exp_poly_cst:
+  exp_poly_cst = ^(EVAL “exp_poly exp_steps” |> concl |> rhs)
+End
+
 (**
   Approximate a function described by transcLang with a real-number polynomial,
   also returns the approximation error
 **)
 (* TODO: Approximate transcendental functions on a case-by-case basis *)
 Definition approx_def:
-  approx transc (iv:real#real) :(poly#real) =
+  approx transc (iv:real#real) :(poly#real) option =
   case transc of
-  | FUN "exp" VAR =>
-      if iv = (0, 0.5) then ([], 0) else ([], 0)
-  | _ => ([],0)
+  | FUN tr VAR =>
+      if (iv = (0, 0.5) ∧ tr = "exp") then
+        SOME (exp_poly_cst, exp_err)
+      else NONE
+  | _ => NONE
 End
 
-
 (**
   Checks that the zero intervals encoded in the certificate actually are
   all of the zeroes of derivative of the difference between the approximated
   polynomial and the transcendental function
 **)
-(* TODO: Is this sufficient for a check? *)
 Definition checkZeroes_def:
-  checkZeroes deriv1 deriv2 iv sseq zeroes =
+  checkZeroes deriv1 deriv2 iv sseq (zeroes:(real#real) list) =
   let numZeroes =
       (variation (MAP (λp. poly p (FST iv)) (deriv1::deriv2::sseq)) -
        variation (MAP (λp. poly p (SND iv)) (deriv1::deriv2::sseq)))
@@ -91,29 +104,27 @@ End
    runs over the full certificate **)
 Definition checker_def:
   checker (cert:certificate) :result =
-    case pointChecker cert of
-    | Invalid s => Invalid s
-    | Valid =>
-      let (transp, err) = approx cert.transc cert.iv;
-          errorp = transp -p cert.poly;
-          deriv1 = diff errorp;
-          deriv2 = diff deriv1
-      in
-        case sturm_seq deriv1 deriv2 of
-        NONE => Invalid "Could not compute sturm sequence"
-        | SOME sseq =>
-            case checkZeroes deriv1 deriv2 cert.iv sseq cert.zeroes of
-            | Valid =>
-                validateZeroesLeqErr deriv1 cert.iv cert.zeroes (cert.eps - err)
-            | Invalid s => Invalid s
+    case approx cert.transc cert.iv of
+    | NONE => Invalid "Could not find appropriate approximation"
+    | SOME (transp, err) =>
+        let errorp = transp -p cert.poly;
+            deriv1 = diff errorp;
+        in
+          case sturm_seq deriv1 (diff deriv1) of
+            NONE => Invalid "Could not compute sturm sequence"
+          | SOME sseq =>
+              case checkZeroes deriv1 (diff deriv1) cert.iv sseq cert.zeroes of
+              | Valid =>
+                  validateZeroesLeqErr errorp cert.iv cert.zeroes (cert.eps - err)
+              | Invalid s => Invalid s
 End
 
 Theorem checkZeroes_sound:
-  ! sseq deriv1 deriv2 iv zeroes.
-    sturm_seq deriv1 (diff deriv1) = SOME sseq /\
-    checkZeroes deriv1 (diff deriv1) iv sseq zeroes = Valid /\
-    FST iv <= SND iv ==>
-    {x | FST iv <= x /\ x <= SND iv /\ (poly deriv1 x = &0)} HAS_SIZE
+  ∀ sseq deriv1 iv zeroes.
+    sturm_seq deriv1 (diff deriv1) = SOME sseq ∧
+    checkZeroes deriv1 (diff deriv1) iv sseq zeroes = Valid ∧
+    FST iv ≤ SND iv ⇒
+    {x | FST iv ≤ x ∧ x ≤ SND iv ∧ (poly deriv1 x = &0)} HAS_SIZE
                                                          LENGTH zeroes
 Proof
   rpt gen_tac
@@ -241,12 +252,60 @@ Proof
 QED
 
 Theorem checker_soundness:
-  ! cert.
-    checker cert = Valid ==>
-    ! x. FST(cert.iv) <= x /\ x <= SND (cert.iv) ==>
-         (interp cert.transc x - poly cert.poly x) <= cert.eps
+  ∀ cert.
+    checker cert = Valid ⇒
+    ∀ x.
+      FST(cert.iv) ≤ x ∧ x ≤ SND (cert.iv) ⇒
+      abs (interp cert.transc x - poly cert.poly x) ≤ cert.eps
 Proof
-  cheat
+  rpt strip_tac
+  >> gs[checker_def, approx_def, CaseEq"option", CaseEq"prod", CaseEq"result",
+        CaseEq"transc", interp_def, getFun_def]
+  (* Step 1: Approximate the transcendental fun with its taylor series *)
+  >> irule REAL_LE_TRANS
+  >> qexists_tac ‘abs (exp x - poly exp_poly_cst x) + abs (poly exp_poly_cst x - poly cert.poly x)’
+  >> conj_tac
+  (* Approximation using triangle inequality *)
+  >- (
+    ‘exp x - poly cert.poly x = (exp x - poly exp_poly_cst x) + (poly exp_poly_cst x - poly cert.poly x)’
+    by real_tac
+    >> pop_assum $ rewrite_tac o single
+    >> irule REAL_ABS_TRIANGLE)
+  >> ‘cert.eps = exp_err + (cert.eps - exp_err)’ by real_tac
+  >> pop_assum $ once_rewrite_tac o single
+  >> irule REAL_LE_ADD2 >> reverse conj_tac
+  >- (
+    gs[GSYM poly_compat, GSYM eval_simps]
+    >> rewrite_tac [poly_compat]
+    >> irule validateZeroesLeqErr_sound
+    >> qexists_tac ‘diff (exp_poly_cst -p cert.poly)’ >> gs[]
+    >> qexists_tac ‘(0, 1/2)’ >> gs[]
+    >> qexists_tac ‘cert.zeroes’ >> gs[]
+    >> drule checkZeroes_sound
+    >> disch_then drule >> gs[])
+  (* Now prove the Taylor series error
+  TODO: Make separate soundness proof *)
+  >> qspecl_then [‘x’, ‘exp_steps’] strip_assume_tac MCLAURIN_EXP_LE
+  >> pop_assum $ rewrite_tac o single
+  >> ‘poly exp_poly_cst x = evalPoly (exp_poly exp_steps) x’
+     by (gs[poly_compat] >> EVAL_TAC)
+  >> pop_assum $ rewrite_tac o single
+  >> gs[exp_sum_to_poly]
+  >> qmatch_goalsub_abbrev_tac ‘abs (exp_taylor + taylor_rem - exp_taylor) ≤ _’
+  >> ‘exp_taylor + taylor_rem - exp_taylor = taylor_rem’ by real_tac
+  >> pop_assum $ rewrite_tac o single
+  >> unabbrev_all_tac
+  >> ‘exp_err = inv (&FACT exp_steps * 2 pow (exp_steps - 1))’ by EVAL_TAC
+  >> pop_assum $ rewrite_tac o single
+  >> qspecl_then [‘exp_steps’, ‘x’,‘t’] mp_tac exp_remainder_bounded
+  >> impl_tac >> gs[] >> reverse conj_tac
+  >- gs[REAL_INV_1OVER]
+  >> gs[abs] >> Cases_on ‘0 ≤ t’
+  >- (
+    irule REAL_LE_TRANS  >> qexists_tac ‘x’ >> gs[REAL_INV_1OVER])
+  >> irule REAL_LE_TRANS >> qexists_tac ‘-t’ >> conj_tac >- real_tac
+  >> irule REAL_LE_TRANS >> qexists_tac ‘x’
+  >> gs[REAL_INV_1OVER]
 QED
 
 val _ = export_theory();

expBoundScript.sml

-open realTheory realLib RealArith transcTheory;
-open renameTheory;
-open preamble;
-
-val _ = new_theory "expBound";
-
-
-(*** Prove lemma for bound on exp in the interval, x ∈ [0, 0.5]
-based on John Harrison's paper **)
-
-Theorem REAL_LE_RCANCEL_IMP:
-  ∀ x y z:real.
-    &0 < z ∧
-    x * z ≤ y * z ⇒
-    x ≤ y
-Proof
-  rpt strip_tac
-  >> assume_tac REAL_LE_LMUL
-  >> pop_assum $ qspecl_then [‘z’, ‘x’, ‘y’] assume_tac
-  >> gs[]
-QED
-
-Theorem REAL_EXP_BOUND_LEMMA:
-  ∀ x.
-    &0 ≤ x ∧ x ≤ inv 2 ⇒
-    exp(x) ≤ &1 + &2 * x
-Proof
-  rpt strip_tac >> irule REAL_LE_TRANS
-  >> qexists_tac ‘suminf (λ n. x pow n)’ >> conj_tac
-  >- (
-    gs[exp] >> irule seqTheory.SER_LE
-    >> gs[seqTheory.summable] >> rpt conj_tac
-    >- (
-      rpt strip_tac
-      >> jrhUtils.GEN_REWR_TAC RAND_CONV [GSYM REAL_MUL_LID]
-      >> irule REAL_LE_RMUL_IMP >> gs[POW_POS]
-      >> irule REAL_INV_LE_1
-      >> gs[REAL_OF_NUM_LE, LESS_EQ_IFF_LESS_SUC]
-      >> ‘1 = SUC 0’ by gs[]
-      >> pop_assum $ rewrite_tac o single
-      >> gs[LESS_MONO_EQ, FACT_LESS])
-    >- (qexists_tac ‘exp x’ >> gs[BETA_RULE EXP_CONVERGES] )
-    >> qexists_tac ‘inv (1 - x)’
-    >> irule seqTheory.GP
-    >> gs[abs] >> irule REAL_LET_TRANS >> qexists_tac ‘inv 2’
-    >> conj_tac >> gs[])
-  >> ‘suminf (λ n. x pow n) = inv (1 - x)’
-     by (
-      irule $ GSYM seqTheory.SUM_UNIQ
-      >> irule seqTheory.GP
-      >> gs[abs] >> irule REAL_LET_TRANS >> qexists_tac ‘inv 2’
-      >> conj_tac >> gs[])
-  >> pop_assum $ rewrite_tac o single
-  >> irule REAL_LE_RCANCEL_IMP
-  >> qexists_tac ‘1 - x’
-  >> ‘1 - x ≠ 0’ by (CCONTR_TAC >> gs[])
-  >> simp[REAL_MUL_LINV]
-  >> conj_tac
-  >- (
-    irule REAL_LET_TRANS >> qexists_tac ‘inv 2 - x’
-    >> rewrite_tac[REAL_ARITH “&0 <= x:real - y <=> y <= x”]
-    >> rewrite_tac[REAL_ARITH “a - x < b - x <=> a < b:real”]
-    >> gs[])
-  >> gs[REAL_SUB_LDISTRIB, REAL_ADD_LDISTRIB]
-  >> rewrite_tac[POW_2,
-                 REAL_ARITH “&1 <= &1 + &2 * x:real - (x + &2 * (x * x)) <=>
-                             x * (&2 * x) <= x * &1”]
-  >> irule REAL_LE_LMUL_IMP >> gs[]
-  >> irule REAL_LE_RCANCEL_IMP >> qexists_tac ‘inv 2’
-  >> rewrite_tac[REAL_MUL_LID, REAL_ARITH “2 * x * inv 2 = x:real * (2 * inv 2)”]
-  >> gs[REAL_MUL_RINV]
-QED
-
-Theorem  REAL_EXP_MINUS1_BOUND_LEMMA:
-  !x. &0 <= x /\ x <= inv(&2) ==> &1 - exp(-x) <= &2 * x
-Proof
-  REPEAT STRIP_TAC >> REWRITE_TAC[REAL_LE_SUB_RADD]
-  >> ONCE_REWRITE_TAC[REAL_ADD_SYM]
-  >> REWRITE_TAC[GSYM REAL_LE_SUB_RADD]
-  >> irule REAL_LE_RCANCEL_IMP
-  >> EXISTS_TAC “exp(x)” >>  REWRITE_TAC[GSYM EXP_ADD]
-  >> REWRITE_TAC[REAL_ADD_LINV, EXP_0, EXP_POS_LT]
-  >> MATCH_MP_TAC REAL_LE_TRANS
-  >> EXISTS_TAC “(&1 - &2 * (x:real)) * (&1 + &2 * x)”
-  >> CONJ_TAC
-  >- ( irule REAL_LE_LMUL_IMP >> reverse conj_tac
-       >- ( REWRITE_TAC[REAL_LE_SUB_LADD, REAL_ADD_LID]
-            >> MATCH_MP_TAC REAL_LE_TRANS
-            >> EXISTS_TAC “&2 * inv(&2)”
-            >> reverse CONJ_TAC
-            >- gs[]
-            >> irule REAL_LE_LMUL_IMP >> gs[]
-          )
-       >> MATCH_MP_TAC REAL_EXP_BOUND_LEMMA >> gs[]
-     )
-  >> ONCE_REWRITE_TAC[REAL_MUL_SYM]
-  >> REWRITE_TAC[REAL_DIFFSQ]
-  >> REWRITE_TAC[REAL_MUL_LID, REAL_LE_SUB_RADD, EXP_NEG_MUL]
-  >> REWRITE_TAC[REAL_LE_ADDR]
-  >> MATCH_MP_TAC REAL_LE_MUL >> REWRITE_TAC[]
-  >> MATCH_MP_TAC REAL_LE_MUL >> gs[]
-QED
-
-val _ = export_theory();

mclaurenScript.sml → mcLaurinApproxScript.sml

@@ -3,9 +3,10 @@ in the transcLang file **)
 
 
 open realTheory realLib RealArith transcTheory arithmeticTheory;
+open realPolyTheory realPolyProofsTheory;
 open preamble;
 
-val _ = new_theory "mclauren";
+val _ = new_theory "mcLaurinApprox";
 
 Theorem SUCC_minus_1:
   ∀m. 0 < m ⇒ (SUC m DIV 2) = (m-1) DIV 2 + 1
@@ -32,9 +33,6 @@ Proof
   >> gs[ADD_DIV_RWT, REAL_POW_ADD]
 QED
 
-
-
-
 Theorem MCLAURIN_SIN_LE:
   ∀ x n. ∃t. abs(t) ≤ abs (x) ∧
              (\n. if EVEN n then
@@ -113,6 +111,45 @@ Proof
   >> gs[]
 QED
 
+Theorem sin_even_remainder_bounded:
+  ∀ n.
+    EVEN n ⇒
+    inv (&FACT n) * sin t * x pow n * -1 pow (n DIV 2) ≤
+    abs(inv (&FACT n) * x pow n * -1 pow (n DIV 2))
+Proof
+  rpt strip_tac
+  >> ‘inv (&FACT n) * x pow n * -1 pow (n DIV 2) = inv (&FACT n) * 1 * x pow n * -1 pow (n DIV 2)’
+     by real_tac
+  >> pop_assum $ rewrite_tac o single
+  >> rewrite_tac[GSYM REAL_MUL_ASSOC]
+  >> once_rewrite_tac[REAL_ABS_MUL]
+  >> ‘0 ≤ inv (&FACT n)’
+     by gs[REAL_LE_INV]
+  >> ‘abs (inv (&FACT n)) = inv (&FACT n)’ by gs[abs]
+  >> pop_assum $ rewrite_tac o single
+  >> irule REAL_LE_LMUL_IMP
+  >> reverse conj_tac >- gs[]
+  >> once_rewrite_tac[REAL_ABS_MUL]
+  >> Cases_on ‘0 ≤ x pow n * -1 pow (n DIV 2)’
+  >- (
+    ‘abs (x pow n * -1 pow (n DIV 2)) = x pow n * -1 pow (n DIV 2)’ by gs[abs]
+    >> pop_assum $ rewrite_tac o single
+    >> irule REAL_LE_RMUL_IMP >> gs[SIN_BOUNDS])
+  >> ‘x pow n * -1 pow (n DIV 2) < 0’ by real_tac
+  >> irule REAL_LE_TRANS
+  >> qexists_tac ‘-1 * (x pow n * -1 pow (n DIV 2))’
+  >> conj_tac
+  >- (
+    once_rewrite_tac [REAL_MUL_COMM]
+    >> drule REAL_LE_LMUL_NEG
+    >> disch_then $ qspecl_then [‘sin t’, ‘-1’] $ rewrite_tac o single
+    >> gs[SIN_BOUNDS])
+  >> ‘∃ y. x pow n * -1 pow (n DIV 2) = -1 * y ∧ 0 ≤ y’
+    by (qexists_tac ‘-1 * x pow n * -1 pow (n DIV 2)’
+        >> real_tac)
+  >> qpat_x_assum `_ = -1 * y` $ rewrite_tac o single
+  >> gs[ABS_LE]
+QED
 
 Theorem MCLAURIN_COS_LE:
   ∀ x n. ∃t. abs(t) ≤ abs (x) ∧
@@ -189,6 +226,171 @@ Proof
   >> gs[]
 QED
 
+(*** Prove lemma for bound on exp in the interval, x ∈ [0, 0.5]
+based on John Harrison's paper **)
 
+Theorem REAL_LE_RCANCEL_IMP:
+  ∀ x y z:real.
+    &0 < z ∧
+    x * z ≤ y * z ⇒
+    x ≤ y
+Proof
+  rpt strip_tac
+  >> assume_tac REAL_LE_LMUL
+  >> pop_assum $ qspecl_then [‘z’, ‘x’, ‘y’] assume_tac
+  >> gs[]
+QED
+
+Theorem REAL_EXP_BOUND_LEMMA:
+  ∀ x.
+    &0 ≤ x ∧ x ≤ inv 2 ⇒
+    exp(x) ≤ &1 + &2 * x
+Proof
+  rpt strip_tac >> irule REAL_LE_TRANS
+  >> qexists_tac ‘suminf (λ n. x pow n)’ >> conj_tac
+  >- (
+    gs[exp] >> irule seqTheory.SER_LE
+    >> gs[seqTheory.summable] >> rpt conj_tac
+    >- (
+      rpt strip_tac
+      >> jrhUtils.GEN_REWR_TAC RAND_CONV [GSYM REAL_MUL_LID]
+      >> irule REAL_LE_RMUL_IMP >> gs[POW_POS]
+      >> irule REAL_INV_LE_1
+      >> gs[REAL_OF_NUM_LE, LESS_EQ_IFF_LESS_SUC]
+      >> ‘1 = SUC 0’ by gs[]
+      >> pop_assum $ rewrite_tac o single
+      >> gs[LESS_MONO_EQ, FACT_LESS])
+    >- (qexists_tac ‘exp x’ >> gs[BETA_RULE EXP_CONVERGES] )
+    >> qexists_tac ‘inv (1 - x)’
+    >> irule seqTheory.GP
+    >> gs[abs] >> irule REAL_LET_TRANS >> qexists_tac ‘inv 2’
+    >> conj_tac >> gs[])
+  >> ‘suminf (λ n. x pow n) = inv (1 - x)’
+     by (
+      irule $ GSYM seqTheory.SUM_UNIQ
+      >> irule seqTheory.GP
+      >> gs[abs] >> irule REAL_LET_TRANS >> qexists_tac ‘inv 2’
+      >> conj_tac >> gs[])
+  >> pop_assum $ rewrite_tac o single
+  >> irule REAL_LE_RCANCEL_IMP
+  >> qexists_tac ‘1 - x’
+  >> ‘1 - x ≠ 0’ by (CCONTR_TAC >> gs[])
+  >> simp[REAL_MUL_LINV]
+  >> conj_tac
+  >- (
+    irule REAL_LET_TRANS >> qexists_tac ‘inv 2 - x’
+    >> rewrite_tac[REAL_ARITH “&0 <= x:real - y <=> y <= x”]
+    >> rewrite_tac[REAL_ARITH “a - x < b - x <=> a < b:real”]
+    >> gs[])
+  >> gs[REAL_SUB_LDISTRIB, REAL_ADD_LDISTRIB]
+  >> rewrite_tac[POW_2,
+                 REAL_ARITH “&1 <= &1 + &2 * x:real - (x + &2 * (x * x)) <=>
+                             x * (&2 * x) <= x * &1”]
+  >> irule REAL_LE_LMUL_IMP >> gs[]
+  >> irule REAL_LE_RCANCEL_IMP >> qexists_tac ‘inv 2’
+  >> rewrite_tac[REAL_MUL_LID, REAL_ARITH “2 * x * inv 2 = x:real * (2 * inv 2)”]
+  >> gs[REAL_MUL_RINV]
+QED
+
+Theorem  REAL_EXP_MINUS1_BOUND_LEMMA:
+  !x. &0 <= x /\ x <= inv(&2) ==> &1 - exp(-x) <= &2 * x
+Proof
+  REPEAT STRIP_TAC >> REWRITE_TAC[REAL_LE_SUB_RADD]
+  >> ONCE_REWRITE_TAC[REAL_ADD_SYM]
+  >> REWRITE_TAC[GSYM REAL_LE_SUB_RADD]
+  >> irule REAL_LE_RCANCEL_IMP
+  >> EXISTS_TAC “exp(x)” >>  REWRITE_TAC[GSYM EXP_ADD]
+  >> REWRITE_TAC[REAL_ADD_LINV, EXP_0, EXP_POS_LT]
+  >> MATCH_MP_TAC REAL_LE_TRANS
+  >> EXISTS_TAC “(&1 - &2 * (x:real)) * (&1 + &2 * x)”
+  >> CONJ_TAC
+  >- ( irule REAL_LE_LMUL_IMP >> reverse conj_tac
+       >- ( REWRITE_TAC[REAL_LE_SUB_LADD, REAL_ADD_LID]
+            >> MATCH_MP_TAC REAL_LE_TRANS
+            >> EXISTS_TAC “&2 * inv(&2)”
+            >> reverse CONJ_TAC
+            >- gs[]
+            >> irule REAL_LE_LMUL_IMP >> gs[]
+          )
+       >> MATCH_MP_TAC REAL_EXP_BOUND_LEMMA >> gs[]
+     )
+  >> ONCE_REWRITE_TAC[REAL_MUL_SYM]
+  >> REWRITE_TAC[REAL_DIFFSQ]
+  >> REWRITE_TAC[REAL_MUL_LID, REAL_LE_SUB_RADD, EXP_NEG_MUL]
+  >> REWRITE_TAC[REAL_LE_ADDR]
+  >> MATCH_MP_TAC REAL_LE_MUL >> REWRITE_TAC[]
+  >> MATCH_MP_TAC REAL_LE_MUL >> gs[]
+QED
+
+Definition exp_poly_def:
+  exp_poly 0 = [] ∧ (* x pow 0 * inv FACT 0 *)
+  exp_poly (SUC n) = (exp_poly n) ++ [inv (&FACT n)]
+End
+
+Theorem exp_poly_LENGTH:
+  LENGTH (exp_poly n) = n
+Proof
+  Induct_on ‘n’ >> gs[exp_poly_def]
+QED
+
+Theorem exp_sum_to_poly:
+  ∀ n x. evalPoly (exp_poly n) x = sum (0,n) (λ m. x pow m / &FACT m)
+Proof
+  Induct_on ‘n’ >> gs[exp_poly_def, evalPoly_def, sum]
+  >> rpt strip_tac >> gs[evalPoly_app, evalPoly_def, exp_poly_LENGTH]
+QED
+
+Theorem exp_remainder_bounded:
+  ∀ n x t.
+    0 < n ∧ abs t ≤ abs x ∧ 0 ≤ x ∧
+    t ≤ inv 2 ∧ x ≤ inv 2 ⇒
+    abs (exp t / &FACT n * x pow n) ≤ inv (&FACT n * 2 pow (n - 1))
+Proof
+  rpt strip_tac >> rewrite_tac[real_div, abs]
+  >> qmatch_goalsub_abbrev_tac ‘(if 0 ≤ exp_bound then _ else _) ≤ _’
+  >> ‘0 ≤ exp_bound’
+    by (
+    unabbrev_all_tac
+    >> rpt (irule REAL_LE_MUL >> gs[POW_POS, EXP_POS_LE]))
+  >> simp[] >> unabbrev_all_tac
+  >> irule REAL_LE_TRANS
+  >> qexists_tac ‘(1 + 2 * inv 2) * (inv (&FACT n) * x pow n)’
+  >> conj_tac
+  >- (
+    rewrite_tac[GSYM REAL_MUL_ASSOC]
+    >> irule REAL_LE_RMUL_IMP
+    >> conj_tac
+    >- (
+      Cases_on ‘0 ≤ t’
+      >- (
+        irule REAL_LE_TRANS
+        >> qexists_tac ‘1 + 2 * t’ >> conj_tac
+        >- (irule REAL_EXP_BOUND_LEMMA >> gs[])
+        >> real_tac)
+      >> ‘t = - (- t)’ by real_tac
+      >> pop_assum $ once_rewrite_tac o single
+      >> once_rewrite_tac[EXP_NEG]
+      >> ‘- (inv 2) ≤ -t’ by real_tac
+      >> irule REAL_LE_TRANS
+      >> qexists_tac ‘inv (exp (- (inv 2)))’
+      >> conj_tac
+      >- (irule REAL_INV_LE_ANTIMONO_IMPR >> gs[EXP_POS_LT, EXP_MONO_LE])
+      >> rewrite_tac[EXP_NEG, REAL_INV_INV]
+      >> irule REAL_EXP_BOUND_LEMMA >> gs[])
+    >> irule REAL_LE_MUL >> gs[REAL_LE_INV, POW_POS])
+  >> ‘1 + 2 * inv 2 = 2’ by gs[]
+  >> pop_assum $ rewrite_tac o single
+  >> rewrite_tac[GSYM REAL_MUL_ASSOC, REAL_INV_MUL']
+  >> irule REAL_LE_TRANS
+  >> qexists_tac ‘2 * (inv (&FACT n) * inv 2 pow n)’
+  >> conj_tac
+  >- (
+    irule REAL_LE_LMUL_IMP >> reverse conj_tac >- gs[]
+    >> irule REAL_LE_LMUL_IMP >> reverse conj_tac >- gs[REAL_LE_INV]
+    >> irule POW_LE >> gs[])
+  >> Cases_on ‘n’ >- gs[]
+  >> rewrite_tac[pow]
+  >> gs[REAL_INV_MUL']
+QED
 
 val _ = export_theory();

realPolyProofsScript.sml

@@ -1863,5 +1863,13 @@ Proof
   >> gs[poly_add_def, poly_add_aux_def, reduce_idempotent]
 QED
 
+Theorem evalPoly_app:
+  ∀ p1 p2 x. evalPoly (p1 ++ p2) x = evalPoly p1 x + evalPoly p2 x * x pow (LENGTH p1)
+Proof
+  Induct_on ‘p1’ >> gs[evalPoly_def]
+  >> rpt strip_tac >> pop_assum kall_tac
+  >> gs[REAL_LDISTRIB, pow]
+  >> real_tac
+QED
 
 val _ = export_theory();