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.
      admit.
      admit.
      admit.
    + 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₁



      *)