proposition: Lemma exists_iff : forall m, exists_ f m = true <-> (exists p, MapsTo (fst p) (snd p) m /\ f (fst p) (snd p) = true).
proof: Proof. unfold exists_. set (f':=fun k e b => if f k e then true else b). intro m. pattern m, (fold f' m false). apply fold_rec. - intros m' Hm'. split; try discriminate. intros ((k,e),(Hke,_)); simpl in *. elim (Hm' k e); auto. - intros k e b m1 m2 _ Hn Hadd IH. clear m. change (Equal m2 (add k e m1)) in Hadd. unfold f'; simpl. case_eq (f k e); intros Hfke. + split; [intros _|auto]. exists (k,e); simpl; split; auto. rewrite Hadd, add_mapsto_iff; auto. + rewrite IH. clear IH. split; intros ((k',e'),(Hke1,Hke2)); simpl in *. * exists (k',e'); simpl; split; auto. rewrite Hadd, add_mapsto_iff; right; split; auto. contradict Hn. exists e'; rewrite Hn; auto. * rewrite Hadd, add_mapsto_iff in Hke1. destruct Hke1 as [(?,?)|(?,?)]. -- assert (f k' e' = f k e) by (apply Hf; auto). congruence. -- exists (k',e'); auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface