data.bool.count

# List of booleans #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove lemmas about the number of ffs and tts in a list of booleans. First we prove that the number of ffs plus the number of tt equals the length of the list. Then we prove that in a list with alternating tts and ffs, the number of tts differs from the number of ffs by at most one. We provide several versions of these statements.

@[simp]
theorem list.count_bnot_add_count (l : list bool) (b : bool) :
list.count (!b) l + l = l.length
@[simp]
theorem list.count_add_count_bnot (l : list bool) (b : bool) :
l + list.count (!b) l = l.length
@[simp]
@[simp]
theorem list.chain.count_bnot {b : bool} {l : list bool} :
l list.count (!b) l = l + l.length % 2
theorem list.chain'.count_bnot_eq_count {l : list bool} (hl : l) (h2 : even l.length) (b : bool) :
list.count (!b) l = l
theorem list.chain'.count_ff_eq_count_tt {l : list bool} (hl : l) (h2 : even l.length) :
theorem list.chain'.count_bnot_le_count_add_one {l : list bool} (hl : l) (b : bool) :
list.count (!b) l l + 1
theorem list.chain'.two_mul_count_bool_of_even {l : list bool} (hl : l) (h2 : even l.length) (b : bool) :
2 * l = l.length
theorem list.chain'.two_mul_count_bool_eq_ite {l : list bool} (hl : l) (b : bool) :
2 * l = ite (even l.length) l.length (ite (b l.head') (l.length + 1) (l.length - 1))
theorem list.chain'.length_div_two_le_count_bool {l : list bool} (hl : l) (b : bool) :
l.length / 2 l