English
If Estimator.improveUntilAux returns an error, then a.get does not satisfy p; if it returns Ok e', then p(bound a e').
Русский
Если функция возвращает ошибку, то a.get не удовлетворяет p; если возвращает Ok e', то p(bound(a,e')).
LaTeX
$$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 improveUntilAux_spec (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT (range (bound a : ε → α))]
(e : ε) (r : Bool) :
match Estimator.improveUntilAux a p e r with
| .error _ => ¬p a.get
| .ok e' => p (bound a e') :=
by
rw [Estimator.improveUntilAux]
by_cases h : p (bound a e)
· simp only [h]; exact h
· simp only [h]
match improve a e, improve_spec e with
| none, eq =>
simp only [Bool.not_eq_true]
rw [eq] at h
exact Bool.bool_eq_false h
| some e', _ => exact Estimator.improveUntilAux_spec a p e' true
termination_by (⟨_, mem_range_self e⟩ : range (bound a))
