proposition: Lemma Partition_Add : forall m m' x e , ~In x m -> Add x e m m' -> forall m1 m2, Partition m' m1 m2 -> exists m3, (Add x e m3 m1 /\ Partition m m3 m2 \/ Add x e m3 m2 /\ Partition m m1 m3).
proof: Proof. unfold Partition. intros m m' x e Hn Hadd m1 m2 (Hdisj,Hor). assert (Heq : m == remove x m'). { change (m' == add x e m) in Hadd. rewrite Hadd. intro k. rewrite remove_o, add_o. destruct K.eq_dec as [He|Hne]; auto. rewrite <- He, <- not_find_in_iff; auto. } assert (H : MapsTo x e m'). { change (m' == add x e m) in Hadd; rewrite Hadd. apply add_1; auto with map. } rewrite Hor in H; destruct H. - exists (remove x m1); left. split; [|split]. + change (m1 == add x e (remove x m1)). intro k. rewrite add_o, remove_o. destruct K.eq_dec as [He|Hne]; auto. rewrite <- He; apply find_1; auto. + intros k (H1,H2). elim (Hdisj k). split; auto. rewrite remove_in_iff in H1; destruct H1; auto. + intros k' e'. rewrite Heq, 2 remove_mapsto_iff, Hor. intuition. elim (Hdisj x); split; [exists e|exists e']; auto. apply MapsTo_1 with k'; auto with map. - exists (remove x m2); right. split; [|split]. + change (m2 == add x e (remove x m2)). intro k. rewrite add_o, remove_o. destruct K.eq_dec as [He|Hne]; auto. rewrite <- He; apply find_1; auto. + intros k (H1,H2). elim (Hdisj k). split; auto. rewrite remove_in_iff in H2; destruct H2; auto. + intros k' e'. rewrite Heq, 2 remove_mapsto_iff, Hor. intuition. elim (Hdisj x); split; [exists e'|exists e]; auto. apply MapsTo_1 with k'; auto with map. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)