Mathlib.Data.Nat.Find

Nat.findX definition

: { n // p n ∧ ∀ m < n, ¬p m }

Full source

/-- Find the smallest `n` satisfying `p n`. Returns a subtype. -/
protected def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
  @WellFounded.fix _ (fun k => (∀ n < k, ¬p n) → { n // p n ∧ ∀ m < n, ¬p m }) lbp (wf_lbp H)
    (fun m IH al =>
      if pm : p m then ⟨m, pm, al⟩
      else
        have : ∀ n ≤ m, ¬p n := fun n h =>
          Or.elim (Nat.lt_or_eq_of_le h) (al n) fun e => by rw [e]; exact pm
        IH _ ⟨rfl, this⟩ fun n h => this n <| Nat.le_of_succ_le_succ h)
    0 fun _ h => absurd h (Nat.not_lt_zero _)

Minimal natural number satisfying a predicate (with proof)

Informal description

Given a decidable predicate $ p $ on natural numbers, `Nat.findX` returns the smallest natural number $ n $ such that $ p(n) $ holds, along with a proof that $ p(n) $ is true and that for all $ m < n $, $ p(m) $ does not hold. More formally, `Nat.findX` produces a pair $(n, \text{proof})$ where: - $ n $ is the minimal natural number satisfying $ p(n) $, - $\text{proof}$ consists of: - a proof that $ p(n) $ holds, and - a proof that for all $ m < n $, $ p(m) $ does not hold. This is constructed using well-founded recursion on the natural numbers with the lexicographic order based on the predicate $ p $.

Nat.find definition

: ℕ

Full source

/-- 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`.
-/
protected def find : ℕ :=
  (Nat.findX H).1

Minimal natural number satisfying a predicate

Informal description

Given a decidable predicate $ p $ on natural numbers and a proof $ H $ that there exists some natural number satisfying $ p $, `Nat.find H` is the smallest natural number $ n $ such that $ p(n) $ holds.

Nat.find_spec theorem

: p (Nat.find H)

Full source

protected theorem find_spec : p (Nat.find H) :=
  (Nat.findX H).2.left

Minimal Satisfying Number Satisfies Predicate

Informal description

For any decidable predicate $p$ on natural numbers and any proof $H$ that there exists a natural number satisfying $p$, the minimal natural number $\text{Nat.find}\, H$ satisfies $p(\text{Nat.find}\, H)$.

Nat.find_min theorem

: ∀ {m : ℕ}, m < Nat.find H → ¬p m

Full source

protected theorem find_min : ∀ {m : ℕ}, m < Nat.find H → ¬p m :=
  @(Nat.findX H).2.right

Minimality Property of `Nat.find`: No Smaller Number Satisfies the Predicate

Informal description

For any natural number $m$ such that $m$ is less than the minimal natural number satisfying the predicate $p$ (i.e., $m < \text{Nat.find}\, H$), the predicate $p$ does not hold at $m$ (i.e., $\neg p(m)$).

Nat.find_min' theorem

{m : ℕ} (h : p m) : Nat.find H ≤ m

Full source

protected theorem find_min' {m : ℕ} (h : p m) : Nat.find H ≤ m :=
  Nat.le_of_not_lt fun l => Nat.find_min H l h

Minimal Satisfying Number is the Least Upper Bound

Informal description

For any natural number $m$ satisfying the predicate $p$, the minimal natural number satisfying $p$ (denoted by $\text{Nat.find}\, H$) is less than or equal to $m$.

Nat.find_eq_iff theorem

(h : ∃ n : ℕ, p n) : Nat.find h = m ↔ p m ∧ ∀ n < m, ¬p n

Full source

lemma find_eq_iff (h : ∃ n : ℕ, p n) : Nat.findNat.find h = m ↔ p m ∧ ∀ n < m, ¬ p n := by
  constructor
  · rintro rfl
    exact ⟨Nat.find_spec h, fun _ ↦ Nat.find_min h⟩
  · rintro ⟨hm, hlt⟩
    exact le_antisymm (Nat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| Nat.find_spec h)

Characterization of Minimal Satisfier: $\text{Nat.find}\,h = m \leftrightarrow (p(m) \land \forall n < m, \neg p(n))$

Informal description

For a decidable predicate $p$ on natural numbers and a proof $h$ that there exists some natural number satisfying $p$, the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ is equal to $m$ if and only if $p(m)$ holds and for all natural numbers $n < m$, $p(n)$ does not hold.

Nat.find_lt_iff theorem

(h : ∃ n : ℕ, p n) (n : ℕ) : Nat.find h < n ↔ ∃ m < n, p m

Full source

@[simp] lemma find_lt_iff (h : ∃ n : ℕ, p n) (n : ℕ) : Nat.findNat.find h < n ↔ ∃ m < n, p m :=
  ⟨fun h2 ↦ ⟨Nat.find h, h2, Nat.find_spec h⟩,
    fun ⟨_, hmn, hm⟩ ↦ Nat.lt_of_le_of_lt (Nat.find_min' h hm) hmn⟩

Minimal Satisfier is Below $n$ if and only if a Satisfier Exists Below $n$

Informal description

For a decidable predicate $p$ on natural numbers and a proof $h$ that there exists some natural number satisfying $p$, the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ is less than $n$ if and only if there exists a natural number $m < n$ such that $p(m)$ holds.

Nat.find_le_iff theorem

(h : ∃ n : ℕ, p n) (n : ℕ) : Nat.find h ≤ n ↔ ∃ m ≤ n, p m

Full source

@[simp] lemma find_le_iff (h : ∃ n : ℕ, p n) (n : ℕ) : Nat.findNat.find h ≤ n ↔ ∃ m ≤ n, p m := by
  simp only [exists_prop, ← Nat.lt_succ_iff, find_lt_iff]

Minimal Satisfier is Less Than or Equal to $n$ if and only if There Exists a Satisfier $\leq n$

Informal description

For a decidable predicate $p$ on natural numbers with a proof $h$ that there exists some $n$ satisfying $p$, the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ is less than or equal to $n$ if and only if there exists some $m \leq n$ such that $p(m)$ holds.

Nat.le_find_iff theorem

(h : ∃ n : ℕ, p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ m < n, ¬p m

Full source

@[simp] lemma le_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n ≤ Nat.find h ↔ ∀ m < n, ¬ p m := by
  simp only [← not_lt, find_lt_iff, not_exists, not_and]

Characterization of Numbers Below Minimal Satisfier: $n \leq \text{find}\,h \leftrightarrow \forall m < n, \neg p(m)$

Informal description

For a decidable predicate $p$ on natural numbers with a proof $h$ that there exists some natural number satisfying $p$, a natural number $n$ is less than or equal to the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ if and only if for all $m < n$, the predicate $p(m)$ does not hold.

Nat.lt_find_iff theorem

(h : ∃ n : ℕ, p n) (n : ℕ) : n < Nat.find h ↔ ∀ m ≤ n, ¬p m

Full source

@[simp] lemma lt_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n < Nat.find h ↔ ∀ m ≤ n, ¬ p m := by
  simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]

Characterization of Numbers Below Minimal Satisfier: $n < \text{find}\,h \leftrightarrow \forall m \leq n, \neg p(m)$

Informal description

For a decidable predicate $p$ on natural numbers with a proof $h$ that there exists some natural number satisfying $p$, a natural number $n$ is strictly less than the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ if and only if for all $m \leq n$, the predicate $p(m)$ does not hold.

Nat.find_eq_zero theorem

(h : ∃ n : ℕ, p n) : Nat.find h = 0 ↔ p 0

Full source

@[simp] lemma find_eq_zero (h : ∃ n : ℕ, p n) : Nat.findNat.find h = 0 ↔ p 0 := by simp [find_eq_iff]

Minimal Satisfier is Zero if and only if Predicate Holds at Zero

Informal description

For a decidable predicate $p$ on natural numbers with a proof $h$ that there exists some natural number satisfying $p$, the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ is equal to $0$ if and only if $p(0)$ holds.

Nat.find_mono_of_le theorem

 [DecidablePred q] {x : ℕ} (hx : q x) (hpq : ∀ n ≤ x, q n → p n) :
  Nat.find ⟨x, show p x from hpq _ le_rfl hx⟩ ≤ Nat.find ⟨x, hx⟩

Full source

/-- 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. -/
lemma find_mono_of_le [DecidablePred q] {x : ℕ} (hx : q x) (hpq : ∀ n ≤ x, q n → p n) :
    Nat.find ⟨x, show p x from hpq _ le_rfl hx⟩ ≤ Nat.find ⟨x, hx⟩ :=
  Nat.find_min' _ (hpq _ (Nat.find_min' _ hx) (Nat.find_spec ⟨x, hx⟩))

Minimal Satisfier Comparison under Local Implication

Informal description

Let $p$ and $q$ be decidable predicates on natural numbers. Suppose there exists a natural number $x$ such that $q(x)$ holds, and for all $n \leq x$, $q(n)$ implies $p(n)$. Then the minimal natural number satisfying $p$ (with existence witness constructed from $x$) is less than or equal to the minimal natural number satisfying $q$ (with existence witness $x$).

Nat.find_mono theorem

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

Full source

/-- A weak version of `Nat.find_mono_of_le`, requiring `q` implies `p` everywhere.
-/
lemma find_mono [DecidablePred q] (h : ∀ n, q n → p n) {hp : ∃ n, p n} {hq : ∃ n, q n} :
    Nat.find hp ≤ Nat.find hq :=
  let ⟨_, hq⟩ := hq; find_mono_of_le hq fun _ _ ↦ h _

Monotonicity of Minimal Satisfier under Global Implication

Informal description

Let $p$ and $q$ be decidable predicates on natural numbers such that for all $n$, $q(n)$ implies $p(n)$. If there exist natural numbers satisfying $p$ and $q$, then the minimal natural number satisfying $p$ is less than or equal to the minimal natural number satisfying $q$.

Nat.find_congr theorem

 [DecidablePred q] {x : ℕ} (hx : p x) (hpq : ∀ n ≤ x, p n ↔ q n) :
  Nat.find ⟨x, hx⟩ = Nat.find ⟨x, show q x from hpq _ le_rfl |>.1 hx⟩

Full source

/-- 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]`.
-/
lemma find_congr [DecidablePred q] {x : ℕ} (hx : p x) (hpq : ∀ n ≤ x, p n ↔ q n) :
    Nat.find ⟨x, hx⟩ = Nat.find ⟨x, show q x from hpq _ le_rfl |>.1 hx⟩ :=
  le_antisymm (find_mono_of_le (hpq _ le_rfl |>.1 hx) fun _ h ↦ (hpq _ h).mpr)
    (find_mono_of_le hx fun _ h ↦ (hpq _ h).mp)

Equality of Minimal Satisfiers under Local Equivalence

Informal description

Let $p$ and $q$ be decidable predicates on natural numbers. Suppose there exists a natural number $x$ such that $p(x)$ holds, and for all $n \leq x$, $p(n)$ holds if and only if $q(n)$ holds. Then the minimal natural number satisfying $p$ (with existence witness $x$) is equal to the minimal natural number satisfying $q$ (with existence witness constructed from $x$ via the equivalence).

Nat.find_congr' theorem

[DecidablePred q] {hp : ∃ n, p n} {hq : ∃ n, q n} (hpq : ∀ {n}, p n ↔ q n) : Nat.find hp = Nat.find hq

Full source

/-- A weak version of `Nat.find_congr`, requiring `p = q` everywhere. -/
lemma find_congr' [DecidablePred q] {hp : ∃ n, p n} {hq : ∃ n, q n} (hpq : ∀ {n}, p n ↔ q n) :
    Nat.find hp = Nat.find hq :=
  let ⟨_, hp⟩ := hp; find_congr hp fun _ _ ↦ hpq

Equality of Minimal Satisfiers under Global Equivalence

Informal description

Let $p$ and $q$ be decidable predicates on natural numbers such that for all $n$, $p(n)$ holds if and only if $q(n)$ holds. If there exist natural numbers satisfying $p$ and $q$, then the minimal natural number satisfying $p$ is equal to the minimal natural number satisfying $q$.

Nat.find_le theorem

{h : ∃ n, p n} (hn : p n) : Nat.find h ≤ n

Full source

lemma find_le {h : ∃ n, p n} (hn : p n) : Nat.find h ≤ n :=
  (Nat.find_le_iff _ _).2 ⟨n, le_refl _, hn⟩

Minimal Satisfier is Less Than or Equal to Any Satisfier

Informal description

For any decidable predicate $p$ on natural numbers with a proof $h$ that there exists some $n$ satisfying $p$, if $p(n)$ holds for a particular natural number $n$, then the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ is less than or equal to $n$.

Nat.find_comp_succ theorem

(h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h0 : ¬p 0) : Nat.find h₁ = Nat.find h₂ + 1

Full source

lemma find_comp_succ (h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h0 : ¬ p 0) :
    Nat.find h₁ = Nat.find h₂ + 1 := by
  refine (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn ↦ ?_⟩
  cases n
  exacts [h0, @Nat.find_min (fun n ↦ p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]

Minimal Satisfier Shift: $\text{Nat.find}\,h_1 = \text{Nat.find}\,h_2 + 1$ when $p(0)$ fails

Informal description

For a decidable predicate $p$ on natural numbers, suppose there exist proofs $h_1$ that some $n$ satisfies $p(n)$ and $h_2$ that some $n$ satisfies $p(n+1)$, and that $p(0)$ does not hold. Then the minimal natural number satisfying $p$ is equal to one plus the minimal natural number satisfying $p(n+1)$, i.e., $\text{Nat.find}\,h_1 = \text{Nat.find}\,h_2 + 1$.

Nat.find_pos theorem

(h : ∃ n : ℕ, p n) : 0 < Nat.find h ↔ ¬p 0

Full source

lemma find_pos (h : ∃ n : ℕ, p n) : 0 < Nat.find h ↔ ¬p 0 :=
  Nat.pos_iff_ne_zero.trans (Nat.find_eq_zero _).not

Positivity of Minimal Satisfier Equivalent to Predicate Failing at Zero

Informal description

For a decidable predicate $p$ on natural numbers with a proof $h$ that there exists some natural number satisfying $p$, the minimal natural number $\text{Nat.find}\,h$ satisfying $p$ is positive if and only if $p(0)$ does not hold. In other words, $0 < \text{Nat.find}\,h \leftrightarrow \neg p(0)$.

Nat.find_add theorem

{hₘ : ∃ m, p (m + n)} {hₙ : ∃ n, p n} (hn : n ≤ Nat.find hₙ) : Nat.find hₘ + n = Nat.find hₙ

Full source

lemma find_add {hₘ : ∃ m, p (m + n)} {hₙ : ∃ n, p n} (hn : n ≤ Nat.find hₙ) :
    Nat.find hₘ + n = Nat.find hₙ := by
  refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_
  · have hnm : n ≤ m := le_trans hn (find_le hpm)
    refine Nat.add_le_of_le_sub hnm (find_le ?_)
    rwa [Nat.sub_add_cancel hnm]
  · rw [← Nat.sub_le_iff_le_add]
    refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_
    rw [Nat.sub_le_iff_le_add]
    exact find_le hpm

Additive Property of Minimal Satisfiers for Shifted Predicates

Informal description

For any decidable predicate $p$ on natural numbers, suppose there exist proofs $h_m$ and $h_n$ that there exist natural numbers satisfying $p(m + n)$ and $p(n)$ respectively. If $n$ is less than or equal to the minimal natural number $\text{Nat.find}\,h_n$ satisfying $p$, then the sum of the minimal natural number $\text{Nat.find}\,h_m$ satisfying $p(m + n)$ and $n$ equals $\text{Nat.find}\,h_n$. That is, $\text{Nat.find}\,h_m + n = \text{Nat.find}\,h_n$.

Nat.findGreatest definition

(P : ℕ → Prop) [DecidablePred P] : ℕ → ℕ

Full source

/-- `Nat.findGreatest P n` is the largest `i ≤ bound` such that `P i` holds, or `0` if no such `i`
exists -/
def findGreatest (P : ℕ → Prop) [DecidablePred P] : ℕ → ℕ
  | 0 => 0
  | n + 1 => if P (n + 1) then n + 1 else Nat.findGreatest P n

Greatest natural number satisfying a predicate up to a bound

Informal description

Given a decidable predicate $ P $ on natural numbers and a natural number $ n $, the function $ \text{Nat.findGreatest} $ returns the largest natural number $ i \leq n $ such that $ P(i) $ holds. If no such $ i $ exists, it returns $ 0 $. More precisely: - $ \text{Nat.findGreatest} \, P \, 0 = 0 $ - For $ n \geq 0 $, $ \text{Nat.findGreatest} \, P \, (n + 1) $ equals $ n + 1 $ if $ P(n + 1) $ holds, otherwise it equals $ \text{Nat.findGreatest} \, P \, n $.

Nat.findGreatest_zero theorem

: Nat.findGreatest P 0 = 0

Full source

@[simp] lemma findGreatest_zero : Nat.findGreatest P 0 = 0 := rfl

Greatest Satisfying Number at Zero is Zero

Informal description

For any decidable predicate $P$ on natural numbers, the greatest natural number less than or equal to 0 satisfying $P$ is 0, i.e., $\text{Nat.findGreatest}\, P\, 0 = 0$.

Nat.findGreatest_succ theorem

(n : ℕ) : Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n

Full source

lemma findGreatest_succ (n : ℕ) :
    Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n := rfl

Recursive Characterization of `Nat.findGreatest` at Successor

Informal description

For any natural number $n$ and decidable predicate $P$, the greatest natural number $i \leq n+1$ satisfying $P(i)$ is equal to $n+1$ if $P(n+1)$ holds, and otherwise equals the greatest natural number $i \leq n$ satisfying $P(i)$. In other words: \[ \text{Nat.findGreatest}\, P\, (n + 1) = \begin{cases} n + 1 & \text{if } P(n + 1), \\ \text{Nat.findGreatest}\, P\, n & \text{otherwise.} \end{cases} \]

Nat.findGreatest_eq theorem

: ∀ {n}, P n → Nat.findGreatest P n = n

Full source

@[simp] lemma findGreatest_eq : ∀ {n}, P n → Nat.findGreatest P n = n
  | 0, _ => rfl
  | n + 1, h => by simp [Nat.findGreatest, h]

Greatest Satisfying Number Equals Input When Predicate Holds

Informal description

For any natural number $n$ satisfying a decidable predicate $P$, the greatest natural number less than or equal to $n$ that satisfies $P$ is equal to $n$ itself, i.e., $\text{Nat.findGreatest}\, P\, n = n$.

Nat.findGreatest_of_not theorem

(h : ¬P (n + 1)) : findGreatest P (n + 1) = findGreatest P n

Full source

@[simp]
lemma findGreatest_of_not (h : ¬ P (n + 1)) : findGreatest P (n + 1) = findGreatest P n := by
  simp [Nat.findGreatest, h]

Preservation of Greatest Satisfier When Predicate Fails at Successor

Informal description

For any decidable predicate $P$ on natural numbers and any natural number $n$, if $P(n+1)$ does not hold, then the greatest natural number $\leq n+1$ satisfying $P$ is equal to the greatest natural number $\leq n$ satisfying $P$. That is, $\text{findGreatest}\,P\,(n+1) = \text{findGreatest}\,P\,n$ when $\neg P(n+1)$.

Nat.findGreatest_eq_iff theorem

: Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n⦄, m < n → n ≤ k → ¬P n

Full source

lemma findGreatest_eq_iff :
    Nat.findGreatestNat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n⦄, m < n → n ≤ k → ¬P n := by
  induction k generalizing m with
  | zero =>
    rw [eq_comm, Iff.comm]
    simp only [zero_eq, Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
    rintro rfl
    exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by omega⟩
  | succ k ihk =>
    by_cases hk : P (k + 1)
    · rw [findGreatest_eq hk]
      constructor
      · rintro rfl
        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by omega⟩
      · rintro ⟨hle, h0, hm⟩
        rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt)
        exacts [rfl, (hm hlt (le_refl _) hk).elim]
    · rw [findGreatest_of_not hk, ihk]
      constructor
      · rintro ⟨hle, hP, hm⟩
        refine ⟨le_trans hle k.le_succ, hP, fun n hlt hle ↦ ?_⟩
        rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt')
        exacts [hk, hm hlt <| Nat.lt_succ_iff.1 hlt']
      · rintro ⟨hle, hP, hm⟩
        refine ⟨Nat.lt_succ_iff.1 (lt_of_le_of_ne hle ?_), hP,
          fun n hlt hle ↦ hm hlt (le_trans hle k.le_succ)⟩
        rintro rfl
        exact hk (hP k.succ_ne_zero)

Characterization of Greatest Satisfying Natural Number up to a Bound

Informal description

For a decidable predicate $P$ on natural numbers and natural numbers $k$ and $m$, the greatest natural number $\leq k$ satisfying $P$ equals $m$ if and only if: 1. $m \leq k$, 2. If $m \neq 0$, then $P(m)$ holds, and 3. For all $n$ such that $m < n \leq k$, $P(n)$ does not hold. In other words: $\text{Nat.findGreatest}\, P\, k = m \leftrightarrow m \leq k \land (m \neq 0 \to P(m)) \land \forall n (m < n \leq k \to \neg P(n))$.

Nat.findGreatest_eq_zero_iff theorem

: Nat.findGreatest P k = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ k → ¬P n

Full source

lemma findGreatest_eq_zero_iff : Nat.findGreatestNat.findGreatest P k = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ k → ¬P n := by
  simp [findGreatest_eq_iff]

Characterization of Zero as Greatest Satisfying Number: $\text{findGreatest}\, P\, k = 0 \leftrightarrow \forall n (0 < n \leq k \rightarrow \neg P(n))$

Informal description

For any decidable predicate $P$ on natural numbers and any natural number $k$, the greatest natural number $\leq k$ satisfying $P$ is zero if and only if for all positive natural numbers $n \leq k$, the predicate $P(n)$ does not hold. In other words: $\text{Nat.findGreatest}\, P\, k = 0 \leftrightarrow \forall n (0 < n \leq k \rightarrow \neg P(n))$

Nat.findGreatest_pos theorem

: 0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Full source

@[simp] lemma findGreatest_pos : 0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n := by
  rw [Nat.pos_iff_ne_zero, Ne, findGreatest_eq_zero_iff]; push_neg; rfl

Positivity of Greatest Satisfying Number: $\text{findGreatest}\, P\, k > 0 \leftrightarrow \exists n (0 < n \leq k \land P(n))$

Informal description

For any decidable predicate $P$ on natural numbers and any natural number $k$, the greatest natural number $\leq k$ satisfying $P$ is positive if and only if there exists a natural number $n$ such that $0 < n \leq k$ and $P(n)$ holds. In other words: $\text{Nat.findGreatest}\, P\, k > 0 \leftrightarrow \exists n (0 < n \leq k \land P(n))$.

Nat.findGreatest_spec theorem

(hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n)

Full source

lemma findGreatest_spec (hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n) := by
  by_cases h : Nat.findGreatest P n = 0
  · cases m
    · rwa [h]
    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim
  · exact (findGreatest_eq_iff.1 rfl).2.1 h

Greatest Satisfying Number Preserves Predicate

Informal description

For any decidable predicate $P$ on natural numbers and natural numbers $m$ and $n$, if $m \leq n$ and $P(m)$ holds, then the greatest natural number $\leq n$ satisfying $P$ also satisfies $P$. In other words, $P(\text{Nat.findGreatest}\, P\, n)$.

Nat.findGreatest_le theorem

(n : ℕ) : Nat.findGreatest P n ≤ n

Full source

lemma findGreatest_le (n : ℕ) : Nat.findGreatest P n ≤ n :=
  (findGreatest_eq_iff.1 rfl).1

Upper Bound Property of Greatest Satisfying Natural Number

Informal description

For any decidable predicate $P$ on natural numbers and any natural number $n$, the greatest natural number $\leq n$ satisfying $P$ is less than or equal to $n$. In other words, $\text{Nat.findGreatest}\, P\, n \leq n$.

Nat.le_findGreatest theorem

(hmb : m ≤ n) (hm : P m) : m ≤ Nat.findGreatest P n

Full source

lemma le_findGreatest (hmb : m ≤ n) (hm : P m) : m ≤ Nat.findGreatest P n :=
  le_of_not_lt fun hlt => (findGreatest_eq_iff.1 rfl).2.2 hlt hmb hm

Lower Bound Property of Greatest Satisfying Natural Number

Informal description

For any decidable predicate $P$ on natural numbers and natural numbers $m$ and $n$, if $m \leq n$ and $P(m)$ holds, then $m$ is less than or equal to the greatest natural number $\leq n$ satisfying $P$. In other words, $m \leq \text{Nat.findGreatest}\, P\, n$.

Nat.findGreatest_mono_right theorem

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

Full source

lemma findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] {m n} (hmn : m ≤ n) :
    Nat.findGreatest P m ≤ Nat.findGreatest P n := by
  induction hmn with
  | refl => simp
  | step hmk ih =>
    rw [findGreatest_succ]
    split_ifs
    · exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)
    · exact ih

Monotonicity of Greatest Satisfying Natural Number with Respect to Upper Bound

Informal description

For any decidable predicate $ P $ on natural numbers and any natural numbers $ m $ and $ n $ such that $ m \leq n $, the greatest natural number $ \leq m $ satisfying $ P $ is less than or equal to the greatest natural number $ \leq n $ satisfying $ P $. In other words, $ \text{Nat.findGreatest}\, P\, m \leq \text{Nat.findGreatest}\, P\, n $.

Nat.findGreatest_mono_left theorem

[DecidablePred Q] (hPQ : ∀ n, P n → Q n) (n : ℕ) : Nat.findGreatest P n ≤ Nat.findGreatest Q n

Full source

lemma findGreatest_mono_left [DecidablePred Q] (hPQ : ∀ n, P n → Q n) (n : ℕ) :
    Nat.findGreatest P n ≤ Nat.findGreatest Q n := by
  induction n with
  | zero => rfl
  | succ n hn =>
    by_cases h : P (n + 1)
    · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
    · rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

Monotonicity of Greatest Satisfier with Respect to Predicate Strength

Informal description

For any decidable predicates $ P $ and $ Q $ on natural numbers such that $ P(n) $ implies $ Q(n) $ for all $ n $, and for any natural number $ n $, the greatest natural number $ \leq n $ satisfying $ P $ is less than or equal to the greatest natural number $ \leq n $ satisfying $ Q $. In other words, $ \text{Nat.findGreatest}\, P\, n \leq \text{Nat.findGreatest}\, Q\, n $.

Nat.findGreatest_mono theorem

[DecidablePred Q] (hPQ : ∀ n, P n → Q n) (hmn : m ≤ n) : Nat.findGreatest P m ≤ Nat.findGreatest Q n

Full source

lemma findGreatest_mono [DecidablePred Q] (hPQ : ∀ n, P n → Q n) (hmn : m ≤ n) :
    Nat.findGreatest P m ≤ Nat.findGreatest Q n :=
  le_trans (Nat.findGreatest_mono_right _ hmn) (findGreatest_mono_left hPQ _)

Monotonicity of Greatest Satisfier with Respect to Predicate Strength and Upper Bound

Informal description

For any decidable predicates $ P $ and $ Q $ on natural numbers such that $ P(n) $ implies $ Q(n) $ for all $ n $, and for any natural numbers $ m $ and $ n $ with $ m \leq n $, the greatest natural number $ \leq m $ satisfying $ P $ is less than or equal to the greatest natural number $ \leq n $ satisfying $ Q $. In other words, $ \text{Nat.findGreatest}\, P\, m \leq \text{Nat.findGreatest}\, Q\, n $.

Nat.findGreatest_is_greatest theorem

(hk : Nat.findGreatest P n < k) (hkb : k ≤ n) : ¬P k

Full source

theorem findGreatest_is_greatest (hk : Nat.findGreatest P n < k) (hkb : k ≤ n) : ¬P k :=
  (findGreatest_eq_iff.1 rfl).2.2 hk hkb

No Larger Number Satisfies Predicate Beyond Greatest Found

Informal description

For a decidable predicate $P$ on natural numbers, if $k$ is a natural number such that $\text{Nat.findGreatest}\, P\, n < k \leq n$, then $P(k)$ does not hold.

Nat.findGreatest_of_ne_zero theorem

(h : Nat.findGreatest P n = m) (h0 : m ≠ 0) : P m

Full source

theorem findGreatest_of_ne_zero (h : Nat.findGreatest P n = m) (h0 : m ≠ 0) : P m :=
  (findGreatest_eq_iff.1 h).2.1 h0

Nonzero Greatest Satisfying Number Satisfies Predicate

Informal description

For a decidable predicate $P$ on natural numbers, if $\text{Nat.findGreatest}\, P\, n = m$ and $m \neq 0$, then $P(m)$ holds.