English
The spec of improveUntilAux is characterized by its matching on the two possible outcomes (error or ok).
Русский
Спецификация improveUntilAux описывается по двум исходам: ошибка и успех.
LaTeX
$$Estimator.improveUntilAux_spec (a,p,e,r) : match Estimator.improveUntilAux a p e r with | .error _ => ¬p a.get | .ok e' => p (bound a e')$$
Lean4
/-- If `Estimator.improveUntil a p e` returns `some e'`, then `bound a e'` satisfies `p`.
Otherwise, that value `a` must not satisfy `p`.
-/
theorem improveUntil_spec (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT (range (bound a : ε → α))]
(e : ε) :
match Estimator.improveUntil a p e with
| .error _ => ¬p a.get
| .ok e' => p (bound a e') :=
Estimator.improveUntilAux_spec a p e false
