proposition: Lemma fold_rec : forall {A}(P : t elt -> A -> Type)(f : key -> elt -> A -> A), forall i m, (forall m, Empty m -> P m i) -> (forall k e a m' m'', MapsTo k e m -> ~In k m' -> Add k e m' m'' -> P m' a -> P m'' (f k e a)) -> P m (fold f m i).
proof: Proof. intros A P f i m Hempty Hstep. rewrite fold_spec_right. set (F:=uncurry f). set (l:=rev (bindings m)). assert (Hstep' : forall k e a m' m'', InA eqke (k,e) l -> ~In k m' -> Add k e m' m'' -> P m' a -> P m'' (F (k,e) a)). { intros k e a m' m'' H ? ? ?; eapply Hstep; eauto. revert H; unfold l; rewrite InA_rev, bindings_mapsto_iff; auto with *. } assert (Hdup : NoDupA eqk l). { unfold l. apply NoDupA_rev; try red; unfold eq_key ; eauto with *. apply bindings_3w. } assert (Hsame : forall k, find k m = findA (eqb k) l). { intros k. unfold l. rewrite bindings_o, findA_rev; auto. apply bindings_3w. } clearbody l. clearbody F. clear Hstep f. revert m Hsame. induction l. - intros m Hsame; simpl. apply Hempty. intros k e. rewrite find_mapsto_iff, Hsame; simpl; discriminate. - intros m Hsame; destruct a as (k,e); simpl. apply Hstep' with (of_list l); auto. + rewrite InA_cons; left; compute; auto with map. + inversion_clear Hdup. contradict H. destruct H as (e',He'). apply InA_eqke_eqk with k e'; auto with map. rewrite <- of_list_1; auto. + intro k'. rewrite Hsame, add_o, of_list_1b. simpl. rewrite eqb_sym. unfold eqb. now destruct K.eq_dec. inversion_clear Hdup; auto with map. + apply IHl. * intros; eapply Hstep'; eauto. * inversion_clear Hdup; auto. * intros; apply of_list_1b. inversion_clear Hdup; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)