List of Booleans

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

@[simp]

theorem List.count_not_add_count (l : List Bool) (b : Bool) : count (!b) l + count b l = l.length

@[simp]

theorem List.count_add_count_not (l : List Bool) (b : Bool) : count b l + count (!b) l = l.length

@[simp]

theorem List.count_false_add_count_true (l : List Bool) : count false l + count true l = l.length

@[simp]

theorem List.count_true_add_count_false (l : List Bool) : count true l + count false l = l.length

theorem List.IsChain.count_not_cons {b : Bool} {l : List Bool} : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) (b :: l) → count (!b) l = count b l + l.length % 2

theorem List.IsChain.count_not_eq_count {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (h2 : Even l.length) (b : Bool) : count (!b) l = count b l

theorem List.IsChain.count_false_eq_count_true {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (h2 : Even l.length) : count false l = count true l

theorem List.IsChain.count_not_le_count_add_one {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (b : Bool) : count (!b) l ≤ count b l + 1

theorem List.IsChain.count_false_le_count_true_add_one {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) : count false l ≤ count true l + 1

theorem List.IsChain.count_true_le_count_false_add_one {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) : count true l ≤ count false l + 1

theorem List.IsChain.two_mul_count_bool_of_even {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (h2 : Even l.length) (b : Bool) : 2 * count b l = l.length

theorem List.IsChain.two_mul_count_bool_eq_ite {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (b : Bool) : 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

theorem List.IsChain.length_sub_one_le_two_mul_count_bool {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (b : Bool) : l.length - 1 ≤ 2 * count b l

theorem List.IsChain.length_div_two_le_count_bool {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (b : Bool) : l.length / 2 ≤ count b l

theorem List.IsChain.two_mul_count_bool_le_length_add_one {l : List Bool} (hl : IsChain (fun (x1 x2 : Bool) => x1 ≠ x2) l) (b : Bool) : 2 * count b l ≤ l.length + 1