If p
is a (decidable) predicate on ℕ
and hp : ∃ (n : ℕ), p n
is a proof that
there exists some natural number satisfying p
, then Nat.find hp
is the
smallest natural number satisfying p
. Note that Nat.find
is protected,
meaning that you can't just write find
, even if the Nat
namespace is open.
The API for Nat.find
is:
Nat.find_spec
is the proof thatNat.find hp
satisfiesp
.Nat.find_min
is the proof that ifm < Nat.find hp
thenm
does not satisfyp
.Nat.find_min'
is the proof that ifm
does satisfyp
thenNat.find hp ≤ m
.
Instances For
If a predicate q
holds at some x
and implies p
up to that x
, then
the earliest xq
such that q xq
is at least the smallest xp
where p xp
.
The stronger version of Nat.find_mono
, since this one needs
implication only up to Nat.find _
while the other requires q
implying p
everywhere.
If a predicate p
holds at some x
and agrees with q
up to that x
, then
their Nat.find
agree. The stronger version of Nat.find_congr'
, since this one needs
agreement only up to Nat.find _
while the other requires p = q
.
Usage of this lemma will likely be via obtain ⟨x, hx⟩ := hp; apply Nat.find_congr hx
to unify q
,
or provide it explicitly with rw [Nat.find_congr (q := q) hx]
.
Nat.findGreatest P n
is the largest i ≤ bound
such that P i
holds, or 0
if no such i
exists
Equations
- Nat.findGreatest P 0 = 0
- Nat.findGreatest P n.succ = if P (n + 1) then n + 1 else Nat.findGreatest P n