proposition: Lemma filter_alt (f:key->elt->bool) m : filter f m == fold (fun k e m => if f k e then add k e m else m) m empty.
proof: Proof. intros x. rewrite fold_spec_right, bindings_o, filter_spec. rewrite findA_rev, filter_rev by apply NoDupA_filter, bindings_spec2w. change K.t with key in *. induction (rev (bindings m)) as [|(y,e) l IH]; simpl. - now rewrite empty_o. - unfold uncurry at 1; simpl. destruct (f y e) eqn:E; simpl; auto. unfold eqb at 1. destruct K.eq_dec as [->|NE]. + now rewrite add_spec1. + rewrite add_spec2; auto. now contradict NE. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)