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.
You mean (forall x y : A, eq_dec x y = true -> eq_dec (f x) (f y) = true)
?
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 13 2024 at 01:02 UTC