Make checkers more verbose to find errors easier, make example explicitly store theorem

checkerScript.sml

@@ -54,8 +54,8 @@ End
   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) option =
+Definition approxPoly_def:
+  approxPoly transc (iv:real#real) :(poly#real) option =
   case transc of
   | FUN tr VAR =>
       if (iv = (0, 1 * inv 2) ∧ tr = "exp") then
@@ -77,8 +77,12 @@ Definition checkZeroes_def:
       (variation (MAP (λp. poly p (FST iv)) (deriv1::deriv2::sseq)) -
        variation (MAP (λp. poly p (SND iv)) (deriv1::deriv2::sseq)))
   in
-    if (LENGTH zeroes <> numZeroes \/ poly deriv1 (FST iv) = 0 \/ poly deriv1 (SND iv) = 0)
-    then Invalid "Incorrect number of zeroes found"
+    if (LENGTH zeroes ≠ numZeroes) then
+      Invalid "Incorrect number of zeroes found"
+    else if (poly deriv1 (FST iv) = 0) then
+      Invalid "Lower bound of derivative is 0"
+    else if (poly deriv1 (SND iv) = 0) then
+      Invalid "Upper bound of derivative is 0"
     else Valid
 End
 
@@ -112,20 +116,21 @@ End
   to be validated.
 **)
 Definition validateZeroesLeqErr_def:
-  validateZeroesLeqErr diffPoly iv zeroes eps =
+  validateZeroesLeqErr errorp iv zeroes eps =
     let mAbs = max (abs (FST iv)) (abs (SND iv));
-        B = poly (MAP abs (diff diffPoly)) mAbs;
+        B = poly (MAP abs (diff errorp)) mAbs;
         e = getMaxWidth zeroes;
-        ub = getMaxAbsLb diffPoly zeroes
+        ub = getMaxAbsLb errorp zeroes
     in
-      if (abs (poly diffPoly (FST iv)) ≤ ub + B * e ∧
-          abs (poly diffPoly (SND iv)) ≤ ub + B * e ∧
-          validBounds iv zeroes ∧
-          EVERY (λ (u,v). poly (diff diffPoly) u * poly (diff diffPoly) v ≤ 0) zeroes ∧
-          recordered (FST iv) zeroes (SND iv))
-      then
+      if ~ (abs (poly errorp (FST iv)) ≤ ub + B * e) then
+        Invalid "Lower bound greater than verifiable error"
+      else if ~(abs (poly errorp (SND iv)) ≤ ub + B * e) then
+        Invalid "Upper bound greater than verifiable error"
+      else if validBounds iv zeroes ∧
+          EVERY (λ (u,v). poly (diff errorp) u * poly (diff errorp) v ≤ 0) zeroes ∧
+          recordered (FST iv) zeroes (SND iv) then
         isValid (ub + B * e ≤ eps) "Bounding error too large"
-      else Invalid "Outer points bigger than error"
+      else Invalid "Could not validate all zeros"
 End
 
 (**
@@ -133,19 +138,20 @@ End
    runs over the full certificate **)
 Definition checker_def:
   checker (cert:certificate) :result =
-    case approx cert.transc cert.iv of
+    case approxPoly 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
+      let 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 errorp cert.iv cert.zeroes (cert.eps - err)
+            | Invalid s => Invalid s
 End
 
 Theorem checkZeroes_sound:
@@ -159,7 +165,7 @@ Proof
   rpt gen_tac
   >> rewrite_tac[checkZeroes_def]
   >> CONV_TAC $ DEPTH_CONV let_CONV
-  >> cond_cases_tac >- gs[]
+  >> rpt (cond_cases_tac >- gs[])
   >> rpt $ pop_assum $ mp_tac o SIMP_RULE std_ss []
   >> rpt strip_tac
   >> qpat_x_assum ‘LENGTH zeroes = _’ $ rewrite_tac o single
@@ -288,7 +294,7 @@ Theorem checker_soundness:
       abs (interp cert.transc x - poly cert.poly x) ≤ cert.eps
 Proof
   rpt strip_tac
-  >> gs[checker_def, approx_def, CaseEq"option", CaseEq"prod", CaseEq"result",
+  >> gs[checker_def, approxPoly_def, CaseEq"option", CaseEq"prod", CaseEq"result",
         CaseEq"transc"] >> rpt VAR_EQ_TAC
   (* Step 1: Approximate the transcendental fun with its taylor series *)
   >> irule REAL_LE_TRANS
@@ -370,7 +376,7 @@ Proof
   >> ‘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]
+  >> 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[]

examples/mockUpScript.sml

@@ -35,6 +35,11 @@ poly := [
   |>
 End
 
+val _ = computeLib.add_thms [REAL_INV_1OVER] computeLib.the_compset;
+val _ = computeLib.add_funs [polyTheory.poly_diff_def, polyTheory.poly_diff_aux_def, polyTheory.poly_def]
+
+Theorem checkerSucceeds = EVAL “checker exp_example”
+
 (* Definition narrowStep_def: *)
 (*   narrowStep (l,h):(real#real) : (real#real) = *)
 (*   let dist = (h - l); *)
@@ -116,7 +121,6 @@ val res4 = Parse.Term ‘MAP (λ(u,v). poly (diff ^errorp) u * poly (diff ^error
 val res5 = Parse.Term ‘recordered (FST exp_example.iv) exp_example.zeroes (SND exp_example.iv)’ |> EVAL
 val res6 = Parse.Term ‘^ub + ^B * ^e1 ≤ (exp_example.eps - ^err)’ |> EVAL
 
-EVAL “checker exp_example”
 *)
 
 val _ = export_theory();