English
Let l be alternating. For any boolean b, 2 × count b l equals: length l if its length is even; otherwise length l + 1 if the head of l is b, else length l − 1.
Русский
Пусть l — чередующийся список. Для любого b ∈ {true,false} имеем: 2 × count b l равно длине l, если длина l чётна; иначе равно длине l + 1, если первый элемент списка равен b, иначе длине l − 1.
LaTeX
$$$$\forall l : \text{List Bool},\ \text{IsChain}(\\neq) l \rightarrow \forall b \in \{\\text{true},\\text{false}\},\\ \\ 2 \cdot \#\{ i \mid l_i = b \} =\\begin{cases}|l|, & \text{if } \operatorname{Even}(|l|) \\ \\ |l|+1, & \text{if } |l| \text{ is odd and head}(l) = b \\ |l|-1, & \text{if } |l| \text{ is odd and head}(l) \neq b \\ \end{cases}.$$$$
Lean4
theorem two_mul_count_bool_eq_ite (hl : IsChain (· ≠ ·) l) (b : Bool) :
2 * count b l =
if Even (length l) then length l else if Option.some b == l.head? then length l + 1 else length l - 1 :=
by
by_cases h2 : Even (length l)
· rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
· rcases l with - | ⟨x, l⟩
· exact (h2 .zero).elim
simp only [if_neg h2, count_cons, mul_add, head?]
rw [length_cons, Nat.even_add_one, not_not] at h2
replace hl : l.IsChain (· ≠ ·) := hl.tail
rw [hl.two_mul_count_bool_of_even h2]
cases b <;> cases x <;> split_ifs <;> simp <;> contradiction
