chore(Algebra/FreeMonoid/Count): remove defeq abuse around FreeMonoid.countP (#20156)

as requested on [zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.2FAlgebra.2FFreeMonoid.2FCount.2Elean)



Co-authored-by: blizzard_inc <edegeltje@gmail.com>

Author: edegeltje

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -121,7 +121,7 @@ variable {a : FreeMonoid α}
 /-- The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length -/
 @[to_additive "The length of an additive free monoid element: 1.length = 0 and (a + b).length =
   a.length + b.length"]
-def length (a : FreeMonoid α) : ℕ := List.length a
+def length (a : FreeMonoid α) : ℕ := a.toList.length
 
 @[to_additive (attr := simp)]
 theorem length_one : length (1 : FreeMonoid α) = 0 := rfl

Mathlib/Algebra/FreeMonoid/Count.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.FreeMonoid.Basic
-import Mathlib.Algebra.Group.TypeTags.Hom
+import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-!
 # `List.count` as a bundled homomorphism
@@ -13,73 +13,76 @@ In this file we define `FreeMonoid.countP`, `FreeMonoid.count`, `FreeAddMonoid.c
 `FreeAddMonoid.count`. These are `List.countP` and `List.count` bundled as multiplicative and
 additive homomorphisms from `FreeMonoid` and `FreeAddMonoid`.
 
-We do not use `to_additive` because it can't map `Multiplicative ℕ` to `ℕ`.
+We do not use `to_additive` too much because it can't map `Multiplicative ℕ` to `ℕ`.
+-/
 
-## TODO
+variable {α : Type*} (p : α → Prop) [DecidablePred p]
 
-There is lots of defeq abuse here of `FreeAddMonoid α = List α`, e.g. in statements like
-```
-theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rfl
-```
-This needs cleaning up.
+namespace FreeMonoid
+/-- `List.countP` lifted to free monoids-/
+@[to_additive "`List.countP` lifted to free additive monoids"]
+def countP' (l : FreeMonoid α) : ℕ := l.toList.countP p
 
--/
+@[to_additive]
+lemma countP'_one : (1 : FreeMonoid α).countP' p = 0 := rfl
 
-variable {α : Type*} (p : α → Prop) [DecidablePred p]
+@[to_additive]
+lemma countP'_mul (l₁ l₂ : FreeMonoid α) : (l₁ * l₂).countP' p = l₁.countP' p + l₂.countP' p := by
+  dsimp [countP']
+  simp only [List.countP_append]
 
-namespace FreeAddMonoid
+/-- `List.countP` as a bundled multiplicative monoid homomorphism. -/
+def countP : FreeMonoid α →* Multiplicative ℕ where
+  toFun := .ofAdd ∘ FreeMonoid.countP' p
+  map_one' := by
+    simp [countP'_one p]
+  map_mul' x y := by
+    simp [countP'_mul p]
 
-/-- `List.countP` as a bundled additive monoid homomorphism. -/
-def countP : FreeAddMonoid α →+ ℕ where
-  toFun := List.countP p
-  map_zero' := List.countP_nil _
-  map_add' := List.countP_append _
+theorem countP_apply (l : FreeMonoid α) : l.countP p = .ofAdd (l.toList.countP p) := rfl
 
-theorem countP_of (x : α) : countP p (of x) = if p x = true then 1 else 0 := by
-  change List.countP p [x] = _
-  simp [List.countP_cons]
+lemma countP_of (x : α) : (of x).countP p =
+    if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by
+  rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]
+  simp only [decide_eq_true_eq]
 
-theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rfl
 
 /-- `List.count` as a bundled additive monoid homomorphism. -/
--- Porting note: was (x = ·)
-def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ := countP (· = x)
-
-theorem count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y := by
-  change List.count x [y] = _
-  simp [Pi.single, Function.update, List.count_cons]
+def count [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ := countP (· = x)
 
-theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) : count x l = List.count x l :=
-  rfl
+theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) :
+    count x l = Multiplicative.ofAdd (l.toList.count x) := rfl
 
-end FreeAddMonoid
+theorem count_of [DecidableEq α] (x y : α) :
+    count x (of y) = Pi.mulSingle (f := fun _ => Multiplicative ℕ) x (Multiplicative.ofAdd 1) y :=
+  by simp only [count, eq_comm, countP_of, ofAdd_zero, Pi.mulSingle_apply]
 
-namespace FreeMonoid
+end FreeMonoid
 
-/-- `List.countP` as a bundled multiplicative monoid homomorphism. -/
-def countP : FreeMonoid α →* Multiplicative ℕ :=
-    AddMonoidHom.toMultiplicative (FreeAddMonoid.countP p)
+namespace FreeAddMonoid
 
-theorem countP_of' (x : α) :
-    countP p (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by
-    erw [FreeAddMonoid.countP_of]
-    simp only [eq_iff_iff, iff_true, ofAdd_zero]; rfl
+/-- `List.countP` as a bundled additive monoid homomorphism. -/
+def countP : FreeAddMonoid α →+ ℕ where
+  toFun := FreeAddMonoid.countP' p
+  map_zero' := countP'_zero p
+  map_add' := countP'_add p
 
-theorem countP_of (x : α) : countP p (of x) = if p x then Multiplicative.ofAdd 1 else 1 := by
-  rw [countP_of', ofAdd_zero]
+theorem countP_apply (l : FreeAddMonoid α) : l.countP p = l.toList.countP p := rfl
 
--- `rfl` is not transitive
-theorem countP_apply (l : FreeAddMonoid α) : countP p l = Multiplicative.ofAdd (List.countP p l) :=
-  rfl
+theorem countP_of (x : α) : countP p (of x) = if p x then 1 else 0 := by
+  rw [countP_apply, toList_of, List.countP_singleton]
+  simp only [decide_eq_true_eq]
 
 /-- `List.count` as a bundled additive monoid homomorphism. -/
-def count [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ := countP (· = x)
+-- Porting note: was (x = ·)
+def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ := countP (· = x)
 
-theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) :
-    count x l = Multiplicative.ofAdd (List.count x l) := rfl
+lemma count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y := by
+  dsimp [count]
+  rw [countP_of]
+  simp [Pi.single, Function.update]
 
-theorem count_of [DecidableEq α] (x y : α) :
-    count x (of y) = @Pi.mulSingle α (fun _ => Multiplicative ℕ) _ _ x (Multiplicative.ofAdd 1) y :=
-  by simp [count, countP_of, Pi.mulSingle_apply, eq_comm, Bool.beq_eq_decide_eq]
+theorem count_apply [DecidableEq α] (x : α) (l : FreeAddMonoid α) : l.count x = l.toList.count x :=
+  rfl
 
-end FreeMonoid
+end FreeAddMonoid