proposition: Lemma Permutation_filter_elements {B} : forall (f : key -> B -> bool) m (Proper_f : Proper (E.eq ==> eq ==> eq) f), Permutation (List.map snd (elements (filter f m))) (List.map snd (List.filter (fun kv => f (fst kv) (snd kv)) (elements m))).
proof: Proof. intros; apply Permutation_InA_cons; eauto using elements_3w. - pose proof (elements_3w m) as NoDupM. induction NoDupM; simpl in *; simpl; try constructor. case_eq (f (fst x) (snd x)); simpl; eauto. intros; constructor; eauto. unfold not; intros; apply H; clear NoDupM IHNoDupM H; induction l; simpl in *. inversion H0; subst; eauto. case_eq (f (fst a) (snd a)); intros; rewrite H in *; eauto. inversion H1; subst. constructor; eauto. constructor 2; eauto. - intros; rewrite <- elements_mapsto_iff, filter_iff; eauto; intuition. + rewrite elements_mapsto_iff in H0; induction H0. * simpl; destruct H; rewrite Proper_f in H1; eauto; rewrite H1; repeat constructor; eauto. * simpl; destruct (f (fst y) (snd y)); simpl; eauto. + rewrite elements_mapsto_iff; induction (elements m); simpl in *. * inversion H. * case_eq (f (fst a) (snd a)); intros; rewrite H0 in H. inversion H; subst. constructor; eauto. constructor 2; eauto. constructor 2; eauto. + induction (elements m); simpl in *. * inversion H. * case_eq (f (fst a) (snd a)); intros; rewrite H0 in H; eauto. inversion H; subst. destruct H2; rewrite Proper_f in H0; eauto. eauto. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances