English
If Estimator.improveUntil a p e returns some e', then bound a e' satisfies p; otherwise, the input value a does not satisfy p.
Русский
Если улучшенная оценка возвращает некоторое e', то bound a e' удовлетворяет p; иначе исходное значение a не удовлетворяет p.
LaTeX
$$Estimator.improveUntil_spec (a) (p) [Estimator a ε] [WellFoundedGT range (bound a : ε → α)] (e) : match Estimator.improveUntil a p e with | .error _ => ¬p a.get | .ok e' => p (bound a e')$$
Lean4
/-- By improving priority estimates as needed, and permuting elements,
ensure that the first element of the queue has the greatest priority.
-/
partial def ensureFirstIsBest (q : BestFirstQueue prio ε m β maxSize) : m (BestFirstQueue prio ε m β maxSize) := do
match q.entryAtIdx? 0 with
| none =>
-- The queue is empty, nothing to do.
return q
| some (n, l) =>
match q.entryAtIdx? 1 with
| none =>
do
-- There's only one element in the queue, no reordering necessary.
return q
| some (m, _) =>
-- `n` is the first index, `m` is the second index.
-- We need to improve our estimate of the priority for `n` to make sure
-- it really should come before `m`.
match improveUntil (prio n.key) (m.estimate < ·) n.estimator with
| .error none =>
-- If we couldn't improve the estimate at all, it is exact, and hence the best element.
return q
| .error (some e') =>
-- If we improve the estimate, but it is still at most the estimate for `m`,
-- this is the best element, so all we need to do is store the updated estimate.
return q.erase n |>.insert ⟨n.key, e'⟩ l
| .ok e' =>
-- If we improved the estimate and it becomes greater than the estimate for `m`,
-- we re-insert `n` with its new estimate, and then try again.
ensureFirstIsBest (q.erase n |>.insert ⟨n.key, e'⟩ l)
