Add a mock-up certificate checker

checkerDefsScript.sml

 open realTheory realLib RealArith stringTheory;
-open renameTheory realPolyTheory;
+open renameTheory realPolyTheory transcLangTheory;
 open preamble;
 
 val _ = new_theory"checkerDefs";
 
 Datatype:
-  certificate = <|
-    transc : real->real; (* transcendental function to be approximated *)
-    poly : poly;         (* real-number polynomial approximation *)
-    omega: real list;    (* the x_i's from Remez *)
-    eps: real            (* approximation error *)
-             |>
+  certificate =
+  <|
+    transc : transc;            (* transcendental function to be approximated *)
+    poly : poly;                (* real-number polynomial approximation *)
+    omega : real list;          (* the x_i's from Remez *)
+    eps : real;                 (* approximation error *)
+    iv: real # real;            (* the interval on which the function is approximated *)
+    zeroes : (real # real) list (* list of intervals in which a zero could be found *)
+   |>
 End
 
 Datatype:
-  result = VALID          (* the checker succeeded *)
-         | INVALID string (* the checker failed with an error message *)
+  result = Valid          (* the checker succeeded *)
+         | Invalid string (* the checker failed with an error message *)
 End
 
 Definition interpResult_def:

checkerScript.sml

@@ -3,17 +3,77 @@
   Dandelion
 **)
 open realTheory realLib RealArith stringTheory;
-open renameTheory realPolyTheory checkerDefsTheory pointCheckerTheory;
+open renameTheory realPolyTheory transcLangTheory sturmComputeTheory
+     checkerDefsTheory pointCheckerTheory;
 open preamble;
 
 val _ = new_theory "checker";
 
+(**
+  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) =
+  case transc of
+  | FUN "exp" VAR =>
+      if iv = (0, 0.5) then ([], 0) else ([], 0)
+  | _ => ([],0)
+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 numZeroes deriv zeroes =
+  if LENGTH zeroes ≠ numZeroes
+  then Invalid "Incorrect number of zeroes found"
+  else Valid
+End
+
+(**
+  Checks that the value at the extrema of the error polynomial are less than or
+  equal to the actual error encoded in the certificate **)
+(* TODO: Is this the correct way of checking the zeroes?? Check Harrison paper *)
+Definition validateZeroesLeqErr_def:
+  validateZeroesLeqErr diffPoly iv [] approxErr eps =
+    (if poly diffPoly (FST iv) + approxErr ≤ eps ∧ poly diffPoly (SND iv) + approxErr ≤ eps
+    then Valid
+    else Invalid "Outer points")
+  ∧
+  validateZeroesLeqErr diffPoly iv ((z1,z2)::zeroes) approxErr eps =
+    (if poly diffPoly z1 + approxErr ≤ eps ∧ poly diffPoly z2 + approxErr ≤ eps
+     then validateZeroesLeqErr diffPoly iv zeroes approxErr eps
+     else Invalid "Zero of derivate not an extremal point or extrema too big")
+End
+
+(**
+   Overall certificate checker combines all of the above functions into one that
+   runs over the full certificate **)
 Definition checker_def:
   checker (cert:certificate) :result =
-    let pointRes = pointChecker cert in
-    if pointRes = VALID then
-      INVALID "Not implemented"
-    else pointRes
+    case pointChecker cert of
+    | Invalid s => Invalid s
+    | Valid =>
+      let (transp, err) = approx cert.transc cert.iv;
+          errorp = transp -p cert.poly;
+          deriv = derive errorp
+      in
+        case sturm_seq errorp deriv of
+        NONE => Invalid "Could not compute sturm sequence"
+        | SOME sseq =>
+          let numZeroes =
+              (variation (MAP (λp. poly p (FST cert.iv)) sseq) -
+               variation (MAP (λp. poly p (SND cert.iv)) sseq));
+          in
+            case checkZeroes numZeroes deriv cert.zeroes of
+            | Valid =>
+                validateZeroesLeqErr errorp cert.iv cert.zeroes err cert.eps
+            | Invalid s => Invalid s
 End
 
 val _ = export_theory();

pointCheckerProofsScript.sml

@@ -10,7 +10,7 @@ val _ = new_theory "pointCheckerProofs";
 
 Theorem pointChecker_intermed:
   ∀ omega transc poly eps.
-    pointCheckerHelper omega transc poly eps = VALID ⇒
+    pointCheckerHelper omega transc poly eps = Valid ⇒
     ∀xi.
       MEM xi omega ⇒
       abs (evalPoly poly xi − transc xi) = eps
@@ -24,10 +24,10 @@ QED
 
 Theorem pointCheckerSound:
   ∀ (cert:certificate).
-    pointChecker cert = VALID ⇒
+    pointChecker cert = Valid ⇒
       ∀ xi.
         MEM xi cert.omega ⇒
-        abs ((evalPoly cert.poly xi) - cert.transc xi) = cert.eps
+        abs ((evalPoly cert.poly xi) - (λ x. interp cert.transc x) xi) = cert.eps
 Proof
  gs[pointChecker_def]
  >> rpt gen_tac >> cond_cases_tac >> gs[]

pointCheckerScript.sml

@@ -6,28 +6,25 @@
 **)
 
 open realTheory realLib RealArith stringTheory;
-open renameTheory realPolyTheory checkerDefsTheory;
+open renameTheory realPolyTheory transcLangTheory checkerDefsTheory;
 open preamble;
 
 val _ = new_theory "pointChecker";
 
 (* TODO: Check for each xi in Omega that p(xi) - f(xi) = cert.eps *)
 
-
 Definition pointCheckerHelper_def:
-  pointCheckerHelper [] transc poly eps = VALID ∧
+  pointCheckerHelper [] transc poly eps = Valid ∧
   pointCheckerHelper (x1::xs) transc poly eps =
     if (abs (evalPoly poly  x1 - transc x1) = eps)
     then  (pointCheckerHelper xs transc poly eps)
-    else INVALID "Point discrepancy"
+    else Invalid "Point discrepancy"
 End
 
-
-
 Definition pointChecker_def:
   pointChecker (cert:certificate): result =
-  if (LENGTH cert.omega = 0) then INVALID "Empty set" else
-  (pointCheckerHelper cert.omega cert.transc cert.poly cert.eps)
+  if (LENGTH cert.omega = 0) then Invalid "Empty set" else
+  (pointCheckerHelper cert.omega (λ x. interp cert.transc x) cert.poly cert.eps)
 End
 
 val _ = export_theory();

transcLangScript.sml

+(**
+  Define a simple "language" for describing transcendental
+  functions. For now we only allow combinations, i.e.
+  exp (sin (cos ...) but no additional operators like +,-,*,/
+**)
+open realTheory realLib RealArith transcTheory;
+open preamble;
+
+val _ = new_theory "transcLang";
+
+Datatype:
+  transc = FUN string transc | VAR
+End
+
+Definition getFun_def:
+  getFun s =
+  case s of
+    |"sqrt" => sqrt
+    | "exp" => exp
+    | "sin" => sin
+    | "cos" => cos
+    | "tan" => tan
+    | _ => λ x. x
+End
+
+Definition interp_def:
+  interp VAR x = x ∧
+  interp (FUN s trans) x =
+    (getFun s) (interp trans x)
+End
+
+val _ = export_theory();