First version of sin

checkerScript.sml

@@ -54,6 +54,17 @@ Definition cos_poly_cst_def:
   cos_poly_cst = ^(cos_poly_cst_EVAL_THM |> concl |> rhs)
 End
 
+Theorem sin_err_EVAL_THM = EVAL “inv (&FACT approx_steps)”
+Theorem sin_poly_cst_EVAL_THM = EVAL “sin_poly approx_steps” |> SIMP_RULE std_ss [one_inv_one, REAL_MUL_LID, mul_neg_one]
+
+Definition sin_err_def:
+  sin_err iv = (max (abs (FST iv)) (abs (SND iv))) pow approx_steps * ^(sin_err_EVAL_THM |> concl |> rhs)
+End
+
+Definition sin_poly_cst_def:
+  sin_poly_cst = ^(sin_poly_cst_EVAL_THM |> concl |> rhs)
+End
+
 (**
   Approximate a function described by transcLang with a real-number polynomial,
   also returns the approximation error
@@ -75,6 +86,8 @@ Definition approxPoly_def:
          else NONE
       else if tr = "cos" then
         SOME (cos_poly_cst, cos_err iv)
+      else if tr = "sin" then
+        SOME (sin_poly_cst, sin_err iv)
       else NONE
   | _ => NONE
 End
@@ -348,7 +361,8 @@ Proof
   >> ‘(tr = "exp" ∧
        ((cert.iv = (0, 1 * inv 2) ∧ getExpHint cert.hints = NONE) ∨
         ∃ n. getExpHint cert.hints = SOME n ∧ cert.iv = (0,&n * inv 2))) ∨
-      tr = "cos"’
+      tr = "cos" ∨
+      tr = "sin"’
     by (every_case_tac >> gs[getExpHint_SOME_MEM])
   (* exp function, 0 to 1/2 *)
   >- (
@@ -396,36 +410,73 @@ Proof
     >- (rpt conj_tac >> gs[] >> real_tac)
     >> rewrite_tac[approx_steps_def])
   (* cos function *)
+  >- (
+    gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
+    >> qspecl_then [‘x’, ‘approx_steps’] strip_assume_tac MCLAURIN_COS_LE
+    >> gs[]
+    >> pop_assum $ rewrite_tac o single
+    >> ‘poly cos_poly_cst x = evalPoly (cos_poly approx_steps) x’
+      by (rewrite_tac [GSYM approx_steps_def, cos_poly_cst_EVAL_THM]
+          >> gs[poly_compat, cos_poly_cst_def])
+    >> pop_assum $ rewrite_tac o single
+    >> gs[cos_sum_to_poly]
+    >> qmatch_goalsub_abbrev_tac ‘abs (cos_taylor + taylor_rem - cos_taylor) ≤ _’
+    >> ‘cos_taylor + taylor_rem - cos_taylor = taylor_rem’ by real_tac
+    >> pop_assum $ rewrite_tac o single
+    >> unabbrev_all_tac
+    >> ‘(x pow approx_steps) * cos t * inv (&FACT approx_steps) =
+        (cos t * ((x pow approx_steps) * inv (&FACT approx_steps)))’
+      by real_tac
+    >> ‘-(x pow approx_steps) * cos t * inv (&FACT approx_steps) =
+        -(cos t * ((x pow approx_steps) * inv (&FACT approx_steps)))’
+      by real_tac
+    >> rewrite_tac [GSYM approx_steps_def]
+    >> ntac 2 $ pop_assum $ rewrite_tac o single
+    >> rewrite_tac [ABS_NEG, Once ABS_MUL]
+    >> qmatch_goalsub_abbrev_tac ‘_ * err_cos_concr’
+    >> irule REAL_LE_TRANS
+    >> qexists_tac ‘ 1 * err_cos_concr’ >> conj_tac
+    >- (irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[COS_BOUND, ABS_POS])
+    >> unabbrev_all_tac
+    >> rewrite_tac [REAL_MUL_LID, cos_err_def, ABS_MUL]
+    >> ‘abs (inv (&FACT approx_steps)) = inv (&FACT approx_steps)’
+      by (rewrite_tac[abs] >>  EVAL_TAC >> gs[])
+    >> pop_assum $ rewrite_tac o single
+    >> rewrite_tac[EVAL “(inv (&FACT approx_steps))”, ABS_MUL, real_div, REAL_MUL_LID]
+    >> irule REAL_LE_RMUL_IMP >> gs[GSYM POW_ABS]
+    >> irule POW_LE >> gs[ABS_POS]
+    >> irule RealSimpsTheory.maxAbs >> gs[])
+  (* sin *)
   >> gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
-  >> qspecl_then [‘x’, ‘approx_steps’] strip_assume_tac MCLAURIN_COS_LE
+  >> qspecl_then [‘x’, ‘approx_steps’] strip_assume_tac MCLAURIN_SIN_LE
   >> gs[]
   >> pop_assum $ rewrite_tac o single
-  >> ‘poly cos_poly_cst x = evalPoly (cos_poly approx_steps) x’
-    by (rewrite_tac [GSYM approx_steps_def, cos_poly_cst_EVAL_THM]
-        >> gs[poly_compat, cos_poly_cst_def])
+  >> ‘poly sin_poly_cst x = evalPoly (sin_poly approx_steps) x’
+    by (rewrite_tac [GSYM approx_steps_def, sin_poly_cst_EVAL_THM]
+        >> gs[poly_compat, sin_poly_cst_def])
   >> pop_assum $ rewrite_tac o single
-  >> gs[cos_sum_to_poly]
-  >> qmatch_goalsub_abbrev_tac ‘abs (cos_taylor + taylor_rem - cos_taylor) ≤ _’
-  >> ‘cos_taylor + taylor_rem - cos_taylor = taylor_rem’ by real_tac
+  >> gs[sin_sum_to_poly]
+  >> qmatch_goalsub_abbrev_tac ‘abs (sin_taylor + taylor_rem - sin_taylor) ≤ _’
+  >> ‘sin_taylor + taylor_rem - sin_taylor = taylor_rem’ by real_tac
   >> pop_assum $ rewrite_tac o single
   >> unabbrev_all_tac
-  >> ‘(x pow approx_steps) * cos t * inv (&FACT approx_steps) =
-      (cos t * ((x pow approx_steps) * inv (&FACT approx_steps)))’
-     by real_tac
-  >> ‘-(x pow approx_steps) * cos t * inv (&FACT approx_steps) =
-      -(cos t * ((x pow approx_steps) * inv (&FACT approx_steps)))’
-     by real_tac
+  >> ‘(x pow approx_steps) * inv (&FACT approx_steps) * sin t  =
+      (sin t * ((x pow approx_steps) * inv (&FACT approx_steps)))’
+    by real_tac
+  >> ‘-(x pow approx_steps) * inv (&FACT approx_steps) * sin t =
+      -(sin t * ((x pow approx_steps) * inv (&FACT approx_steps)))’
+    by real_tac
   >> rewrite_tac [GSYM approx_steps_def]
   >> ntac 2 $ pop_assum $ rewrite_tac o single
   >> rewrite_tac [ABS_NEG, Once ABS_MUL]
-  >> qmatch_goalsub_abbrev_tac ‘_ * err_cos_concr’
+  >> qmatch_goalsub_abbrev_tac ‘_ * err_sin_concr’
   >> irule REAL_LE_TRANS
-  >> qexists_tac ‘ 1 * err_cos_concr’ >> conj_tac
-  >- (irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[COS_BOUND, ABS_POS])
+  >> qexists_tac ‘ 1 * err_sin_concr’ >> conj_tac
+  >- (irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[SIN_BOUND, ABS_POS])
   >> unabbrev_all_tac
-  >> rewrite_tac [REAL_MUL_LID, cos_err_def, ABS_MUL]
+  >> rewrite_tac [REAL_MUL_LID, sin_err_def, ABS_MUL]
   >> ‘abs (inv (&FACT approx_steps)) = inv (&FACT approx_steps)’
-     by (rewrite_tac[abs] >>  EVAL_TAC >> gs[])
+    by (rewrite_tac[abs] >>  EVAL_TAC >> gs[])
   >> pop_assum $ rewrite_tac o single
   >> rewrite_tac[EVAL “(inv (&FACT approx_steps))”, ABS_MUL, real_div, REAL_MUL_LID]
   >> irule REAL_LE_RMUL_IMP >> gs[GSYM POW_ABS]

mcLaurinApproxScript.sml

@@ -34,22 +34,26 @@ Proof
 QED
 
 Theorem MCLAURIN_SIN_LE:
-  ∀ x n. ∃t. abs(t) ≤ abs (x) ∧
-             (\n. if EVEN n then
-                    (sin x = sum(0,n)
-                                (λm.
-                                 (&FACT m)⁻¹ * x pow m *
-                                 if EVEN m then sin 0 * -1 pow (m DIV 2)
-                                 else cos 0 * -1 pow ((m − 1) DIV 2)) +
-                              (&FACT n)⁻¹ * sin t * x pow n * -1 pow (n DIV 2))
-                  else
-                    (sin x = sum (0,n)
-                                 (λm.
-                                    (&FACT m)⁻¹ * x pow m *
-                                    if EVEN m then sin 0 * -1 pow (m DIV 2)
-                                    else cos 0 * -1 pow ((m − 1) DIV 2)) +
-                             cos t * (&FACT n)⁻¹ * x pow n *
-                             -1 pow ((n − 1) DIV 2))) n
+  ∀ x n.
+    ∃t.
+      abs(t) ≤ abs (x) ∧
+      (\n. if EVEN n then
+             (sin x =
+              sum(0,n)
+                 (λm.
+                    inv (&FACT m) * x pow m *
+                    if EVEN m then sin 0 * -1 pow (m DIV 2)
+                    else cos 0 * -1 pow ((m − 1) DIV 2)) +
+              inv (&FACT n) * sin t * x pow n * -1 pow (n DIV 2))
+           else
+             (sin x =
+              sum (0,n)
+                  (λm.
+                     inv (&FACT m) * x pow m *
+                     if EVEN m then sin 0 * -1 pow (m DIV 2)
+                     else cos 0 * -1 pow ((m − 1) DIV 2)) +
+              cos t * inv (&FACT n) * x pow n *
+              -1 pow ((n − 1) DIV 2))) n
 Proof
   rpt strip_tac
   >> assume_tac MCLAURIN_ALL_LE
@@ -254,9 +258,7 @@ Theorem REAL_LE_RCANCEL_IMP:
     x ≤ y
 Proof
   rpt strip_tac
-  >> assume_tac REAL_LE_LMUL
-  >> pop_assum $ qspecl_then [‘z’, ‘x’, ‘y’] assume_tac
-  >> gs[]
+  >> gs[REAL_LE_LMUL]
 QED
 
 Theorem REAL_EXP_BOUND_LEMMA:
@@ -537,4 +539,73 @@ Proof
   >> gs[ABS_LE]
 QED
 
+(** sin **)
+Definition sin_poly_def:
+  sin_poly 0 = [] ∧
+  sin_poly (SUC n) =
+    if (EVEN n) then sin_poly n ++ [0]
+    else sin_poly n ++ [-1 pow ((n - 1) DIV 2) * inv (&FACT n)]
+End
+
+Theorem LENGTH_sin_poly:
+  LENGTH (sin_poly n) = n
+Proof
+  Induct_on ‘n’ >> gs[sin_poly_def]
+  >> cond_cases_tac >> gs[]
+QED
+
+Theorem sin_sum_to_poly:
+  ∀ n x.
+    evalPoly (sin_poly n) x =
+    sum(0,n)
+       (λm.
+          (&FACT m)⁻¹ * x pow m *
+          if EVEN m then sin 0 * -1 pow (m DIV 2)
+          else cos 0 * -1 pow ((m - 1) DIV 2))
+Proof
+  Induct_on ‘n’ >> gs[sum, evalPoly_def, sin_poly_def]
+  >> cond_cases_tac
+  >> gs[evalPoly_app, SIN_0, COS_0, evalPoly_def, LENGTH_sin_poly]
+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
+
 val _ = export_theory();