List counts and scan bounds

Main results

• List.length_flatMap_le: blocks of bounded length have bounded total length.
• List.decide_mem_eq_any: membership as a scan of the list.
• List.countP_and_not_add_countP_and: members satisfying one predicate split by whether they satisfy another.

theorem List.length_flatMap_le {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {k : ℕ} (h : ∀ (a : α), a ∈ l → (f a).length ≤ k) : (flatMap f l).length ≤ l.length * k

Blocks of at most k elements each, one for each element of l, have at most |l| k elements in total.

theorem List.decide_mem_eq_any {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : decide (a ∈ l) = l.any fun (u : α) => decide (u = a)

Membership in a list as a scan of the list, the form in which polynomial-time membership tests are certified.

theorem List.countP_and_not_add_countP_and {α : Type u_1} (p q : α → Prop) [DecidablePred p] [DecidablePred q] (l : List α) : countP (fun (a : α) => decide (¬q a ∧ p a)) l + countP (fun (a : α) => decide (p a ∧ q a)) l = countP (fun (a : α) => decide (p a)) l

Partitioning the elements of a list satisfying p by whether they satisfy q.