Nat.find and Nat.findGreatest

Nat.find

def Nat.findX {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) : { n : ℕ // p n ∧ ∀ m < n, ¬p m }

Find the smallest n satisfying p n. Returns a subtype.

def Nat.find {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) : ℕ

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 that Nat.find hp satisfies p.
• Nat.find_min is the proof that if m < Nat.find hp then m does not satisfy p.
• Nat.find_min' is the proof that if m does satisfy p then Nat.find hp ≤ m.

theorem Nat.find_spec {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) : p (Nat.find H)

theorem Nat.find_min {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) {m : ℕ} : m < Nat.find H → ¬p m

theorem Nat.find_min' {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) {m : ℕ} (h : p m) : Nat.find H ≤ m

theorem Nat.find_eq_iff {m : ℕ} {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) : Nat.find h = m ↔ p m ∧ ∀ n < m, ¬p n

@[simp]

theorem Nat.find_lt_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : Nat.find h < n ↔ ∃ m < n, p m

@[simp]

theorem Nat.find_le_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : Nat.find h ≤ n ↔ ∃ m ≤ n, p m

@[simp]

theorem Nat.le_find_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ m < n, ¬p m

@[simp]

theorem Nat.lt_find_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : n < Nat.find h ↔ ∀ m ≤ n, ¬p m

@[simp]

theorem Nat.find_eq_zero {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) : Nat.find h = 0 ↔ p 0

theorem Nat.find_mono_of_le {p q : ℕ → Prop} [DecidablePred p] [DecidablePred q] {x : ℕ} (hx : q x) (hpq : ∀ n ≤ x, q n → p n) : Nat.find ⋯ ≤ Nat.find ⋯

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.

theorem Nat.find_mono {p q : ℕ → Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ℕ), q n → p n) {hp : ∃ (n : ℕ), p n} {hq : ∃ (n : ℕ), q n} : Nat.find hp ≤ Nat.find hq

A weak version of Nat.find_mono_of_le, requiring q implies p everywhere.

theorem Nat.find_congr {p q : ℕ → Prop} [DecidablePred p] [DecidablePred q] {x : ℕ} (hx : p x) (hpq : ∀ n ≤ x, p n ↔ q n) : Nat.find ⋯ = Nat.find ⋯

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].

theorem Nat.find_congr' {p q : ℕ → Prop} [DecidablePred p] [DecidablePred q] {hp : ∃ (n : ℕ), p n} {hq : ∃ (n : ℕ), q n} (hpq : ∀ {n : ℕ}, p n ↔ q n) : Nat.find hp = Nat.find hq

A weak version of Nat.find_congr, requiring p = q everywhere.

theorem Nat.find_le {n : ℕ} {p : ℕ → Prop} [DecidablePred p] {h : ∃ (n : ℕ), p n} (hn : p n) : Nat.find h ≤ n

theorem Nat.find_comp_succ {p : ℕ → Prop} [DecidablePred p] (h₁ : ∃ (n : ℕ), p n) (h₂ : ∃ (n : ℕ), p (n + 1)) (h0 : ¬p 0) : Nat.find h₁ = Nat.find h₂ + 1

theorem Nat.find_pos {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) : 0 < Nat.find h ↔ ¬p 0

theorem Nat.find_add {n : ℕ} {p : ℕ → Prop} [DecidablePred p] {hₘ : ∃ (m : ℕ), p (m + n)} {hₙ : ∃ (n : ℕ), p n} (hn : n ≤ Nat.find hₙ) : Nat.find hₘ + n = Nat.find hₙ

Nat.findGreatest

def Nat.findGreatest (P : ℕ → Prop) [DecidablePred P] : ℕ → ℕ

Nat.findGreatest P n is the largest i ≤ n such that P i holds, or 0 if no such i exists

@[simp]

theorem Nat.findGreatest_zero {P : ℕ → Prop} [DecidablePred P] : findGreatest P 0 = 0

theorem Nat.findGreatest_succ {P : ℕ → Prop} [DecidablePred P] (n : ℕ) : findGreatest P (n + 1) = if P (n + 1) then n + 1 else findGreatest P n

@[simp]

theorem Nat.findGreatest_eq {P : ℕ → Prop} [DecidablePred P] {n : ℕ} : P n → findGreatest P n = n

@[simp]

theorem Nat.findGreatest_of_not {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (h : ¬P (n + 1)) : findGreatest P (n + 1) = findGreatest P n

theorem Nat.findGreatest_eq_iff {m k : ℕ} {P : ℕ → Prop} [DecidablePred P] : findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n

theorem Nat.findGreatest_eq_zero_iff {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

@[simp]

theorem Nat.findGreatest_pos {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : 0 < findGreatest P k ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n

theorem Nat.findGreatest_spec {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hmb : m ≤ n) (hm : P m) : P (findGreatest P n)

theorem Nat.findGreatest_le {P : ℕ → Prop} [DecidablePred P] (n : ℕ) : findGreatest P n ≤ n

theorem Nat.le_findGreatest {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hmb : m ≤ n) (hm : P m) : m ≤ findGreatest P n

theorem Nat.findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] {m n : ℕ} (hmn : m ≤ n) : findGreatest P m ≤ findGreatest P n

theorem Nat.findGreatest_mono_left {P Q : ℕ → Prop} [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (n : ℕ), P n → Q n) (n : ℕ) : findGreatest P n ≤ findGreatest Q n

theorem Nat.findGreatest_mono {m : ℕ} {P Q : ℕ → Prop} [DecidablePred P] {n : ℕ} [DecidablePred Q] (hPQ : ∀ (n : ℕ), P n → Q n) (hmn : m ≤ n) : findGreatest P m ≤ findGreatest Q n

theorem Nat.findGreatest_is_greatest {k : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (hk : findGreatest P n < k) (hkb : k ≤ n) : ¬P k

theorem Nat.findGreatest_of_ne_zero {m : ℕ} {P : ℕ → Prop} [DecidablePred P] {n : ℕ} (h : findGreatest P n = m) (h0 : m ≠ 0) : P m