Nat.find and Nat.findGreatest

Nat.find

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Nat.find H = (Nat.findX H).val

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 : ℕ), n < m → ¬p n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.lt_find_iff {p : ℕ → Prop} [DecidablePred p] (h : ∃ (n : ℕ), p n) (n : ℕ) : n < Nat.find h ↔ ∀ (m : ℕ), 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 {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

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 ≤ 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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem Nat.findGreatest_eq_iff {m k : ℕ} {P : ℕ → Prop} [DecidablePred P] : Nat.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] : Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

@[simp]

theorem Nat.findGreatest_pos {k : ℕ} {P : ℕ → Prop} [DecidablePred P] : 0 < Nat.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 (Nat.findGreatest P n)

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

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

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

theorem Nat.findGreatest_mono_left {P Q : ℕ → Prop} [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (n : ℕ), P n → Q n) (n : ℕ) : Nat.findGreatest P n ≤ Nat.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) : Nat.findGreatest P m ≤ Nat.findGreatest Q n

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

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