proposition: Lemma fold_Add : forall m1 m2 k e i, ~In k m1 -> Add k e m1 m2 -> eqA (fold f m2 i) (f k e (fold f m1 i)).
proof: Proof. intros. rewrite 2 fold_spec_right. set (f':=uncurry f). change (f k e (fold_right f' i (rev (elements m1)))) with (f' (k,e) (fold_right f' i (rev (elements m1)))). assert (NoDupA eqk (rev (elements m1))) by auto with map typeclass_instances. assert (NoDupA eqk (rev (elements m2))) by auto with map typeclass_instances. apply fold_right_add_restr with (R:=complement eqk)(eqA:=eqke)(eqB:=eqA). 1:auto with typeclass_instances. 1:auto. 2: auto with crelations. 4, 5: auto with map. - intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *. apply Comp; auto. - unfold complement, eq_key_elt, eq_key; repeat red; intuition eauto. - unfold f'; intros (k1,e1) (k2,e2); unfold eq_key, uncurry; simpl; auto. - rewrite <- NoDupA_altdef; auto. - rewrite InA_rev, <- elements_mapsto_iff. firstorder. - intros (a,b). rewrite InA_cons, 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff. unfold eq_key_elt; simpl. rewrite H0. rewrite add_o. destruct (eq_dec k a) as [EQ|NEQ]; split; auto. + intros EQ'; inversion EQ'; auto. + intuition; subst; auto. elim H. exists b; rewrite EQ; auto with map. + intuition. elim NEQ; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface