English
Let P: N → {true,false} be a decidable predicate and k ∈ N. Then the value findGreatest P k is the greatest m ≤ k with P m, characterized by: m ≤ k, and (m ≠ 0 → P m), and for every n with m < n ≤ k, P n does not hold.
Русский
Пусть P: ℕ → {истина, ложь} является разрешимым предикатом и k ∈ ℕ. Тогда значение findGreatest P k есть наибольший m ≤ k such that P m, и эквивалентно: m ≤ k, и (m ≠ 0 → P m), и для любого n, если m < n ≤ k, то ¬P n.
LaTeX
$$$\mathrm{findGreatest} P k = m \;\Longleftrightarrow\; m \le k \land (m \neq 0 \rightarrow P m) \land \forall n\, (m < n \land n \le k \rightarrow \neg P n).$$$
Lean4
theorem findGreatest_eq_iff : Nat.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 [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 cutsat⟩
| 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 cutsat⟩
· rintro ⟨hle, h0, hm⟩
rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
exacts [(hm hlt (le_refl _) hk).elim, rfl]
· 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.lt_or_eq_of_le hle with hlt' | rfl
exacts [hm hlt <| Nat.lt_succ_iff.1 hlt', hk]
· 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)
