Add support for +, unary and binary - to approximations

checkerScript.sml

@@ -77,7 +77,7 @@ End
 Definition approxPoly_def:
   approxPoly transc (iv:real#real) (hs:hint list) approxSteps :(poly#real) option =
   case transc of
-  | FUN tr VAR =>
+  | Fun tr Var =>
       if tr = "exp" then
         case getExpHint hs of
           | NONE =>
@@ -93,6 +93,27 @@ Definition approxPoly_def:
       else if tr = "sin" then
         SOME (sin_poly approxSteps, sin_err iv approxSteps)
       else NONE
+  | Add tr1 tr2 =>
+      (case approxPoly tr1 iv hs approxSteps of
+      | NONE => NONE
+      | SOME (appr1, err1) =>
+          case approxPoly tr2 iv hs approxSteps of
+          | NONE => NONE
+          | SOME (appr2, err2) =>
+              SOME (appr1 +p appr2, err1 + err2))
+  | Sub tr1 tr2 =>
+      (case approxPoly tr1 iv hs approxSteps of
+      | NONE => NONE
+      | SOME (appr1, err1) =>
+          case approxPoly tr2 iv hs approxSteps of
+          | NONE => NONE
+          | SOME (appr2, err2) =>
+              SOME (appr1 -p appr2, err1 + err2))
+  | Neg tr1 =>
+      (case approxPoly tr1 iv hs approxSteps of
+      | NONE => NONE
+      | SOME (appr1, err1) =>
+          SOME (--p appr1, err1))
   | _ => NONE
 End
 
@@ -362,135 +383,171 @@ Theorem approxPoly_soundness:
       FST iv ≤ x ∧ x ≤ SND iv ⇒
       abs (interp transc x - evalPoly p x) ≤ err
 Proof
-  simp[approxPoly_def, approxPolySideCond_def, CaseEq"transc"]
+  ho_match_mp_tac approxPoly_ind
   >> rpt strip_tac
-  >> ‘(tr = "exp" ∧
-       ((iv = (0, 1 * inv 2) ∧ getExpHint hs = NONE) ∨
-        ∃ n. getExpHint hs = SOME n ∧ iv = (0,&n * inv 2))) ∨
-      tr = "cos" ∨
-      tr = "sin"’
-    by (every_case_tac >> gs[getExpHint_SOME_MEM])
-  (* exp function, 0 to 1/2 *)
-  >- (
-    gs[interp_def, getFun_def]
-    >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
-    >> pop_assum $ rewrite_tac o single
-    >> rpt VAR_EQ_TAC
-    >> rewrite_tac[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_small approxSteps = inv (&FACT approxSteps * 2 pow (approxSteps - 1))’ by EVAL_TAC
-    >> qspecl_then [‘approxSteps’, ‘x’,‘t’] mp_tac exp_remainder_bounded_small
-    >> impl_tac >> gs[]
-    >> real_tac)
-  (* exp function, 0 to 1 *)
-  >- (
-    gs[interp_def, getFun_def]
-    >> ‘1 ≠ inv 2’
-      by (once_rewrite_tac [GSYM REAL_INV1]
-          >> CCONTR_TAC
-          >> pop_assum $ mp_tac o SIMP_RULE std_ss []
-          >> rewrite_tac[REAL_INV_INJ] >> real_tac)
-    >> rpt VAR_EQ_TAC
-    >> rewrite_tac[GSYM poly_compat, eval_simps]
-    >> pop_assum $ rewrite_tac o single
-    >> rewrite_tac[exp_sum_to_poly]
-    >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
-    >> pop_assum $ rewrite_tac o single
-    >> 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_big n approxSteps = 2 pow n * &n pow approxSteps * inv (&FACT approxSteps * 2 pow approxSteps)’
-      by (rewrite_tac[] >> EVAL_TAC)
-    >> pop_assum $ rewrite_tac o single
-    >> qspecl_then [‘approxSteps’, ‘n’, ‘x’,‘t’] mp_tac exp_remainder_bounded_big
-    >> impl_tac
-    >- (rpt conj_tac >> gs[] >> real_tac)
-    >> rewrite_tac[])
-  (* cos function *)
+  >> qpat_x_assum ‘approxPoly _ _ _ _ = SOME _’ mp_tac
+  >> Cases_on ‘transc’ >> simp[Once approxPoly_def, CaseEq"transc", CaseEq"option", CaseEq"prod"]
+  >> rpt strip_tac >> gs[approxPolySideCond_def]
   >- (
-    gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
-    >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_COS_LE
+    ‘(s = "exp" ∧
+      ((iv = (0, 1 * inv 2) ∧ getExpHint hs = NONE) ∨
+       ∃ n. getExpHint hs = SOME n ∧ iv = (0,&n * inv 2))) ∨
+     s = "cos" ∨
+     s = "sin"’
+     by (every_case_tac >> gs[getExpHint_SOME_MEM])
+  (* exp function, 0 to 1/2 *)
+    >- (
+      gs[interp_def, getFun_def]
+      >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
+      >> pop_assum $ rewrite_tac o single
+      >> rpt VAR_EQ_TAC
+      >> rewrite_tac[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_small approxSteps = inv (&FACT approxSteps * 2 pow (approxSteps - 1))’ by EVAL_TAC
+      >> rename1 ‘exp t’
+      >> qspecl_then [‘approxSteps’, ‘x’,‘t’] mp_tac exp_remainder_bounded_small
+      >> impl_tac >> gs[]
+      >> real_tac)
+    (* exp function, 0 to 1 *)
+    >- (
+      gs[interp_def, getFun_def]
+      >> ‘1 ≠ inv 2’
+        by (once_rewrite_tac [GSYM REAL_INV1]
+            >> CCONTR_TAC
+            >> pop_assum $ mp_tac o SIMP_RULE std_ss []
+            >> rewrite_tac[REAL_INV_INJ] >> real_tac)
+      >> rpt VAR_EQ_TAC
+      >> rewrite_tac[GSYM poly_compat, eval_simps]
+      >> pop_assum $ rewrite_tac o single
+      >> rewrite_tac[exp_sum_to_poly]
+      >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
+      >> pop_assum $ rewrite_tac o single
+      >> 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_big n approxSteps = 2 pow n * &n pow approxSteps * inv (&FACT approxSteps * 2 pow approxSteps)’
+        by (rewrite_tac[] >> EVAL_TAC)
+      >> pop_assum $ rewrite_tac o single
+      >> qspecl_then [‘approxSteps’, ‘n’, ‘x’,‘t’] mp_tac exp_remainder_bounded_big
+      >> impl_tac
+      >- (rpt conj_tac >> gs[] >> real_tac)
+      >> rewrite_tac[])
+    (* cos function *)
+    >- (
+      gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
+      >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_COS_LE
+      >> gs[]
+      >> 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 approxSteps) * cos t * inv (&FACT approxSteps) =
+          (cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
+        by real_tac
+      >> ‘-(x pow approxSteps) * cos t * inv (&FACT approxSteps) =
+          -(cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
+        by real_tac
+      >> rewrite_tac []
+      >> ntac 2 $ pop_assum $ rewrite_tac o single
+      >> rewrite_tac [GSYM REAL_MUL_ASSOC]
+      >> qmatch_goalsub_abbrev_tac ‘abs (cos _ * err_cos_concr)’
+      >> irule REAL_LE_TRANS
+      >> qexists_tac ‘ 1 * abs err_cos_concr’ >> conj_tac
+      >- (rewrite_tac[ABS_MUL] >> irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[COS_BOUND, ABS_POS])
+      >> rewrite_tac[REAL_MUL_LID]
+      >> ‘abs err_cos_concr = err_cos_concr’
+        by (unabbrev_all_tac
+            >> rewrite_tac[ABS_REFL]
+            >> irule REAL_LE_MUL >> conj_tac
+            >- (irule REAL_LE_INV >> gs[REAL_POS])
+            >> irule REAL_LE_MUL >> conj_tac
+            >> gs[REAL_POW_GE0])
+      >> pop_assum $ rewrite_tac o single
+      >> unabbrev_all_tac
+      >> rewrite_tac [cos_err_def]
+      >> imp_res_tac EVEN_ODD_EXISTS >> gs[POW_MINUS1]
+      >> irule REAL_LE_LMUL_IMP >> gs[GSYM POW_ABS]
+      >> irule REAL_LE_TRANS
+      >> qexists_tac ‘abs (x pow (2 * m))’ >> gs[ABS_LE, 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’, ‘approxSteps’] strip_assume_tac MCLAURIN_SIN_LE
     >> gs[]
     >> 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 approxSteps) * cos t * inv (&FACT approxSteps) =
-        (cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
+    >> ‘inv (&FACT approxSteps) * sin t  * x pow approxSteps * -1 pow (approxSteps DIV 2) =
+        (sin t * ((x pow approxSteps) * inv (&FACT approxSteps) * -1 pow (approxSteps DIV 2)))’
       by real_tac
-    >> ‘-(x pow approxSteps) * cos t * inv (&FACT approxSteps) =
-        -(cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
+    >> ‘-(x pow approxSteps) * inv (&FACT approxSteps) * sin t =
+        -(sin t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
       by real_tac
     >> rewrite_tac []
     >> ntac 2 $ pop_assum $ rewrite_tac o single
-    >> rewrite_tac [GSYM REAL_MUL_ASSOC]
-    >> qmatch_goalsub_abbrev_tac ‘abs (cos _ * err_cos_concr)’
+    >> rewrite_tac[GSYM REAL_MUL_ASSOC]
+    >> qmatch_goalsub_abbrev_tac ‘_ * err_sin_concr’
+    >> rewrite_tac [ABS_NEG, Once ABS_MUL]
     >> irule REAL_LE_TRANS
-    >> qexists_tac ‘ 1 * abs err_cos_concr’ >> conj_tac
-    >- (rewrite_tac[ABS_MUL] >> irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[COS_BOUND, ABS_POS])
-    >> rewrite_tac[REAL_MUL_LID]
-    >> ‘abs err_cos_concr = err_cos_concr’
+    >> qexists_tac ‘ 1 * abs err_sin_concr’ >> conj_tac
+    >- (irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[SIN_BOUND, ABS_POS])
+    >> rewrite_tac [REAL_MUL_LID, sin_err_def, ABS_MUL]
+    >> ‘abs err_sin_concr = err_sin_concr’
       by (unabbrev_all_tac
           >> rewrite_tac[ABS_REFL]
           >> irule REAL_LE_MUL >> conj_tac
-          >- (irule REAL_LE_INV >> gs[REAL_POS])
-          >> irule REAL_LE_MUL >> conj_tac
-          >> gs[REAL_POW_GE0])
+          >> gs[REAL_POW_GE0]
+          >> irule REAL_LE_MUL >> gs[REAL_POS, REAL_POW_GE0])
     >> pop_assum $ rewrite_tac o single
     >> unabbrev_all_tac
-    >> rewrite_tac [cos_err_def]
+    >> rewrite_tac [sin_err_def]
     >> imp_res_tac EVEN_ODD_EXISTS >> gs[POW_MINUS1]
     >> irule REAL_LE_LMUL_IMP >> gs[GSYM POW_ABS]
     >> irule REAL_LE_TRANS
-    >> qexists_tac ‘abs (x pow (2 * m'))’ >> gs[ABS_LE, GSYM POW_ABS]
+    >> qexists_tac ‘abs (x pow (2 * m))’ >> gs[ABS_LE, 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’, ‘approxSteps’] strip_assume_tac MCLAURIN_SIN_LE
-  >> gs[]
-  >> pop_assum $ rewrite_tac o single
-  >> 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
-  >> ‘inv (&FACT approxSteps) * sin t  * x pow approxSteps * -1 pow (approxSteps DIV 2) =
-      (sin t * ((x pow approxSteps) * inv (&FACT approxSteps) * -1 pow (approxSteps DIV 2)))’
-    by real_tac
-  >> ‘-(x pow approxSteps) * inv (&FACT approxSteps) * sin t =
-      -(sin t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
-    by real_tac
-  >> rewrite_tac []
-  >> ntac 2 $ pop_assum $ rewrite_tac o single
-  >> rewrite_tac[GSYM REAL_MUL_ASSOC]
-  >> qmatch_goalsub_abbrev_tac ‘_ * err_sin_concr’
-  >> rewrite_tac [ABS_NEG, Once ABS_MUL]
-  >> irule REAL_LE_TRANS
-  >> qexists_tac ‘ 1 * abs err_sin_concr’ >> conj_tac
-  >- (irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[SIN_BOUND, ABS_POS])
-  >> rewrite_tac [REAL_MUL_LID, sin_err_def, ABS_MUL]
-  >> ‘abs err_sin_concr = err_sin_concr’
-    by (unabbrev_all_tac
-        >> rewrite_tac[ABS_REFL]
-        >> irule REAL_LE_MUL >> conj_tac
-        >> gs[REAL_POW_GE0]
-        >> irule REAL_LE_MUL >> gs[REAL_POS, REAL_POW_GE0])
+  >- (
+    rpt VAR_EQ_TAC
+    >> gs[interp_def, eval_simps]
+    >> qmatch_goalsub_abbrev_tac ‘abs (f_x + g_x - (f_poly_x + g_poly_x)) ≤ _’
+    >> ‘f_x + g_x - (f_poly_x + g_poly_x) = (f_x - f_poly_x) + (g_x - g_poly_x)’
+      by real_tac
+    >> pop_assum $ rewrite_tac o single
+    >> irule REAL_LE_TRANS
+    >> qexists_tac ‘abs (f_x - f_poly_x) + abs (g_x - g_poly_x)’
+    >> gs[REAL_ABS_TRIANGLE]
+    >> irule REAL_LE_ADD2 >> unabbrev_all_tac >> gs[])
+  >- (
+    rpt VAR_EQ_TAC
+    >> gs[interp_def, eval_simps]
+    >> qmatch_goalsub_abbrev_tac ‘abs (f_x - g_x - (f_poly_x - g_poly_x)) ≤ _’
+    >> ‘f_x - g_x - (f_poly_x - g_poly_x) = (f_x - f_poly_x) - (g_x - g_poly_x)’
+      by real_tac
+    >> pop_assum $ rewrite_tac o single
+    >> irule REAL_LE_TRANS
+    >> qexists_tac ‘abs (f_x - f_poly_x) + abs (- (g_x - g_poly_x))’
+    >> conj_tac
+    >- (rewrite_tac[real_sub] >> irule REAL_ABS_TRIANGLE)
+    >> gs[real_sub]
+    >> irule REAL_LE_ADD2 >> unabbrev_all_tac >> gs[])
+  >> rpt VAR_EQ_TAC
+  >> gs[interp_def, eval_simps, real_sub]
+  >> qmatch_goalsub_abbrev_tac ‘abs (- f_x + f_poly_x)’
+  >> ‘- f_x + f_poly_x = f_poly_x - f_x’ by real_tac
   >> pop_assum $ rewrite_tac o single
-  >> unabbrev_all_tac
-  >> rewrite_tac [sin_err_def]
-  >> imp_res_tac EVEN_ODD_EXISTS >> gs[POW_MINUS1]
-  >> irule REAL_LE_LMUL_IMP >> gs[GSYM POW_ABS]
-  >> irule REAL_LE_TRANS
-  >> qexists_tac ‘abs (x pow (2 * m'))’ >> gs[ABS_LE, GSYM POW_ABS]
-  >> irule POW_LE >> gs[ABS_POS]
-  >> irule RealSimpsTheory.maxAbs >> gs[]
+  >> once_rewrite_tac [ABS_SUB]
+  >> unabbrev_all_tac >> gs[real_sub]
 QED
 
 (*

transcLangScript.sml

@@ -9,7 +9,12 @@ open preamble;
 val _ = new_theory "transcLang";
 
 Datatype:
-  transc = FUN string transc | VAR
+  transc =
+    Fun string transc
+    | Add transc transc
+    | Sub transc transc
+    | Neg transc
+    | Var
 End
 
 Definition getFun_def:
@@ -24,8 +29,11 @@ Definition getFun_def:
 End
 
 Definition interp_def:
-  interp VAR x = x ∧
-  interp (FUN s trans) x =
+  interp Var x = x ∧
+  interp (Neg t) x = - (interp t x) ∧
+  interp (Add t1 t2) x = (interp t1 x) + (interp t2 x) ∧
+  interp (Sub t1 t2) x = (interp t1 x) - (interp t2 x) ∧
+  interp (Fun s trans) x =
     (getFun s) (interp trans x)
 End