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) : List.count (!b) l + List.count b l = List.length l

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.Chain.count_not {b : Bool} {l : List Bool} : List.Chain (fun (x x_1 : Bool) => x ≠ x_1) b l → List.count (!b) l = List.count b l + List.length l % 2

theorem List.Chain'.count_not_eq_count {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) (h2 : Even (List.length l)) (b : Bool) : List.count (!b) l = List.count b l

theorem List.Chain'.count_false_eq_count_true {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) (h2 : Even (List.length l)) : List.count false l = List.count true l

theorem List.Chain'.count_not_le_count_add_one {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) (b : Bool) : List.count (!b) l ≤ List.count b l + 1

theorem List.Chain'.count_false_le_count_true_add_one {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) : List.count false l ≤ List.count true l + 1

theorem List.Chain'.count_true_le_count_false_add_one {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) : List.count true l ≤ List.count false l + 1

theorem List.Chain'.two_mul_count_bool_of_even {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) (h2 : Even (List.length l)) (b : Bool) : 2 * List.count b l = List.length l

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

theorem List.Chain'.length_sub_one_le_two_mul_count_bool {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) (b : Bool) : List.length l - 1 ≤ 2 * List.count b l

theorem List.Chain'.length_div_two_le_count_bool {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) (b : Bool) : List.length l / 2 ≤ List.count b l

theorem List.Chain'.two_mul_count_bool_le_length_add_one {l : List Bool} (hl : List.Chain' (fun (x x_1 : Bool) => x ≠ x_1) l) (b : Bool) : 2 * List.count b l ≤ List.length l + 1