Stream: Coq users

Topic: List.filter respects Setoid Equality (equivlistA)


view this post on Zulip 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.
      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₁



      *)

view this post on Zulip Li-yao (Dec 08 2022 at 09:25):

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

view this post on Zulip 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)?

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC