Made some progress on the checker soundness lemma

checkerScript.sml

@@ -67,7 +67,7 @@ Definition validateZeroesLeqErr_def:
   ∧
   validateZeroesLeqErr diffPoly iv ((z1,z2)::zeroes) eps =
   ( if ((FST iv) < z1 ∧ z2 < (SND iv) ∧ z1 ≤ z2 ∧
-        ((poly diffPoly z1) * (poly diffPoly z2) < &0) ∧
+        ((poly (diff diffPoly) z1) * (poly (diff diffPoly) z2) < &0) ∧
         abs(poly diffPoly z1) ≤ eps ∧ abs(poly diffPoly z2) ≤ eps)
         then validateZeroesLeqErr diffPoly iv zeroes eps
      else Invalid "Zero of derivativ not an extremal point or extrema too big")
@@ -126,25 +126,146 @@ Proof
 QED
 
 Theorem validateZeroesLeqErr_EVERY:
-  validateZeroesLeqErr deriv iv zeroes err = Valid ⇒
-  EVERY (λ (u,v). FST iv ≤ u ∧ v ≤ SND iv ∧ abs (poly errorp u) ≤ ub) l
+  ∀err. validateZeroesLeqErr errorp iv zeroes err = Valid ⇒
+        EVERY (λ (u,v). FST iv ≤ u ∧ v ≤ SND iv ∧ abs (u − v) ≤ e ∧
+                        abs (poly errorp u) ≤ ub) l
 Proof
   cheat
 QED
 
+
+Theorem bound_for_deriv:
+  validateZeroesLeqErr errorp iv zeroes err = Valid ⇒
+  ∀x'. FST iv ≤ x' ∧ x' ≤ SND iv ⇒ abs (poly (diff errorp) x') ≤ B
+Proof
+  cheat
+QED
+
+Theorem validateZeroesLeqErr_zeroes_true:
+  zeroes ≠ [] ⇒
+  validateZeroesLeqErr errorp iv zeroes err = Valid ⇒
+  (∀x'. FST iv ≤ x' ∧ x' ≤ SND iv ∧ poly (diff errorp) x' = 0 ⇒
+        EXISTS (λ(u,v). (u ≤ x' ∧ x' ≤ v)) zeroes)
+Proof
+  Induct_on ‘zeroes’
+  >- gs[]
+  >> rpt strip_tac
+  >> gs[]
+  >> Cases_on ‘zeroes = []’
+  >- ( gs[]
+       >> ‘h = (FST h, SND h)’ by gs[]
+       >> ‘validateZeroesLeqErr errorp iv [h] err =
+           validateZeroesLeqErr errorp iv [(FST h, SND h)] err’ by gs[]
+       >> last_x_assum mp_tac
+       >> rw[validateZeroesLeqErr_def]
+       >> ‘(λ(u,v). u ≤ x' ∧ x' ≤ v) h =
+           (λ(u,v). u ≤ x' ∧ x' ≤ v) (FST h, SND h)’ by cheat
+       >> gs[]
+       >> cheat
+     )
+  >> gs[]
+  >> ‘(h::zeroes) = ((FST h, SND h) :: zeroes)’ by gs[]
+  >> ‘validateZeroesLeqErr errorp iv (h::zeroes) err =
+      validateZeroesLeqErr errorp iv ((FST h,SND h)::zeroes) err’ by gs[]
+  >> qpat_x_assum ‘validateZeroesLeqErr errorp iv (h::zeroes) err = Valid’ mp_tac
+  >> rw[validateZeroesLeqErr_def]
+QED
+
+(** Distribute the err into ub, B, e **)
+Theorem error_distr:
+  ∀ err:real. ∃ ub B e. err = ub + B * e
+Proof
+  cheat
+QED
+
+(** Bounds at the end points **)
+Theorem bound_holds_left_end:
+  ∀ err.
+    validateZeroesLeqErr errorp iv zeroes err = Valid ⇒
+    abs (poly errorp (FST iv)) ≤ err
+Proof
+  gen_tac
+  >> Induct_on ‘zeroes’
+  >- ( gs[validateZeroesLeqErr_def]
+       >> cond_cases_tac >> gs[]
+     )
+  >> rpt strip_tac
+  >> ‘h = (FST h, SND h)’ by gs[]
+  >> ‘validateZeroesLeqErr errorp iv (h::zeroes) err =
+      validateZeroesLeqErr errorp iv ((FST h,SND h)::zeroes) err’ by gs[]
+  >> qpat_x_assum ‘validateZeroesLeqErr errorp iv (h::zeroes) err = Valid’ mp_tac
+  >> rw[validateZeroesLeqErr_def]
+QED
+
+Theorem bound_holds_right_end:
+  ∀ err.
+    validateZeroesLeqErr errorp iv zeroes err = Valid ⇒
+    abs (poly errorp (SND iv)) ≤ err
+Proof
+  gen_tac
+  >> Induct_on ‘zeroes’
+  >- ( gs[validateZeroesLeqErr_def]
+       >> cond_cases_tac >> gs[]
+     )
+  >> rpt strip_tac
+  >> ‘h = (FST h, SND h)’ by gs[]
+  >> ‘validateZeroesLeqErr errorp iv (h::zeroes) err =
+      validateZeroesLeqErr errorp iv ((FST h,SND h)::zeroes) err’ by gs[]
+  >> qpat_x_assum ‘validateZeroesLeqErr errorp iv (h::zeroes) err = Valid’ mp_tac
+  >> rw[validateZeroesLeqErr_def]
+QED
+
+
+
 Theorem validateZeroesLeqErr_sound:
   ∀ deriv errorp iv zeroes err.
     deriv = diff errorp ∧
     {x | FST iv ≤ x ∧ x ≤ SND iv ∧ (poly deriv x = &0)} HAS_SIZE LENGTH zeroes ∧
-    validateZeroesLeqErr deriv iv zeroes err = Valid ⇒
-    ∀ x. FST iv ≤ x ∧ x ≤ SND iv ⇒ poly errorp x ≤ err
+    validateZeroesLeqErr errorp iv zeroes err = Valid ⇒
+    ∀ x. FST iv ≤ x ∧ x ≤ SND iv ⇒ abs(poly errorp x) ≤ err
 Proof
   rpt strip_tac
   >> ‘∀ x. FST iv ≤ x ∧ x ≤ SND iv ⇒ ((λ x. poly errorp x) diffl poly deriv x) x’
      by (rpt strip_tac >> gs[polyTheory.POLY_DIFF])
   >> drule (GEN_ALL BOUND_THEOREM_INEXACT |> SPEC_ALL |> GEN “e:real”)
   >> gs[validateZeroesLeqErr_def]
-  >> cheat
+  >> rpt strip_tac
+  >> assume_tac error_distr
+  >> pop_assum $ qspec_then ‘err’ strip_assume_tac
+  >> qpat_x_assum ‘∀ ub l B' e x'. _’ $ qspecl_then
+                  [‘ub’, ‘zeroes’, ‘B’, ‘e’,‘x’] assume_tac
+  >> VAR_EQ_TAC
+  >> first_assum irule
+  >> rpt conj_tac
+  >- ( Cases_on ‘zeroes = []’
+       >- ( gs[validateZeroesLeqErr_def]
+            >> gs[HAS_SIZE]
+            >> cheat (** Should be true by definition of empty set **)
+          )
+       >> rpt strip_tac >> irule validateZeroesLeqErr_zeroes_true
+       >> rpt conj_tac
+       >- gs[]
+       >> qexists_tac ‘ub + B * e’ >> qexists_tac ‘errorp’ >> qexists_tac ‘iv’
+       >> gs[]
+     )
+  >- ( rpt strip_tac >> irule bound_for_deriv
+       >> qexists_tac ‘ub + B * e’ >> qexists_tac ‘iv’ >> qexists_tac ‘zeroes’
+       >> gs[]
+     ) (** Prove a bound for the derivative: perhaps the Taylor approx **)
+  >- ( irule validateZeroesLeqErr_EVERY
+       >> qexists_tac ‘ub + B * e’ >> qexists_tac ‘zeroes’
+       >> gs[]
+     ) (** This is perhaps the bound given by the error after subtracting
+                 Taylor approx **)
+  >- gs[]
+  >- gs[]
+  (** Boundedness at the end point **)
+  >- ( irule bound_holds_left_end
+       >> qexists_tac ‘zeroes’ >> gs[]
+     )
+  (** Boundedness at the end point **)
+  >> irule bound_holds_right_end
+  >> qexists_tac ‘zeroes’ >> gs[]
 QED
 
 Theorem checker_soundness: