Struggling with List.filter

Stream: Is there code for X?

[Michael Stoll]

While trying to prove the Euler product for the Riemann zeta function, I found myself in a situation where I need something like the following.

import Mathlib

example {α} (P : α → Prop) [DecidablePred P] (l : List α) : l.filter P ++ l.filter (¬ P ·) ~ l := sorry

(Side question: in mathlib3, list.filter had a α → Prop argument. In Mathlib, it is α → Bool, which induces lots of decide (blah) terms coming up in the code. I assume there is a CS reason for this change, bit it seems to make life more difficult when you just want to prove things. Is there an alternative that uses Prop instead?)

In any case, what would be a good way to prove the above? (It looks like it should be in Mathlib anyway...)

[Yaël Dillies]

Answer to side question: No :sad:

[Michael Stoll]

Just out of curiosity: Can somebody elaborate on the reasons for going from Prop to Bool?

[Michael Stoll]

Here is an attempt:

example {α} [DecidableEq α] (P : α → Prop) [DecidablePred P] (l : List α) :
    l.filter P ++ l.filter (¬ P ·) ~ l := by
  refine List.perm_iff_count.mpr fun a ↦ ?_
  rw [List.count_append]
  induction l with
  | nil => simp
  | cons head tail ih =>
      rcases eq_or_ne head a with rfl | ha
      · by_cases h : P head <;> simpa [h] using ih
      · by_cases h : P head <;> simpa [h, List.count_cons_of_ne ha.symm] using ih

But my feeling is there should be something more direct than going via counting occurrences...

[Michael Stoll]

(It also needs an additional DecidableEq instance.)

[Yaël Dillies]

Do you know about docs#List.perm_iff_count ?

[Michael Stoll]

In a similar context, I needed to add

local instance {α : Type*} : Trans (@List.Perm α) (@List.Perm α) (@List.Perm α) where
  trans := @List.Perm.trans α

to be able to use calc with list permutations. Should this be an instance in Mathlib?

[Michael Stoll]

Yaël Dillies said:

Do you know about docs#List.perm_iff_count ?

Yes, as you can see from the proof above.

[Yaël Dillies]

Then I don't understand what you mean by

But my feeling is there should be something more direct that going via counting occurrences...

[Yaël Dillies]

Certainly

  induction l with
  | nil => simp
  | cons head tail ih =>
      rcases eq_or_ne head a with rfl | ha
      · by_cases h : P head <;> simpa [h] using ih
      · by_cases h : P head <;> simpa [h, List.count_cons_of_ne ha.symm] using ih

should be its own lemma, if that's what you mean.

[Michael Stoll]

Yaël Dillies said:

Then I don't understand what you mean by

But my feeling is there should be something more direct that going via counting occurrences...

Typo, it should read "than", not "that" :smile:

[Yaël Dillies]

Ah! My feeling is that this is the most direct.

[Michael Stoll]

OK. Will try to PR the two lemmas later (the one you separated out above and the original one using the other one).

[Michael Stoll]

What would be a good file for these to go in?
#find_home suggests Mathlib.Data.Nat.Order.Basic, which is not what I would have expected...

[Michael Stoll]

I think for my original statement, Mathlib.Data.List.Perm is appropriate.
Yaël's lemma needs only List.count and List.filter. This could perhaps go into Mathlib.Data.List.Lemmas?

[Yaël Dillies]

Data.List.Count is where my lemma should go

[Michael Stoll]

#8189 for the Trans instance and Yaël's lemma. The other lemma is essentially covered by docs#List.filter_append_perm (which I noticed by looking for occurrences of filterin Data.List.Perm while trying to find a good place for the lemma).

[Antoine Chambert-Loir]

Equivalence of lists corresponds to equality of multisets, so I'd be tempted to compare the two multisets, in the hope that more API exists for them.

[Kyle Miller]

Indeed:

example {α} [DecidableEq α] (P : α → Prop) [DecidablePred P] (l : List α) :
    l.filter P ++ l.filter (¬ P ·) ~ l := by
  simp_rw [← Multiset.coe_eq_coe, ← Multiset.coe_add, ←Multiset.coe_filter, Multiset.filter_add_not]