diff --git a/checkerDefsScript.sml b/checkerDefsScript.sml
index a54a700be03bd94d29d437ec1984d3d9651cfe15..4299164aa9e6032dbe4b1f2cab0d007ec0b32a1b 100644
--- a/checkerDefsScript.sml
+++ b/checkerDefsScript.sml
@@ -1,21 +1,24 @@
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:
diff --git a/checkerScript.sml b/checkerScript.sml
index 52546e8379da76f3ad6b66f17cecb67c2c8efa29..4e4b78ccdf1e94dde308added283ff937ba7eea2 100644
--- a/checkerScript.sml
+++ b/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();
diff --git a/pointCheckerProofsScript.sml b/pointCheckerProofsScript.sml
index 77f715d1ba9e3e1c02bc936485d3e6d7f1f18388..96e63db295efbf3520ee655435055de94e23503e 100644
--- a/pointCheckerProofsScript.sml
+++ b/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[]
diff --git a/pointCheckerScript.sml b/pointCheckerScript.sml
index 947ec1f0f665e13645bb174e6824b5863d201287..6db9b5ae100acea0a32f8823a1ed561e6f05eaf5 100644
--- a/pointCheckerScript.sml
+++ b/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();
diff --git a/transcLangScript.sml b/transcLangScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..175c0f490321fc84a8526e50e8a20f64a54d9dce
--- /dev/null
+++ b/transcLangScript.sml
@@ -0,0 +1,32 @@
+(**
+ 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();