List counts and scan bounds

Main results

• List.length_flatMap_le: blocks of bounded length have bounded total length.
• List.length_flatMap_of_forall_length_eq: blocks of a common length k have total length |l| k.
• List.decide_mem_eq_any: membership as a scan of the list.
• List.not_any_one_lt_countP_iff_nodup: duplicate-freeness as a scan of the list.
• List.countP_and_not_add_countP_and: members satisfying one predicate split by whether they satisfy another.
• List.existsUnique_fin_of_countP_eq_one, List.existsUnique_mem_of_countP_eq_one: a Boolean predicate with countP equal to 1 holds at a unique list index and at a unique member.

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.length_flatMap_of_forall_length_eq {α : 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 exactly k elements each, one for each element of l, have exactly |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.not_any_one_lt_countP_iff_nodup {α : Type u_1} [DecidableEq α] (l : List α) : (!l.any fun (a : α) => decide (1 < countP (fun (b : α) => decide (b = a)) l)) = true ↔ l.Nodup

Duplicate-freeness as a scan of the list: no member occurs more than once, counted with countP. This is the form in which polynomial-time tests for repetitions 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.

theorem List.existsUnique_fin_of_countP_eq_one {α : Type u_1} {l : List α} {p : α → Bool} (h : countP p l = 1) : ∃! i : Fin l.length, p l[i] = true

If l.countP p = 1, there is a unique index i : Fin l.length with p l[i] = true.

theorem List.existsUnique_mem_of_countP_eq_one {α : Type u_1} {l : List α} {p : α → Bool} (h : countP p l = 1) : ∃! a : α, a ∈ l ∧ p a = true

If l.countP p = 1, there is a unique element a satisfying a ∈ l ∧ p a = true.