Add some dummy definitions

Holmakefile

-#INCLUDES = ""
-OPTIONS = QUIT_ON_FAILURE
+INCLUDES = $(FLOVERDIR)/hol4/semantics $(HOLDIR)/examples/algebra/polynomial

checkerDefsScript.sml

+open realTheory realLib RealArith stringTheory;
+open renameTheory realPolyTheory;
+open preamble;
+
+val _ = new_theory"checkerDefs";
+
+Datatype:
+  certificate = <|
+    transc : real->real;
+    poly : poly;
+    omega: real list;
+    delta: real
+             |>
+End
+
+Datatype:
+  result = VALID | INVALID string
+End
+
+Definition interpResult_def:
+  interpResult (VALID) = T ∧
+  interpResult _ = F
+End
+
+val _ = export_theory();

checkerScript.sml

+(**
+  CheckerScript: Define a Certificate Checker and a certificate structure for
+  Dandelion
+**)
+open realTheory realLib RealArith stringTheory;
+open renameTheory realPolyTheory checkerDefsTheory pointCheckerTheory;
+open preamble;
+
+val _ = new_theory "checker";
+
+Definition checker_def:
+  checker (cert:certificate) :result =
+    let pointRes = pointChecker cert in
+    if pointRes = VALID then
+      INVALID "Not implemented"
+    else pointRes
+End
+
+val _ = export_theory();

floverConnScript.sml

+(**
+  Connection to FloVer roundoff error analyzer
+**)
+
+open ExpressionsTheory ExpressionSemanticsTheory realPolyTheory
+open preamble;
+
+val _ = new_theory "floverConn";
+
+Definition poly2FloVer_def:
+  poly2FloVer []:real expr = Const REAL 0 ∧
+  poly2FloVer (c1::cs) = Binop Plus (Const REAL c1) (Binop Mult (Var 0) (poly2FloVer cs))
+End
+
+Theorem polyEval_implies_FloVer_eval:
+  ∀ (p:poly) (x:real) (r:real).
+    evalPoly p x = r ⇒
+    eval_expr (λ v:num. if v = 0 then SOME x else NONE) (λ e:real expr. SOME REAL) (poly2FloVer p) r REAL
+Proof
+  Induct_on ‘p’ >> gs[evalPoly_def, eval_expr_rules, poly2FloVer_def]
+  >> rpt strip_tac
+  >- (
+    irule Const_dist' >> gs[]
+    >> qexists_tac ‘0’ >> gs[perturb_def, MachineTypeTheory.mTypeToR_pos])
+  >> irule Binop_dist'
+  >> qexists_tac ‘0’ >> gs[perturb_def, MachineTypeTheory.mTypeToR_pos, MachineTypeTheory.isJoin_def]
+  >> ntac 2 $ qexists_tac ‘REAL’
+  >> qexists_tac ‘h’ >> qexists_tac ‘x * evalPoly p x’
+  >> gs[evalBinop_def, MachineTypeTheory.isFixedPoint_def, MachineTypeTheory.join_fl_def]
+  >> conj_tac
+  >- (
+    irule Const_dist' >> gs[]
+    >> qexists_tac ‘0’ >> gs[perturb_def, MachineTypeTheory.mTypeToR_pos])
+  >> irule Binop_dist'
+  >> qexists_tac ‘0’ >> gs[perturb_def, MachineTypeTheory.mTypeToR_pos, MachineTypeTheory.isJoin_def]
+  >> ntac 2 $ qexists_tac ‘REAL’
+  >> qexists_tac ‘x’ >> qexists_tac ‘evalPoly p x’
+  >> gs[evalBinop_def, MachineTypeTheory.isFixedPoint_def, MachineTypeTheory.join_fl_def]
+  >> irule Var_load >> gs[]
+QED
+
+Theorem FloVer_eval_real_typed:
+  ∀ p r x m.
+    eval_expr (λ v:num. if v = 0 then SOME x else NONE) (λ e. SOME REAL) (poly2FloVer p) r m ⇒
+    m = REAL
+Proof
+  Induct_on `p` \\ rpt strip_tac \\ gs[poly2FloVer_def, Once eval_expr_cases]
+QED
+
+Theorem FloVer_eval_implies_polyEval:
+  ∀ p x r.
+    eval_expr (λ v:num. if v = 0 then SOME x else NONE) (λ e. SOME REAL) (poly2FloVer p) r REAL ⇒
+    evalPoly p x = r
+Proof
+  Induct_on ‘p’ >> gs[evalPoly_def, eval_expr_cases, poly2FloVer_def]
+  >> rpt strip_tac
+  >- gs[perturb_def]
+  >> qpat_x_assum `r = _` $ gs o single
+  >> gs[perturb_def]
+  >> imp_res_tac FloVer_eval_real_typed >> gs[]
+  >> res_tac >> gs[evalBinop_def]
+QED
+
+Theorem evalPoly_Flover_eval_bisim:
+  ∀ p x r.
+    evalPoly p x = r ⇔
+    eval_expr (λ v:num. if v = 0 then SOME x else NONE) (λ e. SOME REAL) (poly2FloVer p) r REAL
+Proof
+  rpt strip_tac >> EQ_TAC >> gs[FloVer_eval_implies_polyEval, polyEval_implies_FloVer_eval]
+QED
+
+val _ = export_theory();

pointCheckerScript.sml

+(**
+  A simple checker for polynomial evaluation
+  Part one of the soundness proof requires showing that the approximated
+  polynomial agrees with what Remez thought the trancendental function behaves
+  like on the set of points Ω
+**)
+
+open realTheory realLib RealArith stringTheory;
+open renameTheory realPolyTheory checkerDefsTheory;
+open preamble;
+
+val _ = new_theory "pointChecker";
+
+Definition pointChecker_def:
+  pointChecker (cert:certificate): result = INVALID"Not implemented"
+End
+
+val _ = export_theory();

preamble.sml

@@ -16,15 +16,14 @@ open ASCIInumbersTheory BasicProvers Defn HolKernel Parse SatisfySimps Tactic
      wordsTheory;
 (* TOOD: move? *)
 val wf_rel_tac = WF_REL_TAC
-val induct_on = Induct_on
-val cases_on = Cases_on;
-val every_case_tac = BasicProvers.EVERY_CASE_TAC;
-val full_case_tac = BasicProvers.FULL_CASE_TAC;
 val sym_sub_tac = SUBST_ALL_TAC o SYM;
-fun asm_match q = Q.MATCH_ASSUM_RENAME_TAC q
 val match_exists_tac = part_match_exists_tac (hd o strip_conj)
 val asm_exists_tac = first_assum(match_exists_tac o concl)
-val has_pair_type = can dest_prod o type_of
+val cond_cases_tac = COND_CASES_TAC
+val top_case_tac = TOP_CASE_TAC
+val real_tac = RealArith.REAL_ASM_ARITH_TAC
+val eq_tac = EQ_TAC
+val eval_tac = EVAL_TAC
 fun impl_subgoal_tac th =
   let
     val hyp_to_prove = lhand (concl th)

realPolyScript.sml

 (**
   Definition of datatype for real-valued polynomials
+
+  We formalize univariate polynomials only. Currently HOL4 only supports
+  derivatives of univariate polynomials, and therefore adding
+  multivariate polynomials would significantly increase the complexity
+  of the project.
 **)
-open realTheory
+open realTheory realLib RealArith renameTheory;
 open preamble;
 
 val _ = new_theory "realPoly";
 
-Type env = “:(string # real) list”
+(**
+  We follow the "standard" formalizations used in the HOL family,
+  a polynomial p = c_0 * x^0 + c_1 * x^1 + c_2 * x^2 + ...
+  is expressed as the list of real numbers [c_0; c_1; c_2; ...]
+**)
+Type poly = “:real list”
 
-Definition envLookup_def:
-  envLookup (x:string) (E:env) =
-    FIND (λ (y,r). x = y) E
+(* Evaluation of a polynomial *)
+Definition evalPoly_def:
+  evalPoly [] x = 0:real ∧
+  evalPoly (c::cs) x = c + (x * evalPoly cs x)
 End
 
-Definition envAppend_def:
-  envAppend (E:env) (x:string) (r:real) =
-    (x,r)::E
+(* Normalization; remove trailing zeroes *)
+Definition normalize_def:
+  normalize []:poly = [] ∧
+  normalize (c::cs) =
+    (let normalCs = normalize cs in
+    if normalCs = [] then
+       if c = 0 then [] else [c]
+     else c::normalCs)
 End
 
-Datatype:
-  bop = Add | Sub | Mul | Div
+(* Smart constructors for constants and variables *)
+Definition cst_def:
+  cst (c:real):poly = if c = 0 then [] else [c]
 End
 
-Datatype:
-  uop = Neg
+Definition var_def:
+  var (0:num):poly = [1] ∧
+  var (SUC n) = 0::(var n)
 End
 
-Datatype:
-  poly =
-    Var string
-    | Const real
-    | Uop uop poly
-    | Bop bop poly poly
+(* Negation, Addition, Subtraction, Multiplication with constants,
+polynomial multiplication *)
+Definition poly_add_aux_def:
+  poly_add_aux [] p2:poly = p2 ∧
+  poly_add_aux (c1::cs1) p2 =
+    case p2 of
+    | [] => (c1::cs1)
+    | (c2::cs2) => (c1+c2):: poly_add_aux cs1 cs2
 End
 
-Definition evalUop_def:
-  evalUop Neg (r:real) = - r
+Definition poly_add_def:
+  poly_add p1 p2 = normalize (poly_add_aux p1 p2)
 End
 
-val _ = enable_monadsyntax();
-val _ = monadsyntax.enable_monad "option";
+Definition poly_mul_cst_aux_def:
+  poly_mul_cst_aux c []:poly = [] ∧
+  poly_mul_cst_aux c (c1::cs) = (c * c1) :: poly_mul_cst_aux c cs
+End
 
-(** TODO: Turn this into a function defined using equations **)
-Definition evalPoly_def:
-  evalPoly (p:poly) (E:env) =
-    (case p of
-    | Const r => SOME r
-    | Var x =>
-      do
-      (y,r) <- envLookup x E;
-      return r
-      od
-    | Uop u p =>
-      do
-        r <- evalPoly p E;
-        return (evalUop u r);
-      od
-    | Bop b p1 p2 => NONE)
+Definition poly_mul_cst_def:
+  poly_mul_cst c p = normalize (poly_mul_cst_aux c p)
+End
+
+Definition poly_neg_def:
+  poly_neg p = poly_mul_cst (-1) p
+End
+
+Definition poly_mul_def:
+  poly_mul [] p2 = [] ∧
+  poly_mul (c1::cs1) p2 =
+    poly_add (poly_mul_cst c1 p2) (if cs1 = [] then [] else 0::(poly_mul cs1 p2))
+End
+
+Definition poly_exp_def:
+  poly_exp p 0 = [1]:poly ∧
+  poly_exp p (SUC n) = poly_mul p (poly_exp p n)
+End
+
+Definition derive_aux_def:
+  derive_aux n ([]:poly) = [] ∧
+  derive_aux n (c::cs) = (&n * c) :: derive_aux n cs
 End
 
-Definition vars_def:
-vars (Const _) = ∅ ∧
-vars (Var s) = { s } ∧
-vars (Uop u p) = vars p ∧
-vars (Bop b p1 p2) = (vars p1) ∪ (vars p2)
+Definition derive_def:
+  derive (l:poly) = normalize (if l = [] then [] else derive_aux 1 (TL l))
 End
 
-Theorem evalPoly_total:
-  ∀ p E.
-    (∀ x. x IN (vars p) ⇒
-     ∃ r. envLookup x E = SOME (x,r)) ⇒
-    ∃ r.
-    evalPoly p E = SOME r
+Definition degree_def:
+  deg(p:poly) = LENGTH (normalize p) - 1
+End
+
+val _ = map Parse.overload_on [
+    ("--p", Term ‘poly_neg’),
+    ("+p", Term ‘poly_add’),
+    ("-p", Term ‘λ (x:poly) (y:poly). poly_add x (poly_neg y)’),
+    ("*p", Term ‘poly_mul’),
+    ("*c", Term ‘poly_mul_cst’),
+    ("**p", Term ‘poly_exp’)
+    ]
+
+val _ = map (uncurry set_fixity)
+            [ ("+p", Infix(NONASSOC, 461)),
+              ("-p", Infix(NONASSOC, 461)),
+              ("*p", Infix(NONASSOC, 470)),
+              ("*c", Infix(NONASSOC, 470)),
+              ("**p",Infix(NONASSOC, 471))
+            ]
+
+Theorem normalize_preserving:
+  ∀ p.
+    evalPoly (normalize p) = evalPoly p
 Proof
-  Induct_on ‘p’
-  (* Var *)
-  >- (
-   rpt strip_tac
-   \\ fs[evalPoly_def]
-   \\ first_x_assum (qspec_then ‘s’ mp_tac)
-   \\ impl_tac
-   >- (
-    simp[vars_def])
-   \\ strip_tac
-   \\ fs[])
-  (* Const case *)
-  >- (
-   cheat)
-  (* Uop case *)
+  Induct_on ‘p’ >> gs[normalize_def, FUN_EQ_THM]
+  >> rpt strip_tac >> gs[evalPoly_def]
+  >> rename1 ‘c1 :: normalize cs’
+  >> cond_cases_tac
+  >> gs[evalPoly_def]
+  >> cond_cases_tac >> gs[evalPoly_def]
+QED
+
+Theorem cst_normalized:
+  ∀ c. normalize (cst c) = cst c
+Proof
+  rpt strip_tac >> gs[cst_def] >> cond_cases_tac >> gs[normalize_def]
+QED
+
+Theorem var_not_empty:
+  ∀ n. var n ≠ []
+Proof
+  strip_tac >> Cases_on ‘n’ >> gs[var_def]
+QED
+
+Theorem var_normalized:
+  ∀ n.
+    normalize (var n) = var n
+Proof
+  Induct_on ‘n’ >> gs[var_def, normalize_def, var_not_empty]
+QED
+
+Theorem normalize_idempotent:
+  ∀ p.
+    normalize (normalize p) = normalize p
+Proof
+  Induct_on ‘p’ >> gs[normalize_def]
+  >> rpt strip_tac >> cond_cases_tac
+  >- (cond_cases_tac >> gs[normalize_def])
+  >> gs[normalize_def]
+QED
+
+Theorem poly_add_normalized:
+  ∀ p1 p2.
+        normalize (p1 +p p2) = p1 +p p2
+Proof
+  gs[poly_add_def, normalize_idempotent]
+QED
+
+Theorem poly_mul_cst_normalized:
+  ∀ c p.
+    normalize (c *c p) = c *c p
+Proof
+  gs[poly_mul_cst_def, normalize_idempotent]
+QED
+
+Theorem poly_neg_normalized:
+  ∀ p.
+    normalize (--p p) = --p p
+Proof
+  gs[poly_neg_def, poly_mul_cst_normalized]
+QED
+
+Theorem poly_mul_normalized:
+  ∀ p1 p2.
+    normalize (p1 *p p2) = p1 *p p2
+Proof
+  Induct_on ‘p1’ >> gs[normalize_def, poly_mul_def, poly_add_normalized]
+QED
+
+Theorem poly_exp_normalized:
+  ∀ p n.
+    normalize (p **p n) = p **p n
+Proof
+  Induct_on ‘n’ >> gs[normalize_def, poly_exp_def, poly_mul_normalized]
+QED
+
+(* Relate to univariate HOL4 functions *)
+Definition polyEvalsTo_def:
+  polyEvalsTo (p:poly) x (r:real) ⇔
+    evalPoly p x = r
+End
+
+Theorem polyEvalsTo_Var:
+  ∀ x.
+    polyEvalsTo (var n) x (x pow n)
+Proof
+  Induct_on ‘n’ >> gs[polyEvalsTo_def, evalPoly_def, var_def, pow]
+QED
+
+Theorem polyEvalsTo_Const:
+  ∀ c x.
+    polyEvalsTo (cst c) x c
+Proof
+  rpt strip_tac >> gs[polyEvalsTo_def, cst_def]
+  >> cond_cases_tac >> gs[evalPoly_def]
+QED
+
+Theorem polyEvalsTo_MulCst:
+  ∀ p1 r1 c x.
+    polyEvalsTo p1 x r1 ⇒
+    polyEvalsTo (c *c p1) x (c * r1)
+Proof
+  Induct_on ‘p1’
+  >> gs[polyEvalsTo_def, evalPoly_def, poly_mul_cst_def, normalize_preserving,
+        poly_mul_cst_aux_def]
+  >> rpt strip_tac >> pop_assum kall_tac >> real_tac
+QED
+
+Theorem polyEvalsTo_Neg:
+  ∀ p1 x r1.
+    polyEvalsTo p1 x r1 ⇒
+    polyEvalsTo (--p p1) x (- r1)
+Proof
+  rpt strip_tac >> pop_assum $ mp_then Any assume_tac polyEvalsTo_MulCst
+  >> pop_assum $ qspec_then ‘-1’ assume_tac >> gs[poly_neg_def]
+  >> real_tac
+QED
+
+Theorem polyEvalsTo_Add:
+  ∀ p1 r1 p2 r2 x.
+    polyEvalsTo p1 x r1 ⇒
+    polyEvalsTo p2 x r2 ⇒
+    polyEvalsTo (p1 +p p2) x (r1 + r2)
+Proof
+  Induct_on ‘p1’ >> rpt strip_tac >> gs[polyEvalsTo_def, evalPoly_def, poly_add_def, normalize_preserving, poly_add_aux_def]
+  >> top_case_tac >> pop_assum $ rewrite_tac o single o GSYM
+  >> gs[evalPoly_def]
+  >> pop_assum $ rewrite_tac o single o GSYM
+  >> pop_assum kall_tac
+  >> real_tac
+QED
+
+Theorem polyEvalsTo_Sub:
+  ∀ p1 r1 p2 r2 x.
+    polyEvalsTo p1 x r1 ⇒
+    polyEvalsTo p2 x r2 ⇒
+    polyEvalsTo (p1 -p p2) x (r1 - r2)
+Proof
+  rpt strip_tac
+  >> pop_assum $ mp_then Any mp_tac polyEvalsTo_Neg
+  >> pop_assum $ mp_then Any mp_tac polyEvalsTo_Add
+  >> rpt strip_tac >> res_tac >> real_tac
+QED
+
+Theorem poly_add_aux_lid:
+  poly_add_aux p [] = p
+Proof
+  Induct_on ‘p’ >> gs[poly_add_aux_def]
+QED
+
+Theorem poly_add_lid:
+  p +p [] = normalize p
+Proof
+  Induct_on ‘p’ >> gs[poly_add_def, poly_add_aux_lid, normalize_def]
+QED
+
+Theorem polyEvalsTo_cons:
+  x ≠ 0 ∧
+  polyEvalsTo (c1::cs) x r ⇒
+  polyEvalsTo cs x ((r - c1) / x)
+Proof
+  gs[polyEvalsTo_def, evalPoly_def] >> rpt strip_tac
+  >> pop_assum $ gs o single o GSYM >> gs[real_div] >> real_tac
+QED
+
+Theorem polyEvalsTo_cons_zero:
+  polyEvalsTo cs x r ⇒
+  polyEvalsTo (0::cs) x (r * x)
+Proof
+  gs[polyEvalsTo_def, evalPoly_def]
+QED
+
+Theorem polyEvalsTo_Mul:
+  ∀ p1 r1 p2 r2 x.
+    polyEvalsTo p1 x r1 ⇒
+    polyEvalsTo p2 x r2 ⇒
+    polyEvalsTo (p1 *p p2) x (r1 * r2)
+Proof
+  Induct_on ‘p1’ >> rpt strip_tac
+  >- gs[polyEvalsTo_def, evalPoly_def, poly_mul_def]
+  >> ‘polyEvalsTo (h *c p2) x (h * r2)’
+     by (irule polyEvalsTo_MulCst >> gs[])
+  >> gs[poly_mul_def]
+  >> first_assum $ mp_then Any mp_tac polyEvalsTo_Add
+  >> cond_cases_tac
+  >- gs[poly_add_lid, polyEvalsTo_def, evalPoly_def, poly_mul_cst_def, normalize_preserving]
+  >> disch_then $ qspecl_then [‘0::(p1 *p p2)’] mp_tac
+  >> Cases_on ‘x = 0’
   >- (
-   rpt strip_tac
-   \\ simp[Once evalPoly_def]
-   \\ first_x_assum irule
-   \\ fs[Once vars_def])
-  (* Bop case *)
-  \\ cheat
+    gs[] >> disch_then $ qspec_then ‘0’ mp_tac
+    >> impl_tac >> gs[polyEvalsTo_def, evalPoly_def])
+  >> last_x_assum $ mp_then Any mp_tac polyEvalsTo_cons >> impl_tac >> gs[]
+  >> disch_then (fn thm => last_x_assum (fn ithm => mp_then Any mp_tac ithm thm))
+  >> disch_then (fn ithm => last_x_assum (fn thm => mp_then Any mp_tac ithm thm))
+  >> strip_tac
+  >> pop_assum $ mp_then Any assume_tac polyEvalsTo_cons_zero
+  >> disch_then drule >> strip_tac
+  >> gs[polyEvalsTo_def] >> real_tac
+QED
+
+Theorem polyEvalsTo_Exp:
+  ∀ p n r x.
+    polyEvalsTo p x r ⇒
+    polyEvalsTo (p **p n) x (r pow n)
+Proof
+  Induct_on ‘n’
+  >- gs[polyEvalsTo_def, evalPoly_def, poly_exp_def]
+  >> rpt strip_tac >> res_tac
+  >> last_x_assum $ mp_then Any mp_tac polyEvalsTo_Mul
+  >> disch_then drule >> gs[poly_exp_def, pow]
+QED
+
+Theorem deep_embedding:
+(∀ x. polyEvalsTo p x r) ⇒
+∀ x. evalPoly p x = (λ x:real. r) x
+Proof
+  rpt strip_tac >> gs[polyEvalsTo_def]
 QED
 
 val _ = export_theory();

renameScript.sml

+(**
+  renaming theory to unify naming of theorems
+**)
+
+open preamble;
+
+val _ = new_theory "rename";
+
+val _ = map save_thm [
+    ("OPTION_MAP_def", OPTION_MAP_DEF)
+  ]
+
+val _ = export_theory();