Polynomial-time bounded search

Nat.findGreatest searches the inclusive interval from zero to a computed unary bound. It returns the greatest matching index, or zero when no index matches. The predicate may capture the original input; its certificate is joint in that input and the candidate unary index.

The implementation enumerates the interval, reverses it, and searches the resulting list. Its certificate charges the full candidate list, reversal, copying, every predicate call, and output. The ordinary Mathlib specification of Nat.findGreatest remains available to clients.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.findGreatest: exact total bounded search with uniform polynomial time in the caller's input encoding.

References

Adapted from Cslib/Computability/Probabilistic/Search.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the plain deterministic calculus.

theorem Turing.MultiTapeTM.ComputableInPolyTime.findGreatest {α : Type} {input : α ↪ List Bool} {bound : α → ℕ} {predicate : α → ℕ → Prop} [(a : α) → DecidablePred (predicate a)] (hbound : ComputableInPolyTime bound input encUnary) (hpredicate : ComputableInPolyTime (fun (p : α × ℕ) => decide (predicate p.1 p.2)) (encPair input encUnary) encBool) : ComputableInPolyTime (fun (a : α) => Nat.findGreatest (predicate a) (bound a)) input encUnary

Search every index up to the supplied unary bound, returning the greatest match or zero. Both the bound and the predicate are certified uniformly in the original input.