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₁ *)
You need to assume that
f gives the same answer for equivalent elements.
(forall x y : A, eq_dec x y = true -> eq_dec (f x) (f y) = true)?
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 (
Last updated: Oct 04 2023 at 23:01 UTC