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 + list.count b l = l.length
@[simp]
theorem
list.count_add_count_bnot
(l : list bool)
(b : bool) :
list.count b l + list.count (!b) l = l.length
@[simp]
theorem
list.count_ff_add_count_tt
(l : list bool) :
list.count bool.ff l + list.count bool.tt l = l.length
@[simp]
theorem
list.count_tt_add_count_ff
(l : list bool) :
list.count bool.tt l + list.count bool.ff l = l.length
theorem
list.chain.count_bnot
{b : bool}
{l : list bool} :
list.chain ne b l → list.count (!b) l = list.count b l + l.length % 2
theorem
list.chain'.count_bnot_eq_count
{l : list bool}
(hl : list.chain' ne l)
(h2 : even l.length)
(b : bool) :
list.count (!b) l = list.count b l
theorem
list.chain'.count_ff_eq_count_tt
{l : list bool}
(hl : list.chain' ne l)
(h2 : even l.length) :
theorem
list.chain'.count_bnot_le_count_add_one
{l : list bool}
(hl : list.chain' ne l)
(b : bool) :
list.count (!b) l ≤ list.count b l + 1
theorem
list.chain'.count_ff_le_count_tt_add_one
{l : list bool}
(hl : list.chain' ne l) :
list.count bool.ff l ≤ list.count bool.tt l + 1
theorem
list.chain'.count_tt_le_count_ff_add_one
{l : list bool}
(hl : list.chain' ne l) :
list.count bool.tt l ≤ list.count bool.ff l + 1
theorem
list.chain'.two_mul_count_bool_of_even
{l : list bool}
(hl : list.chain' ne l)
(h2 : even l.length)
(b : bool) :
2 * list.count b l = l.length
theorem
list.chain'.length_sub_one_le_two_mul_count_bool
{l : list bool}
(hl : list.chain' ne l)
(b : bool) :
l.length - 1 ≤ 2 * list.count b l
theorem
list.chain'.length_div_two_le_count_bool
{l : list bool}
(hl : list.chain' ne l)
(b : bool) :
l.length / 2 ≤ list.count b l
theorem
list.chain'.two_mul_count_bool_le_length_add_one
{l : list bool}
(hl : list.chain' ne l)
(b : bool) :
2 * list.count b l ≤ l.length + 1