## Stream: Coq users

### Topic: List.filter respects Setoid Equality (equivlistA)

#### Mukesh Tiwari (Dec 08 2022 at 08:55):

I am trying to prove this simple lemma with the equivalence relation `equivlistA` defined in Coq.Lists.SetoidList. However, I can't finish the proof. Any idea how process the induction case?

``````From Coq Require Import List Psatz
SetoidList.
Require Import Utf8.
Import ListNotations.

Section Filter.
Variables
(A : Type)
(eqA : A -> A -> Prop).

Local Notation "a =S= b" :=
(equivlistA eqA a b) (at level 70).

Lemma filter_congruence_gen :
forall X Y f,
X =S= Y ->
List.filter f X =S=
List.filter f Y.
Proof.
induction X.
+ intros ? ? Ha.
apply equivlist_equiv in Ha.
apply equivlistA_nil_eq in Ha.
rewrite Ha.
+ intros ? ? Ha.
(* Do I need decidable equality of A?
(eq_dec : A -> A -> bool?)
In_dec eq_dec a X + ~In_dec eq_dec a X
1. In_dec eq_dec a X  (a ∈ X)
I can write
a :: X =S= X  (1)
from Ha: X =S= Y
I can also infer
filter f (a :: X) =S= filter f X (because a ∈ X)
I can use induction hypothesis.

2. ~In_dec eq_dec a X
Y = Y₁ ++ Y₂ where
Y₁ = List.filter (fun x => eq_dec a x) Y
Y₂ = List.filter (fun x => negb (eq_dec a x)) Y
Y =S= a :: Y₂ (I am disregarding Y₁)
Now from
a :: X =S= a :: Y₂ I have
Hd: X =S= Y₂
specialize (IHX Y₂ f Hd), I get
He : filter f X =S= filter f Y₁

*)
``````

#### Li-yao (Dec 08 2022 at 09:25):

You need to assume that `f` gives the same answer for equivalent elements.

#### Mukesh Tiwari (Dec 08 2022 at 09:28):

You mean `(forall x y : A, eq_dec x y = true -> eq_dec (f x) (f y) = true)`?

#### Gaëtan Gilbert (Dec 08 2022 at 09:31):

no, `Proper (eqA ==> eq) f`
also using induction seems like the wrong way to prove this, instead you should use a lemma relating filter and InA (`filter_InA`)

Last updated: Oct 04 2023 at 23:01 UTC