English
Let α be a type with decidable equality, l a finite list of α, and x an element of α. The number of occurrences of the list x :: l inside the list permutations'Aux x l equals 1 plus the length of the initial run of x's at the front of l. In other words, the count of x :: l in permutations'Aux x l is 1 + |{ prefix of l consisting only of x }|.
Русский
Пусть α — тип с разрешённым равенством, l — конечный список элементов α, и x — элемент α. Число вхождений списка x :: l в список permutations'Aux x l равно 1 плюс длина максимального префикса l, состоящего из x. Иными словами, количество вхождений x :: l в permutations'Aux x l равно 1 + длина максимального префикса l, где каждый элемент равен x.
LaTeX
$$$\operatorname{count}(x :: l)\; (\operatorname{permutations'Aux} x l) = \operatorname{length}(\operatorname{takeWhile}(\lambda y. x = y)\, l) + 1$$$
Lean4
theorem count_permutations'Aux_self [DecidableEq α] (l : List α) (x : α) :
count (x :: l) (permutations'Aux x l) = length (takeWhile (x = ·) l) + 1 := by
induction l generalizing x with
| nil => simp [takeWhile, count]
| cons y l IH =>
rw [permutations'Aux, count_cons_self]
by_cases hx : x = y
· subst hx
simpa [takeWhile, Nat.succ_inj, DecEq_eq] using IH _
· rw [takeWhile]
simp only [mem_map, cons.injEq, Ne.symm hx, false_and, and_false, exists_false, not_false_iff,
count_eq_zero_of_not_mem, Nat.zero_add, hx, decide_false, length_nil]
