proposition: Lemma fold_rec : forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), forall (i:A)(m:t elt), (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 (elements 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, elements_mapsto_iff. auto. } assert (Hdup : NoDupA eqk l). { unfold l. apply NoDupA_rev; try red; unfold eq_key. - auto with typeclass_instances. - apply elements_3w. } assert (Hsame : forall k, find k m = findA (eqb k) l). { intros k. unfold l. rewrite elements_o, findA_rev; auto. apply elements_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; red; auto. + inversion_clear Hdup. contradict H. destruct H as (e',He'). apply InA_eqke_eqk with k e'; auto. rewrite <- of_list_1; auto. + intro k'. rewrite Hsame, add_o, of_list_1b. * simpl. unfold eqb. do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto. * inversion_clear Hdup; auto. + apply IHl. * intros; eapply Hstep'; eauto. * inversion_clear Hdup; auto. * intros; apply of_list_1b. inversion_clear Hdup; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface