proposition: Lemma filter_singular_perm: forall {A} (f g: A -> bool) l x, (forall i, In i l -> i <> x -> f i = g i) -> In x l -> g x = false -> f x = true -> NoDup l -> Permutation (filter f l) (x :: filter g l).
proof: Proof. intros. induction l. 1: inversion H0. simpl. simpl in H0. destruct H0. - subst a. rewrite H1. rewrite H2. constructor. cut (filter f l = filter g l). + intros. rewrite H0. reflexivity. + apply filter_ext. intros. apply H. * simpl; right; assumption. * apply NoDup_cons_2 in H3. intro. subst i. contradiction. - assert (a <> x) by (apply NoDup_cons_2 in H3; intro; subst a; contradiction). assert (f a = g a) by (apply H; [left; reflexivity | assumption]). assert (Permutation (filter f l) (x :: filter g l)). { apply IHl; [intros; apply H; [right|] | |apply NoDup_cons_1 in H3]; assumption. } destruct (f a); destruct (g a); try discriminate; clear H5; [transitivity (a :: x :: filter g l); constructor|]; assumption. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver