proposition: Lemma map_lookup_filter m i : filter P m !! i = x ← m !! i; guard (P (i,x));; Some x.
proof: Proof. revert m i. apply (map_fold_ind (λ m1 m2, ∀ i, m1 !! i = x ← m2 !! i; guard (P (i,x));; Some x)); intros i. { by rewrite lookup_empty. } intros y m m' Hm IH j. case (decide (j = i))as [->|?]. - case_decide. + rewrite !lookup_insert. simpl. by rewrite option_guard_True. + rewrite lookup_insert. simpl. by rewrite option_guard_False, IH, Hm. - case_decide. + by rewrite !lookup_insert_ne by done. + by rewrite !lookup_insert_ne. Qed.
imports: Coq(Permutation) stdpp(options)