proposition: Lemma partition_after_KeyBasedPartition_and_add : forall {TValue} k v' (m: t TValue), Partition (add k v' m) (add k v' (fst (partition (KeyBasedPartitioningFunction TValue k) m))) (snd (partition (KeyBasedPartitioningFunction TValue k) m)).
proof: Proof. unfold Partition. split. { unfold Disjoint. intros key (in_modified & in_unmodified). rewrite add_in_iff in in_modified. assert (E.eq k key) by ( destruct in_modified; [ assumption | eapply In_KeyBasedPartition_fst; eauto ] ); clear in_modified. apply In_KeyBasedPartition_snd in in_unmodified. intuition. } split; intros * maps_to'. rewrite add_mapsto_iff in maps_to'. destruct maps_to' as [ (keq & veq) | (kneq & maps_to') ]; subst. left; apply add_1; eauto. right; rewrite partition_iff_2 with (f := KeyBasedPartitioningFunction TValue k) (m := m) by (eauto using KeyBasedPartitioningFunction_Proper); rewrite <- KeyBasedPartitioningFunction_eq_false; intuition. destruct maps_to' as [ maps_to' | maps_to' ]. rewrite add_mapsto_iff in maps_to'; destruct maps_to' as [ (keq & veq) | (kneq & maps_to') ]; [ subst; apply add_1; assumption | ]. exfalso. apply MapsTo_KeyBasedPartition_fst in maps_to'. intuition. pose proof maps_to'. apply MapsTo_KeyBasedPartition_snd in maps_to'. apply add_2; [ assumption | eapply MapsTo_partition_snd; eauto using KeyBasedPartitioningFunction_Proper ]. 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