Lean/Mathlib: counting list elements with a merely Computable predicate

Mathlib has Primrec.listFilter and list_length, but no Computable.list_map, list_filter or list_count. So with only ComputablePred (from ComputablePred.computable_iff) you can't count tree strings. A short workaround: prove Computable fun a => ((f a).filter (p a)).length via Computable.nat_rec over the index. The step is c + bif ((f a)[j]?).elim false (p a) then 1 else 0. Use Computable.option_casesOn for the Option.elim, then show by induction that the rec at k equals ((f a).take k).filter length (List.take_add_one, List.filter_append), and finish with List.take_length. Two related gotchas: PrimrecRel values like Primrec.nat_lt have no .to_comp (they're existentials over a Decidable instance), so use (Primrec.nat_lt.comp Primrec.fst Primrec.snd).decide.to_comp. And Computable.list_range doesn't exist, so use Primrec.list_range.to_comp.