English
For any list l and predicate p, the value of find? p on l equals the head of the list obtained by dropping elements not satisfying p: l.find? p = (l.dropWhile (λ x, ¬ p x)).head?
Русский
Для списка l и предиката p значение find? p на l равно голове списка, полученного путём отброса элементов, не удовлетворяющих p: l.find? p = (l.dropWhile (λ x, ¬ p x)).head?
LaTeX
$$$$ l.find?\\,p = (l.dropWhile (\\lambda x \\mapsto \\neg p(x))).head? $$$$
Lean4
theorem find?_eq_head?_dropWhile_not : l.find? p = (l.dropWhile (fun x ↦ !(p x))).head? :=
by
induction l
case nil => simp
case cons head tail hi =>
set ph := p head with phh
rcases ph with rfl | rfl
· have phh' : ¬(p head = true) := by simp [phh.symm]
rw [find?_cons_of_neg phh', dropWhile_cons_of_pos]
· exact hi
· simpa using phh
· rw [find?_cons_of_pos phh.symm, dropWhile_cons_of_neg]
· simp
· simpa using phh
