Lean4
theorem toList_spec (xs : t α) : toList xs = FreeMonoid.toList (foldMap FreeMonoid.of xs) :=
Eq.symm <|
calc
FreeMonoid.toList (foldMap FreeMonoid.of xs) = FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse := by
simp only [FreeMonoid.reverse_reverse]
_ = (List.foldr cons [] (foldMap FreeMonoid.of xs).toList.reverse).reverse := by simp
_ = (unop (Foldl.ofFreeMonoid (flip cons) (foldMap FreeMonoid.of xs)) []).reverse := by
simp [Function.flip_def, List.foldr_reverse, Foldl.ofFreeMonoid, unop_op]
_ = toList xs := by
rw [foldMap_hom_free (Foldl.ofFreeMonoid (flip <| @cons α))]
simp only [toList, foldl, Foldl.get, foldl.ofFreeMonoid_comp_of, Function.comp_apply]
