FMapFacts.v

(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (** * Finite maps library *) (** This functor derives additional facts from [FMapInterface.S]. These facts are mainly the specifications of [FMapInterface.S] written using different styles: equivalence and boolean equalities. *)

Require Import Bool DecidableType DecidableTypeEx OrderedType Morphisms.

Require Export FMapInterface.

Set Implicit Arguments.

Unset Strict Implicit.

Local Ltac Tauto.intuition_solver ::= auto with bool map.

#[global] Hint Extern 1 (Equivalence _) => constructor; congruence : core.

(** * Facts about weak maps *)

Module WFacts_fun (E:DecidableType)(Import M:WSfun E).

Notation eq_dec := E.eq_dec.

Definition eqb x y := if eq_dec x y then true else false.

Lemma eq_bool_alt : forall b b', b=b' <-> (b=true <-> b'=true).

destruct b; destruct b'; intuition.

Lemma eq_option_alt : forall (elt:Type)(o o':option elt), o=o' <-> (forall e, o=Some e <-> o'=Some e).

subst; split; auto.

destruct o; destruct o'; try rewrite H; auto.

symmetry; rewrite <- H; auto.

Lemma MapsTo_fun : forall (elt:Type) m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'.

generalize (find_1 H) (find_1 H0); clear H H0.

intros; rewrite H in H0; injection H0; auto.

(** ** Specifications written using equivalences *)

Variable elt elt' elt'': Type.

Implicit Type m: t elt.

Implicit Type x y z: key.

Implicit Type e: elt.

Lemma In_iff : forall m x y, E.eq x y -> (In x m <-> In y m).

split; intros (e0,H0); exists e0.

apply (MapsTo_1 H H0); auto.

apply (MapsTo_1 (E.eq_sym H) H0); auto.

Lemma MapsTo_iff : forall m x y e, E.eq x y -> (MapsTo x e m <-> MapsTo y e m).

split; apply MapsTo_1; auto.

Lemma mem_in_iff : forall m x, In x m <-> mem x m = true.

split; [apply mem_1|apply mem_2].

Lemma not_mem_in_iff : forall m x, ~In x m <-> mem x m = false.

intros; rewrite mem_in_iff; destruct (mem x m); intuition.

Lemma In_dec : forall m x, { In x m } + { ~ In x m }.

generalize (mem_in_iff m x).

destruct (mem x m); [left|right]; intuition.

Lemma find_mapsto_iff : forall m x e, MapsTo x e m <-> find x m = Some e.

split; [apply find_1|apply find_2].

Lemma not_find_in_iff : forall m x, ~In x m <-> find x m = None.

rewrite eq_option_alt.

rewrite <- find_mapsto_iff.

split; try discriminate.

intro H'; elim H; exists e; auto.

intros (e,He); rewrite find_mapsto_iff,H in He; discriminate.

Lemma in_find_iff : forall m x, In x m <-> find x m <> None.

intros; rewrite <- not_find_in_iff, mem_in_iff.

destruct mem; intuition.

Lemma equal_iff : forall m m' cmp, Equivb cmp m m' <-> equal cmp m m' = true.

split; [apply equal_1|apply equal_2].

Lemma empty_mapsto_iff : forall x e, MapsTo x e (empty elt) <-> False.

intuition; apply (empty_1 H).

Lemma empty_in_iff : forall x, In x (empty elt) <-> False.

split; [intros (e,H); rewrite empty_mapsto_iff in H|]; intuition.

Lemma is_empty_iff : forall m, Empty m <-> is_empty m = true.

split; [apply is_empty_1|apply is_empty_2].

Lemma add_mapsto_iff : forall m x y e e', MapsTo y e' (add x e m) <-> (E.eq x y /\ e=e') \/ (~E.eq x y /\ MapsTo y e' m).

destruct (eq_dec x y); [left|right].

symmetry; apply (MapsTo_fun (e':=e) H); auto with map.

split; auto; apply add_3 with x e; auto.

subst; auto with map.

Lemma add_in_iff : forall m x y e, In y (add x e m) <-> E.eq x y \/ In y m.

destruct (eq_dec x y) as [E|E]; auto.

right; exists e'; auto.

apply (add_3 E H).

destruct (eq_dec x y) as [E|E]; auto.

exists e; apply add_1; auto.

intros [H|(e',H)].

exists e'; apply add_2; auto.

Lemma add_neq_mapsto_iff : forall m x y e e', ~ E.eq x y -> (MapsTo y e' (add x e m) <-> MapsTo y e' m).

split; [apply add_3|apply add_2]; auto.

Lemma add_neq_in_iff : forall m x y e, ~ E.eq x y -> (In y (add x e m) <-> In y m).

split; intros (e',H0); exists e'.

apply (add_3 H H0).

apply add_2; auto.

Lemma remove_mapsto_iff : forall m x y e, MapsTo y e (remove x m) <-> ~E.eq x y /\ MapsTo y e m.

assert (In y (remove x m)) by (exists e; auto).

intro H1; apply (remove_1 H1 H0).

apply remove_3 with x; auto.

apply remove_2; intuition.

Lemma remove_in_iff : forall m x y, In y (remove x m) <-> ~E.eq x y /\ In y m.

assert (In y (remove x m)) by (exists e; auto).

intro H1; apply (remove_1 H1 H0).

exists e; apply remove_3 with x; auto.

intros (H,(e,H0)); exists e; apply remove_2; auto.

Lemma remove_neq_mapsto_iff : forall m x y e, ~ E.eq x y -> (MapsTo y e (remove x m) <-> MapsTo y e m).

split; [apply remove_3|apply remove_2]; auto.

Lemma remove_neq_in_iff : forall m x y, ~ E.eq x y -> (In y (remove x m) <-> In y m).

split; intros (e',H0); exists e'.

apply (remove_3 H0).

apply remove_2; auto.

Lemma elements_mapsto_iff : forall m x e, MapsTo x e m <-> InA (@eq_key_elt _) (x,e) (elements m).

split; [apply elements_1 | apply elements_2].

Lemma elements_in_iff : forall m x, In x m <-> exists e, InA (@eq_key_elt _) (x,e) (elements m).

unfold In; split; intros (e,H); exists e; [apply elements_1 | apply elements_2]; auto.

Lemma map_mapsto_iff : forall m x b (f : elt -> elt'), MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m.

case_eq (find x m); intros.

apply (MapsTo_fun (m:=map f m) (x:=x)); auto with map.

apply find_2; auto with map.

assert (In x (map f m)) by (exists b; auto).

destruct (map_2 H1) as (a,H2).

rewrite (find_1 H2) in H; discriminate.

intros (a,(H,H0)).

subst b; auto with map.

Lemma map_in_iff : forall m x (f : elt -> elt'), In x (map f m) <-> In x m.

split; intros; eauto with map.

destruct H as (a,H).

exists (f a); auto with map.

Lemma mapi_in_iff : forall m x (f:key->elt->elt'), In x (mapi f m) <-> In x m.

split; intros; eauto with map.

destruct H as (a,H).

destruct (mapi_1 f H) as (y,(H0,H1)).

exists (f y a); auto.

(** Unfortunately, we don't have simple equivalences for [mapi] and [MapsTo]. The only correct one needs compatibility of [f]. *)

Lemma mapi_inv : forall m x b (f : key -> elt -> elt'), MapsTo x b (mapi f m) -> exists a y, E.eq y x /\ b = f y a /\ MapsTo x a m.

intros; case_eq (find x m); intros.

destruct (@mapi_1 _ _ m x e f) as (y,(H1,H2)).

apply find_2; auto with map.

exists y; repeat split; auto with map.

apply (MapsTo_fun (m:=mapi f m) (x:=x)); auto with map.

assert (In x (mapi f m)) by (exists b; auto).

destruct (mapi_2 H1) as (a,H2).

rewrite (find_1 H2) in H0; discriminate.

Lemma mapi_1bis : forall m x e (f:key->elt->elt'), (forall x y e, E.eq x y -> f x e = f y e) -> MapsTo x e m -> MapsTo x (f x e) (mapi f m).

destruct (mapi_1 f H0) as (y,(H1,H2)).

replace (f x e) with (f y e) by auto.

Lemma mapi_mapsto_iff : forall m x b (f:key->elt->elt'), (forall x y e, E.eq x y -> f x e = f y e) -> (MapsTo x b (mapi f m) <-> exists a, b = f x a /\ MapsTo x a m).

destruct (mapi_inv H0) as (a,(y,(H1,(H2,H3)))).

exists a; split; auto.

intros (a,(H0,H1)).

apply mapi_1bis; auto.

(** Things are even worse for [map2] : we don't try to state any equivalence, see instead boolean results below. *)

(** Useful tactic for simplifying expressions like [In y (add x e (remove z m))] *)

Ltac map_iff := repeat (progress ( rewrite add_mapsto_iff || rewrite add_in_iff || rewrite remove_mapsto_iff || rewrite remove_in_iff || rewrite empty_mapsto_iff || rewrite empty_in_iff || rewrite map_mapsto_iff || rewrite map_in_iff || rewrite mapi_in_iff)).

(** ** Specifications written using boolean predicates *)

Lemma mem_find_b : forall (elt:Type)(m:t elt)(x:key), mem x m = if find x m then true else false.

generalize (find_mapsto_iff m x)(mem_in_iff m x); unfold In.

destruct (find x m); destruct (mem x m); auto.

rewrite <- H0; exists e; rewrite H; auto.

destruct H0 as (e,H0).

destruct (H e); intuition discriminate.

Variable elt elt' elt'' : Type.

Implicit Types m : t elt.

Implicit Types x y z : key.

Implicit Types e : elt.

Lemma mem_b : forall m x y, E.eq x y -> mem x m = mem y m.

generalize (mem_in_iff m x) (mem_in_iff m y)(In_iff m H).

destruct (mem x m); destruct (mem y m); intuition.

Lemma find_o : forall m x y, E.eq x y -> find x m = find y m.

rewrite eq_option_alt.

rewrite <- 2 find_mapsto_iff.

apply MapsTo_iff; auto.

Lemma empty_o : forall x, find x (empty elt) = None.

rewrite eq_option_alt.

rewrite <- find_mapsto_iff, empty_mapsto_iff; now intuition.

Lemma empty_a : forall x, mem x (empty elt) = false.

case_eq (mem x (empty elt)); intros; auto.

generalize (mem_2 H).

rewrite empty_in_iff; intuition.

Lemma add_eq_o : forall m x y e, E.eq x y -> find y (add x e m) = Some e.

Lemma add_neq_o : forall m x y e, ~ E.eq x y -> find y (add x e m) = find y m.

rewrite eq_option_alt.

rewrite <- 2 find_mapsto_iff.

apply add_neq_mapsto_iff; auto.

#[local] Hint Resolve add_neq_o : map.

Lemma add_o : forall m x y e, find y (add x e m) = if eq_dec x y then Some e else find y m.

intros; destruct (eq_dec x y); auto with map.

Lemma add_eq_b : forall m x y e, E.eq x y -> mem y (add x e m) = true.

intros; rewrite mem_find_b; rewrite add_eq_o; auto.

Lemma add_neq_b : forall m x y e, ~E.eq x y -> mem y (add x e m) = mem y m.

intros; do 2 rewrite mem_find_b; rewrite add_neq_o; auto.

Lemma add_b : forall m x y e, mem y (add x e m) = eqb x y || mem y m.

intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb.

destruct (eq_dec x y); simpl; auto.

Lemma remove_eq_o : forall m x y, E.eq x y -> find y (remove x m) = None.

rewrite eq_option_alt.

rewrite <- find_mapsto_iff, remove_mapsto_iff; now intuition.

#[local] Hint Resolve remove_eq_o : map.

Lemma remove_neq_o : forall m x y, ~ E.eq x y -> find y (remove x m) = find y m.

rewrite eq_option_alt.

rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition.

#[local] Hint Resolve remove_neq_o : map.

Lemma remove_o : forall m x y, find y (remove x m) = if eq_dec x y then None else find y m.

intros; destruct (eq_dec x y); auto with map.

Lemma remove_eq_b : forall m x y, E.eq x y -> mem y (remove x m) = false.

intros; rewrite mem_find_b; rewrite remove_eq_o; auto.

Lemma remove_neq_b : forall m x y, ~ E.eq x y -> mem y (remove x m) = mem y m.

intros; do 2 rewrite mem_find_b; rewrite remove_neq_o; auto.

Lemma remove_b : forall m x y, mem y (remove x m) = negb (eqb x y) && mem y m.

intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb.

destruct (eq_dec x y); auto.

Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = Datatypes.option_map f (find x m).

generalize (find_mapsto_iff (map f m) x) (find_mapsto_iff m x) (fun b => map_mapsto_iff m x b f).

destruct (find x (map f m)); destruct (find x m); simpl; auto; intros.

rewrite <- H; rewrite H1; exists e0; rewrite H0; auto.

destruct (H e) as [_ H2].

destruct H2 as (a,(_,H2)); auto.

rewrite H0 in H2; discriminate.

rewrite <- H; rewrite H1; exists e; rewrite H0; auto.

Lemma map_b : forall m x (f:elt->elt'), mem x (map f m) = mem x m.

intros; do 2 rewrite mem_find_b; rewrite map_o.

destruct (find x m); simpl; auto.

Lemma mapi_b : forall m x (f:key->elt->elt'), mem x (mapi f m) = mem x m.

generalize (mem_in_iff (mapi f m) x) (mem_in_iff m x) (mapi_in_iff m x f).

destruct (mem x (mapi f m)); destruct (mem x m); simpl; auto; intros.

symmetry; rewrite <- H0; rewrite <- H1; rewrite H; auto.

rewrite <- H; rewrite H1; rewrite H0; auto.

Lemma mapi_o : forall m x (f:key->elt->elt'), (forall x y e, E.eq x y -> f x e = f y e) -> find x (mapi f m) = Datatypes.option_map (f x) (find x m).

generalize (find_mapsto_iff (mapi f m) x) (find_mapsto_iff m x) (fun b => mapi_mapsto_iff m x b H).

destruct (find x (mapi f m)); destruct (find x m); simpl; auto; intros.

rewrite <- H0; rewrite H2; exists e0; rewrite H1; auto.

destruct (H0 e) as [_ H3].

destruct H3 as (a,(_,H3)); auto.

rewrite H1 in H3; discriminate.

rewrite <- H0; rewrite H2; exists e; rewrite H1; auto.

Lemma map2_1bis : forall (m: t elt)(m': t elt') x (f:option elt->option elt'->option elt''), f None None = None -> find x (map2 f m m') = f (find x m) (find x m').

case_eq (find x m); intros.

apply map2_1; auto with map.

left; exists e; auto with map.

case_eq (find x m'); intros.

rewrite <- H0; rewrite <- H1.

apply map2_1; auto.

right; exists e; auto with map.

case_eq (find x (map2 f m m')); intros; auto with map.

assert (In x (map2 f m m')) by (exists e; auto with map).

destruct (map2_2 H3) as [(e0,H4)|(e0,H4)].

rewrite (find_1 H4) in H0; discriminate.

rewrite (find_1 H4) in H1; discriminate.

Lemma elements_o : forall m x, find x m = findA (eqb x) (elements m).

rewrite eq_option_alt.

rewrite <- find_mapsto_iff, elements_mapsto_iff.

rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto.

Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m).

generalize (mem_in_iff m x)(elements_in_iff m x) (existsb_exists (fun p => eqb x (fst p)) (elements m)).

destruct (mem x m); destruct (existsb (fun p => eqb x (fst p)) (elements m)); auto; intros.

symmetry; rewrite H1.

destruct H0 as (H0,_).

destruct H0 as (e,He); [ intuition |].

rewrite InA_alt in He.

destruct He as ((y,e'),(Ha1,Ha2)).

compute in Ha1; destruct Ha1; subst e'.

exists (y,e); split; simpl; auto.

unfold eqb; destruct (eq_dec x y); intuition.

rewrite <- H; rewrite H0.

destruct H1 as (H1,_).

destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|].

unfold eqb in *; destruct (eq_dec x y); auto; try discriminate.

exists e; rewrite InA_alt.

exists (y,e); intuition.

Section Equalities.

Variable elt:Type.

(** Another characterisation of [Equal] *)

Lemma Equal_mapsto_iff : forall m1 m2 : t elt, Equal m1 m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2).

split; [intros Heq k e|intros Hiff].

rewrite 2 find_mapsto_iff, Heq.

rewrite eq_option_alt.

rewrite <- 2 find_mapsto_iff; auto.

(** * Relations between [Equal], [Equiv] and [Equivb]. *) (** First, [Equal] is [Equiv] with Leibniz on elements. *)

Lemma Equal_Equiv : forall (m m' : t elt), Equal m m' <-> Equiv Logic.eq m m'.

rewrite Equal_mapsto_iff.

split; intros (e,Hin); exists e; [rewrite <- H|rewrite H]; auto.

intros; apply MapsTo_fun with m k; auto; rewrite H; auto.

assert (Hin : In k m') by (rewrite <- H; exists e; auto).

destruct Hin as (e',He').

rewrite (H0 k e e'); auto.

assert (Hin : In k m) by (rewrite H; exists e; auto).

destruct Hin as (e',He').

rewrite <- (H0 k e' e); auto.

(** [Equivb] and [Equiv] and equivalent when [eq_elt] and [cmp] are related. *)

Variable eq_elt : elt->elt->Prop.

Variable cmp : elt->elt->bool.

Definition compat_cmp := forall e e', cmp e e' = true <-> eq_elt e e'.

Lemma Equiv_Equivb : compat_cmp -> forall m m', Equiv eq_elt m m' <-> Equivb cmp m m'.

unfold Equivb, Equiv, Cmp; intuition.

red in H; rewrite H; eauto.

red in H; rewrite <-H; eauto.

(** Composition of the two last results: relation between [Equal] and [Equivb]. *)

Lemma Equal_Equivb : forall cmp, (forall e e', cmp e e' = true <-> e = e') -> forall (m m':t elt), Equal m m' <-> Equivb cmp m m'.

intros; rewrite Equal_Equiv.

apply Equiv_Equivb; auto.

Lemma Equal_Equivb_eqdec : forall eq_elt_dec : (forall e e', { e = e' } + { e <> e' }), let cmp := fun e e' => if eq_elt_dec e e' then true else false in forall (m m':t elt), Equal m m' <-> Equivb cmp m m'.

intros; apply Equal_Equivb.

unfold cmp; clear cmp; intros.

destruct eq_elt_dec; now intuition.

(** * [Equal] is a setoid equality. *)

Lemma Equal_refl : forall (elt:Type)(m : t elt), Equal m m.

Lemma Equal_sym : forall (elt:Type)(m m' : t elt), Equal m m' -> Equal m' m.

unfold Equal; auto.

Lemma Equal_trans : forall (elt:Type)(m m' m'' : t elt), Equal m m' -> Equal m' m'' -> Equal m m''.

unfold Equal; congruence.

Definition Equal_ST : forall elt:Type, Equivalence (@Equal elt).

constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans].

Add Relation key E.eq reflexivity proved by E.eq_refl symmetry proved by E.eq_sym transitivity proved by E.eq_trans as KeySetoid.

Arguments Equal {elt} m m'.

Add Parametric Relation (elt : Type) : (t elt) Equal reflexivity proved by (@Equal_refl elt) symmetry proved by (@Equal_sym elt) transitivity proved by (@Equal_trans elt) as EqualSetoid.

Add Parametric Morphism elt : (@In elt) with signature E.eq ==> Equal ==> iff as In_m.

unfold Equal; intros k k' Hk m m' Hm.

rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.

Add Parametric Morphism elt : (@MapsTo elt) with signature E.eq ==> eq ==> Equal ==> iff as MapsTo_m.

unfold Equal; intros k k' Hk e m m' Hm.

rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; intuition.

Add Parametric Morphism elt : (@Empty elt) with signature Equal ==> iff as Empty_m.

unfold Empty; intros m m' Hm.

split; intros; intro.

rewrite <-Hm in H0; eapply H, H0.

rewrite Hm in H0; eapply H, H0.

Add Parametric Morphism elt : (@is_empty elt) with signature Equal ==> eq as is_empty_m.

rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.

Add Parametric Morphism elt : (@mem elt) with signature E.eq ==> Equal ==> eq as mem_m.

intros k k' Hk m m' Hm.

rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.

Add Parametric Morphism elt : (@find elt) with signature E.eq ==> Equal ==> eq as find_m.

intros k k' Hk m m' Hm.

rewrite eq_option_alt.

rewrite <- 2 find_mapsto_iff, Hk, Hm.

Add Parametric Morphism elt : (@add elt) with signature E.eq ==> eq ==> Equal ==> Equal as add_m.

intros k k' Hk e m m' Hm y.

rewrite add_o, add_o; do 2 destruct eq_dec as [|?Hnot]; auto.

elim Hnot; rewrite <-Hk; auto.

elim Hnot; rewrite Hk; auto.

Add Parametric Morphism elt : (@remove elt) with signature E.eq ==> Equal ==> Equal as remove_m.

intros k k' Hk m m' Hm y.

rewrite remove_o, remove_o; do 2 destruct eq_dec as [|?Hnot]; auto.

elim Hnot; rewrite <-Hk; auto.

elim Hnot; rewrite Hk; auto.

Add Parametric Morphism elt elt' : (@map elt elt') with signature eq ==> Equal ==> Equal as map_m.

intros f m m' Hm y.

rewrite map_o, map_o, Hm; auto.

(* Later: Add Morphism cardinal *) (* old name: *)

Notation not_find_mapsto_iff := not_find_in_iff.

(** * Same facts for self-contained weak sets and for full maps *)

Module WFacts (M:WS) := WFacts_fun M.E M.

Module Facts := WFacts.

(** * Additional Properties for weak maps Results about [fold], [elements], induction principles... *)

Module WProperties_fun (E:DecidableType)(M:WSfun E).

Module Import F:=WFacts_fun E M.

Variable elt:Type.

Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).

Lemma Add_transpose_neqkey : forall k1 k2 e1 e2 m1 m2 m3, ~ E.eq k1 k2 -> Add k1 e1 m1 m2 -> Add k2 e2 m2 m3 -> { m | Add k2 e2 m1 m /\ Add k1 e1 m m3 }.

exists (add k2 e2 m1).

unfold Add; intros.

destruct (E.eq_dec k1 y).

assert (~ E.eq k2 y).

apply E.eq_trans with (y:=y); auto.

now rewrite add_neq_o, add_eq_o, H0, add_eq_o by assumption.

destruct (E.eq_dec k2 y).

now rewrite add_eq_o, add_neq_o, add_eq_o by assumption.

now rewrite add_neq_o, H0, add_neq_o, add_neq_o, add_neq_o by assumption.

Notation eqke := (@eq_key_elt elt).

Notation eqk := (@eq_key elt).

Instance eqk_equiv : Equivalence eqk.

unfold eq_key; split; eauto.

Instance eqke_equiv : Equivalence eqke.

unfold eq_key_elt; split; repeat red; firstorder.

(** Complements about InA, NoDupA and findA *)

Lemma InA_eqke_eqk : forall k1 k2 e1 e2 l, E.eq k1 k2 -> InA eqke (k1,e1) l -> InA eqk (k2,e2) l.

intros k1 k2 e1 e2 l Hk.

rewrite 2 InA_alt.

intros ((k',e') & (Hk',He') & H); simpl in *.

exists (k',e'); split; auto.

red; simpl; eauto.

Lemma NoDupA_eqk_eqke : forall l, NoDupA eqk l -> NoDupA eqke l.

induction 1; auto.

constructor; auto.

destruct x as (k,e).

eauto using InA_eqke_eqk.

Lemma findA_rev : forall l k, NoDupA eqk l -> findA (eqb k) l = findA (eqb k) (rev l).

case_eq (findA (eqb k) l).

rewrite <- findA_NoDupA, InA_rev, findA_NoDupA by (eauto using NoDupA_rev with *); eauto.

case_eq (findA (eqb k) (rev l)); auto.

rewrite <- findA_NoDupA, InA_rev, findA_NoDupA by (eauto using NoDupA_rev with *).

intro Eq; rewrite Eq; auto.

Lemma elements_Empty : forall m:t elt, Empty m <-> elements m = nil.

assert (forall a, ~ List.In a (elements m)).

apply (H (fst a) (snd a)).

rewrite elements_mapsto_iff.

rewrite InA_alt; exists a; auto.

split; auto; split; auto.

destruct (elements m); auto.

elim (H0 p); simpl; auto.

rewrite elements_mapsto_iff in H0.

rewrite InA_alt in H0; destruct H0.

rewrite H in H0; destruct H0 as (_,H0); inversion H0.

Lemma elements_empty : elements (@empty elt) = nil.

rewrite <-elements_Empty; apply empty_1.

(** * Conversions between maps and association lists. *)

Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W := fun p => f (fst p) (snd p).

Definition of_list := List.fold_right (uncurry (@add _)) (empty elt).

Definition to_list := elements.

Lemma of_list_1 : forall l k e, NoDupA eqk l -> (MapsTo k e (of_list l) <-> InA eqke (k,e) l).

induction l as [|(k',e') l IH]; simpl; intros k e Hnodup.

rewrite empty_mapsto_iff, InA_nil; intuition.

unfold uncurry; simpl.

inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].

specialize (IH k e Hnodup'); clear Hnodup'.

rewrite add_mapsto_iff, InA_cons, <- IH.

unfold eq_key_elt at 1; simpl.

split; destruct 1 as [H|H]; try (intuition;fail).

destruct (eq_dec k k'); [left|right]; split; auto.

contradict Hnotin.

apply InA_eqke_eqk with k e; intuition.

Lemma of_list_1b : forall l k, NoDupA eqk l -> find k (of_list l) = findA (eqb k) l.

induction l as [|(k',e') l IH]; simpl; intros k Hnodup.

unfold uncurry; simpl.

inversion_clear Hnodup as [| ? ? Hnotin Hnodup'].

specialize (IH k Hnodup'); clear Hnodup'.

rewrite add_o, IH.

unfold eqb; do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto.

Lemma of_list_2 : forall l, NoDupA eqk l -> equivlistA eqke l (to_list (of_list l)).

intros l Hnodup (k,e).

rewrite <- elements_mapsto_iff, of_list_1; intuition.

Lemma of_list_3 : forall s, Equal (of_list (to_list s)) s.

rewrite of_list_1b, elements_o; auto.

apply elements_3w.

(** * Fold *) (** Alternative specification via [fold_right] *)

Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) : fold f m i = List.fold_right (uncurry f) i (rev (elements m)).

apply fold_left_rev_right.

(** ** Induction principles about fold contributed by S. Lescuyer *) (** In the following lemma, the step hypothesis is deliberately restricted to the precise map m we are considering. *)

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).

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.

assert (Hdup : NoDupA eqk 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).

rewrite elements_o, findA_rev; auto.

apply elements_3w.

intros m Hsame; simpl.

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.

destruct H as (e',He').

apply InA_eqke_eqk with k e'; auto.

rewrite <- of_list_1; auto.

rewrite Hsame, add_o, of_list_1b.

do 2 destruct eq_dec as [|?Hnot]; auto; elim Hnot; eauto.

inversion_clear Hdup; auto.

intros; eapply Hstep'; eauto.

inversion_clear Hdup; auto.

intros; apply of_list_1b.

inversion_clear Hdup; auto.

(** Same, with [empty] and [add] instead of [Empty] and [Add]. In this case, [P] must be compatible with equality of sets *)

Theorem fold_rec_bis : forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A), forall (i:A)(m:t elt), (forall m m' a, Equal m m' -> P m a -> P m' a) -> (P (empty _) i) -> (forall k e a m', MapsTo k e m -> ~In k m' -> P m' a -> P (add k e m') (f k e a)) -> P m (fold f m i).

intros A P f i m Pmorphism Pempty Pstep.

apply fold_rec; intros.

apply Pmorphism with (empty _); auto.

case_eq (find k m0); auto; intros e'; rewrite <- find_mapsto_iff.

intro H'; elim (H k e'); auto.

apply Pmorphism with (add k e m'); try intro; auto.

Lemma fold_rec_nodep : forall (A:Type)(P : A -> Type)(f : key -> elt -> A -> A)(i:A)(m:t elt), P i -> (forall k e a, MapsTo k e m -> P a -> P (f k e a)) -> P (fold f m i).

intros; apply fold_rec_bis with (P:=fun _ => P); auto.

(** [fold_rec_weak] is a weaker principle than [fold_rec_bis] : the step hypothesis must here be applicable anywhere. At the same time, it looks more like an induction principle, and hence can be easier to use. *)

Lemma fold_rec_weak : forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A)(i:A), (forall m m' a, Equal m m' -> P m a -> P m' a) -> P (empty _) i -> (forall k e a m, ~In k m -> P m a -> P (add k e m) (f k e a)) -> forall m, P m (fold f m i).

intros; apply fold_rec_bis; auto.

Lemma fold_rel : forall (A B:Type)(R : A -> B -> Type) (f : key -> elt -> A -> A)(g : key -> elt -> B -> B)(i : A)(j : B) (m : t elt), R i j -> (forall k e a b, MapsTo k e m -> R a b -> R (f k e a) (g k e b)) -> R (fold f m i) (fold g m j).

intros A B R f g i j m Rempty Rstep.

rewrite 2 fold_spec_right.

set (l:=rev (elements m)).

assert (Rstep' : forall k e a b, InA eqke (k,e) l -> R a b -> R (f k e a) (g k e b)) by (intros; apply Rstep; auto; rewrite elements_mapsto_iff, <- InA_rev; assumption).

clearbody l; clear Rstep m.

induction l; simpl; auto.

apply Rstep'; auto.

destruct a; simpl; rewrite InA_cons; left; red; auto.

(** From the induction principle on [fold], we can deduce some general induction principles on maps. *)

Lemma map_induction : forall P : t elt -> Type, (forall m, Empty m -> P m) -> (forall m m', P m -> forall x e, ~In x m -> Add x e m m' -> P m') -> forall m, P m.

apply (@fold_rec _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto.

Lemma map_induction_bis : forall P : t elt -> Type, (forall m m', Equal m m' -> P m -> P m') -> P (empty _) -> (forall x e m, ~In x m -> P m -> P (add x e m)) -> forall m, P m.

apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ _ => tt) tt m); eauto.

(** [fold] can be used to reconstruct the same initial set. *)

Lemma fold_identity : forall m : t elt, Equal (fold (@add _) m (empty _)) m.

apply fold_rec with (P:=fun m acc => Equal acc m); auto with map.

case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff.

intro; elim (Heq k' e'); auto.

intros k e a m' m'' _ _ Hadd Heq k'.

rewrite Hadd, 2 add_o, Heq; auto.

Section Fold_More.

(** ** Additional properties of fold *) (** When a function [f] is compatible and allows transpositions, we can compute [fold f] in any order. *)

Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A).

(** This is more convenient than a [compat_op eqke ...]. In fact, every [compat_op], [compat_bool], etc, should become a [Proper] someday. *)

Hypothesis Comp : Proper (E.eq==>eq==>eqA==>eqA) f.

Lemma fold_init : forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i').

apply fold_rel with (R:=eqA); auto.

Lemma fold_Empty : forall m i, Empty m -> eqA (fold f m i) i.

apply fold_rec_nodep with (P:=fun a => eqA a i).

elim (H k e); auto.

(** As noticed by P. Casteran, asking for the general [SetoidList.transpose] here is too restrictive. Think for instance of [f] being [M.add] : in general, [M.add k e (M.add k e' m)] is not equivalent to [M.add k e' (M.add k e m)]. Fortunately, we will never encounter this situation during a real [fold], since the keys received by this [fold] are unique. Hence we can ask the transposition property to hold only for non-equal keys. This idea could be push slightly further, by asking the transposition property to hold only for (non-equal) keys living in the map given to [fold]. Please contact us if you need such a version. FSets could also benefit from a restricted [transpose], but for this case the gain is unclear. *)

Definition transpose_neqkey := forall k k' e e' a, ~E.eq k k' -> eqA (f k e (f k' e' a)) (f k' e' (f k e a)).

Hypothesis Tra : transpose_neqkey.

Lemma fold_commutes : forall i m k e, ~In k m -> eqA (fold f m (f k e i)) (f k e (fold f m i)).

intros i m k e Hnotin.

apply fold_rel with (R:= fun a b => eqA a (f k e b)); auto.

transitivity (f k0 e0 (f k e b)).

contradict Hnotin; rewrite <- Hnotin; exists e0; auto.

#[local] Hint Resolve NoDupA_eqk_eqke NoDupA_rev elements_3w : map.

Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 -> eqA (fold f m1 i) (fold f m2 i).

rewrite 2 fold_spec_right.

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_equivlistA_restr with (R:=complement eqk)(eqA:=eqke).

1:auto with typeclass_instances.

2: auto with crelations.

4, 5: auto with map.

intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.

unfold complement, eq_key, eq_key_elt; repeat red.

intros (k,e) (k',e'); unfold eq_key, uncurry; simpl; auto.

rewrite <- NoDupA_altdef; auto.

rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H.

auto with crelations.

Lemma fold_Equal2 : forall m1 m2 i j, Equal m1 m2 -> eqA i j -> eqA (fold f m1 i) (fold f m2 j).

rewrite 2 fold_spec_right.

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_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke).

1:auto with typeclass_instances.

2: auto with crelations.

4, 5: auto with map.

intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto.

unfold complement, eq_key, eq_key_elt; repeat red.

intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto.

rewrite <- NoDupA_altdef; auto.

rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H.

auto with crelations.

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)).

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.

2: auto with crelations.

4, 5: auto with map.

intros (k1,e1) (k2,e2) (Hk,He) a a' Ha; unfold f'; simpl in *.

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.

rewrite InA_cons, 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff.

unfold eq_key_elt; simpl.

destruct (eq_dec k a) as [EQ|NEQ]; split; auto.

intros EQ'; inversion EQ'; auto.

intuition; subst; auto.

exists b; rewrite EQ; auto with map.

Lemma fold_add : forall m k e i, ~In k m -> eqA (fold f (add k e m) i) (f k e (fold f m i)).

apply fold_Add; try red; auto.

Lemma cardinal_fold : forall m : t elt, cardinal m = fold (fun _ _ => S) m 0.

intros; rewrite cardinal_1, fold_1.

symmetry; apply fold_left_length; auto.

Lemma cardinal_Empty : forall m : t elt, Empty m <-> cardinal m = 0.

rewrite cardinal_1, elements_Empty.

destruct (elements m); intuition; discriminate.

Lemma Equal_cardinal : forall m m' : t elt, Equal m m' -> cardinal m = cardinal m'.

intros; do 2 rewrite cardinal_fold.

apply fold_Equal with (eqA:=eq); compute; auto.

Lemma cardinal_1 : forall m : t elt, Empty m -> cardinal m = 0.

intros; rewrite <- cardinal_Empty; auto.

Lemma cardinal_2 : forall m m' x e, ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).

intros; do 2 rewrite cardinal_fold.

change S with ((fun _ _ => S) x e).

apply fold_Add with (eqA:=eq); compute; auto.

Lemma cardinal_Add_In: forall m m' x e, In x m -> Add x e m m' -> cardinal m' = cardinal m.

assert (forall k e m, MapsTo k e m -> Add k e (remove k m) m) as remove_In_Add.

destruct (F.eq_dec k y).

rewrite <-MapsTo_m; [exact H|assumption|reflexivity|reflexivity].

rewrite F.remove_neq_o by assumption.

assert (Equal (remove x m) (remove x m')).

rewrite 2!F.remove_o.

destruct (F.eq_dec x y).

rewrite F.add_neq_o by assumption.

apply Equal_cardinal in H1.

rewrite 2!cardinal_fold.

destruct H as (e' & H).

rewrite fold_Add with (eqA:=eq) (m1:=remove x m) (m2:=m) (k:=x) (e:=e'); try now (compute; auto).

rewrite fold_Add with (eqA:=eq) (m1:=remove x m') (m2:=m') (k:=x) (e:=e); try now (compute; auto).

rewrite <- 2!cardinal_fold.

apply remove_In_Add.

rewrite F.add_eq_o; reflexivity.

apply remove_In_Add.

Lemma cardinal_inv_1 : forall m : t elt, cardinal m = 0 -> Empty m.

intros; rewrite cardinal_Empty; auto.

#[local] Hint Resolve cardinal_inv_1 : map.

Lemma cardinal_inv_2 : forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.

intros; rewrite M.cardinal_1 in *.

generalize (elements_mapsto_iff m).

destruct (elements m); try discriminate.

rewrite H0; destruct p; simpl; auto.

constructor; red; auto.

Lemma cardinal_inv_2b : forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }.

generalize (@cardinal_inv_2 m); destruct cardinal.

(** * Additional notions over maps *)

Definition Disjoint (m m' : t elt) := forall k, ~(In k m /\ In k m').

Definition Partition (m m1 m2 : t elt) := Disjoint m1 m2 /\ (forall k e, MapsTo k e m <-> MapsTo k e m1 \/ MapsTo k e m2).

(** * Emulation of some functions lacking in the interface *)

Definition filter (f : key -> elt -> bool)(m : t elt) := fold (fun k e m => if f k e then add k e m else m) m (empty _).

Definition for_all (f : key -> elt -> bool)(m : t elt) := fold (fun k e b => if f k e then b else false) m true.

Definition exists_ (f : key -> elt -> bool)(m : t elt) := fold (fun k e b => if f k e then true else b) m false.

Definition partition (f : key -> elt -> bool)(m : t elt) := (filter f m, filter (fun k e => negb (f k e)) m).

(** [update] adds to [m1] all the bindings of [m2]. It can be seen as an [union] operator which gives priority to its 2nd argument in case of binding conflit. *)

Definition update (m1 m2 : t elt) := fold (@add _) m2 m1.

(** [restrict] keeps from [m1] only the bindings whose key is in [m2]. It can be seen as an [inter] operator, with priority to its 1st argument in case of binding conflit. *)

Definition restrict (m1 m2 : t elt) := filter (fun k _ => mem k m2) m1.

(** [diff] erases from [m1] all bindings whose key is in [m2]. *)

Definition diff (m1 m2 : t elt) := filter (fun k _ => negb (mem k m2)) m1.

Variable f : key -> elt -> bool.

Hypothesis Hf : Proper (E.eq==>eq==>eq) f.

Lemma filter_iff : forall m k e, MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true.

set (f':=fun k e m => if f k e then add k e m else m).

pattern m, (fold f' m (empty _)).

intros m' Hm' k e.

rewrite empty_mapsto_iff.

elim (Hm' k e); auto.

intros k e acc m1 m2 Hke Hn Hadd IH k' e'.

change (Equal m2 (add k e m1)) in Hadd; rewrite Hadd.

case_eq (f k e); intros Hfke; simpl; rewrite !add_mapsto_iff, IH; clear IH; intuition.

rewrite <- Hfke; apply Hf; auto.

destruct (eq_dec k k') as [Hk|Hk]; [left|right]; auto.

elim Hn; exists e'; rewrite Hk; auto.

assert (f k e = f k' e') by (apply Hf; auto).

Lemma for_all_iff : forall m, for_all f m = true <-> (forall k e, MapsTo k e m -> f k e = true).

set (f':=fun k e b => if f k e then b else false).

pattern m, (fold f' m true).

elim (Hm' k e); auto.

intros k e b m1 m2 _ Hn Hadd IH.

change (Equal m2 (add k e m1)) in Hadd.

case_eq (f k e); intros Hfke.

(* f k e = true *)

split; intros Hmapsto k' e' Hke'.

rewrite Hadd, add_mapsto_iff in Hke'.

destruct Hke' as [(?,?)|(?,?)]; auto.

rewrite <- Hfke; apply Hf; auto.

rewrite Hadd, add_mapsto_iff; right; split; auto.

contradict Hn; exists e'; rewrite Hn; auto.

(* f k e = false *)

split; try discriminate.

rewrite Hadd, add_mapsto_iff; auto.

Lemma exists_iff : forall m, exists_ f m = true <-> (exists p, MapsTo (fst p) (snd p) m /\ f (fst p) (snd p) = true).

set (f':=fun k e b => if f k e then true else b).

pattern m, (fold f' m false).

split; try discriminate.

intros ((k,e),(Hke,_)); simpl in *.

elim (Hm' k e); auto.

intros k e b m1 m2 _ Hn Hadd IH.

change (Equal m2 (add k e m1)) in Hadd.

case_eq (f k e); intros Hfke.

(* f k e = true *)

split; [intros _|auto].

exists (k,e); simpl; split; auto.

rewrite Hadd, add_mapsto_iff; auto.

(* f k e = false *)

split; intros ((k',e'),(Hke1,Hke2)); simpl in *.

exists (k',e'); simpl; split; auto.

rewrite Hadd, add_mapsto_iff; right; split; auto.

exists e'; rewrite Hn; auto.

rewrite Hadd, add_mapsto_iff in Hke1.

destruct Hke1 as [(?,?)|(?,?)].

assert (f k' e' = f k e) by (apply Hf; auto).

exists (k',e'); auto.

Lemma Disjoint_alt : forall m m', Disjoint m m' <-> (forall k e e', MapsTo k e m -> MapsTo k e' m' -> False).

unfold Disjoint; split.

intros H k v v' H1 H2.

apply H with k; split.

exists v; trivial.

exists v'; trivial.

intros H k ((v,Hv),(v',Hv')).

Section Partition.

Variable f : key -> elt -> bool.

Hypothesis Hf : Proper (E.eq==>eq==>eq) f.

Lemma partition_iff_1 : forall m m1 k e, m1 = fst (partition f m) -> (MapsTo k e m1 <-> MapsTo k e m /\ f k e = true).

unfold partition; simpl; intros.

apply filter_iff; auto.

Lemma partition_iff_2 : forall m m2 k e, m2 = snd (partition f m) -> (MapsTo k e m2 <-> MapsTo k e m /\ f k e = false).

unfold partition; simpl; intros.

rewrite filter_iff.

split; intros (H,H'); split; auto.

destruct (f k e); simpl in *; auto.

repeat red; intros.

Lemma partition_Partition : forall m m1 m2, partition f m = (m1,m2) -> Partition m m1 m2.

rewrite Disjoint_alt.

rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) by (rewrite H; auto).

intros (U,V) (W,Z).

rewrite <- (MapsTo_fun U W) in Z; congruence.

rewrite (@partition_iff_1 m m1), (@partition_iff_2 m m2) by (rewrite H; auto).

destruct (f k e); intuition.

Lemma Partition_In : forall m m1 m2 k, Partition m m1 m2 -> In k m -> {In k m1}+{In k m2}.

intros m m1 m2 k Hm Hk.

destruct (In_dec m1 k) as [H|H]; [left|right]; auto.

destruct Hm as (Hm,Hm').

destruct Hk as (e,He); rewrite Hm' in He; destruct He.

elim H; exists e; auto.

Lemma Disjoint_sym : forall m1 m2, Disjoint m1 m2 -> Disjoint m2 m1.

intros m1 m2 H k (H1,H2).

Lemma Partition_sym : forall m m1 m2, Partition m m1 m2 -> Partition m m2 m1.

intros m m1 m2 (H,H'); split.

apply Disjoint_sym; auto.

intros; rewrite H'; intuition.

Lemma Partition_Empty : forall m m1 m2, Partition m m1 m2 -> (Empty m <-> (Empty m1 /\ Empty m2)).

intros m m1 m2 (Hdisj,Heq).

split; intros k e Hke; elim (He k e); rewrite Heq; auto.

intros (He1,He2) k e Hke.

rewrite Heq in Hke.

elim (He1 k e); auto.

elim (He2 k e); auto.

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).

intros m m' x e Hn Hadd m1 m2 (Hdisj,Hor).

assert (Heq : Equal m (remove x m')).

change (Equal m' (add x e m)) in Hadd.

rewrite remove_o, add_o.

destruct eq_dec as [He|Hne]; auto.

rewrite <- He, <- not_find_in_iff; auto.

assert (H : MapsTo x e m').

change (Equal m' (add x e m)) in Hadd; rewrite Hadd.

apply add_1; auto.

rewrite Hor in H; destruct H.

(* first case : x in m1 *)

exists (remove x m1); left.

change (Equal m1 (add x e (remove x m1))).

rewrite add_o, remove_o.

destruct eq_dec as [He|Hne]; auto.

rewrite <- He; apply find_1; auto.

rewrite remove_in_iff in H1; destruct H1; auto.

rewrite Heq, 2 remove_mapsto_iff, Hor.

elim (Hdisj x); split; [exists e|exists e']; auto.

apply MapsTo_1 with k'; auto.

(* second case : x in m2 *)

exists (remove x m2); right.

change (Equal m2 (add x e (remove x m2))).

rewrite add_o, remove_o.

destruct eq_dec as [He|Hne]; auto.

rewrite <- He; apply find_1; auto.

rewrite remove_in_iff in H2; destruct H2; auto.

rewrite Heq, 2 remove_mapsto_iff, Hor.

elim (Hdisj x); split; [exists e'|exists e]; auto.

apply MapsTo_1 with k'; auto.

Lemma Partition_fold : forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A), Proper (E.eq==>eq==>eqA==>eqA) f -> transpose_neqkey eqA f -> forall m m1 m2 i, Partition m m1 m2 -> eqA (fold f m i) (fold f m1 (fold f m2 i)).

intros A eqA st f Comp Tra.

induction m as [m Hm|m m' IH k e Hn Hadd] using map_induction.

intros m1 m2 i Hp.

rewrite (fold_Empty (eqA:=eqA)); auto.

rewrite (Partition_Empty Hp) in Hm.

rewrite 2 (fold_Empty (eqA:=eqA)); auto.

intros m1 m2 i Hp.

destruct (Partition_Add Hn Hadd Hp) as (m3,[(Hadd',Hp')|(Hadd',Hp')]).

(* fst case: m3 is (k,e)::m1 *)

assert (~In k m3).

destruct Hn as (e',He').

destruct Hp' as (Hp1,Hp2).

rewrite Hp2; auto.

transitivity (f k e (fold f m i)).

apply fold_Add with (eqA:=eqA); auto.

transitivity (f k e (fold f m3 (fold f m2 i))).

apply fold_Add with (eqA:=eqA); auto.

symmetry; apply IH; auto.

(* snd case: m3 is (k,e)::m2 *)

assert (~In k m3).

destruct Hn as (e',He').

destruct Hp' as (Hp1,Hp2).

rewrite Hp2; auto.

assert (~In k m1).

destruct Hn as (e',He').

destruct Hp' as (Hp1,Hp2).

rewrite Hp2; auto.

transitivity (f k e (fold f m i)).

apply fold_Add with (eqA:=eqA); auto.

transitivity (f k e (fold f m1 (fold f m3 i))).

apply Comp; auto using IH.

transitivity (fold f m1 (f k e (fold f m3 i))).

apply fold_commutes with (eqA:=eqA); auto.

apply fold_init with (eqA:=eqA); auto.

apply fold_Add with (eqA:=eqA); auto.

Lemma Partition_cardinal : forall m m1 m2, Partition m m1 m2 -> cardinal m = cardinal m1 + cardinal m2.

rewrite (cardinal_fold m), (cardinal_fold m1).

set (f:=fun (_:key)(_:elt)=>S).

setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)).

rewrite <- cardinal_fold.

apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.

apply Partition_fold with (eqA:=eq); repeat red; auto.

Lemma Partition_partition : forall m m1 m2, Partition m m1 m2 -> let f := fun k (_:elt) => mem k m1 in Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)).

intros m m1 m2 Hm f.

assert (Hf : Proper (E.eq==>eq==>eq) f).

intros k k' Hk e e' _; unfold f; rewrite Hk; auto.

set (m1':= fst (partition f m)).

set (m2':= snd (partition f m)).

split; rewrite Equal_mapsto_iff; intros k e.

rewrite (@partition_iff_1 f Hf m m1') by auto.

rewrite <- mem_in_iff.

destruct Hm as (Hm,Hm').

elim (Hm k); split; auto; exists e; auto.

rewrite (@partition_iff_2 f Hf m m2') by auto.

rewrite <- not_mem_in_iff.

destruct Hm as (Hm,Hm').

elim (Hm k); split; auto; exists e; auto.

elim H1; exists e; auto.

Lemma update_mapsto_iff : forall m m' k e, MapsTo k e (update m m') <-> (MapsTo k e m' \/ (MapsTo k e m /\ ~In k m')).

pattern m', (fold (@add _) m' m).

intros m0 Hm0 k e.

assert (~In k m0) by (intros (e0,He0); apply (Hm0 k e0); auto).

elim (Hm0 k e); auto.

intros k e m0 m1 m2 _ Hn Hadd IH k' e'.

change (Equal m2 (add k e m1)) in Hadd.

rewrite Hadd, 2 add_mapsto_iff, IH, add_in_iff.

Lemma update_dec : forall m m' k e, MapsTo k e (update m m') -> { MapsTo k e m' } + { MapsTo k e m /\ ~In k m'}.

intros m m' k e H.

rewrite update_mapsto_iff in H.

destruct (In_dec m' k) as [H'|H']; [left|right]; intuition.

elim H'; exists e; auto.

Lemma update_in_iff : forall m m' k, In k (update m m') <-> In k m \/ In k m'.

intros (e,H); rewrite update_mapsto_iff in H.

destruct H; [right|left]; exists e; intuition.

destruct (In_dec m' k) as [H|H].

destruct H as (e,H).

intros _; exists e.

rewrite update_mapsto_iff; left; auto.

destruct 1 as [H'|H']; [|elim H; auto].

destruct H' as (e,H').

rewrite update_mapsto_iff; right; auto.

Lemma diff_mapsto_iff : forall m m' k e, MapsTo k e (diff m m') <-> MapsTo k e m /\ ~In k m'.

rewrite filter_iff.

rewrite mem_1 in *; auto; discriminate.

intros ? ? Hk _ _ _; rewrite Hk; auto.

Lemma diff_in_iff : forall m m' k, In k (diff m m') <-> In k m /\ ~In k m'.

intros (e,H); rewrite diff_mapsto_iff in H.

destruct H; split; auto.

intros ((e,H),H'); exists e; rewrite diff_mapsto_iff; auto.

Lemma restrict_mapsto_iff : forall m m' k e, MapsTo k e (restrict m m') <-> MapsTo k e m /\ In k m'.

rewrite filter_iff.

intros ? ? Hk _ _ _; rewrite Hk; auto.

Lemma restrict_in_iff : forall m m' k, In k (restrict m m') <-> In k m /\ In k m'.

intros (e,H); rewrite restrict_mapsto_iff in H.

destruct H; split; auto.

intros ((e,H),H'); exists e; rewrite restrict_mapsto_iff; auto.

(** specialized versions analyzing only keys (resp. elements) *)

Definition filter_dom (f : key -> bool) := filter (fun k _ => f k).

Definition filter_range (f : elt -> bool) := filter (fun _ => f).

Definition for_all_dom (f : key -> bool) := for_all (fun k _ => f k).

Definition for_all_range (f : elt -> bool) := for_all (fun _ => f).

Definition exists_dom (f : key -> bool) := exists_ (fun k _ => f k).

Definition exists_range (f : elt -> bool) := exists_ (fun _ => f).

Definition partition_dom (f : key -> bool) := partition (fun k _ => f k).

Definition partition_range (f : elt -> bool) := partition (fun _ => f).

Add Parametric Morphism elt : (@cardinal elt) with signature Equal ==> eq as cardinal_m.

intros; apply Equal_cardinal; auto.

Add Parametric Morphism elt : (@Disjoint elt) with signature Equal ==> Equal ==> iff as Disjoint_m.

intros m1 m1' Hm1 m2 m2' Hm2.

rewrite <- Hm1, <- Hm2; auto.

rewrite Hm1, Hm2; auto.

Add Parametric Morphism elt : (@Partition elt) with signature Equal ==> Equal ==> Equal ==> iff as Partition_m.

intros m1 m1' Hm1 m2 m2' Hm2 m3 m3' Hm3.

rewrite <- Hm2, <- Hm3.

split; intros (H,H'); split; auto; intros.

rewrite <- Hm1, <- Hm2, <- Hm3; auto.

rewrite Hm1, Hm2, Hm3; auto.

Add Parametric Morphism elt : (@update elt) with signature Equal ==> Equal ==> Equal as update_m.

intros m1 m1' Hm1 m2 m2' Hm2.

setoid_replace (update m1 m2) with (update m1' m2); unfold update.

apply fold_Equal with (eqA:=Equal); auto.

intros k k' Hk e e' He m m' Hm; rewrite Hk,He,Hm; red; auto.

intros k k' e e' i Hneq x.

rewrite !add_o; do 2 destruct eq_dec; auto.

apply fold_init with (eqA:=Equal); auto.

intros k k' Hk e e' He m m' Hm; rewrite Hk,He,Hm; red; auto.

Add Parametric Morphism elt : (@restrict elt) with signature Equal ==> Equal ==> Equal as restrict_m.

intros m1 m1' Hm1 m2 m2' Hm2.

setoid_replace (restrict m1 m2) with (restrict m1' m2); unfold restrict, filter.

apply fold_rel with (R:=Equal); try red; auto.

intros k e i i' H Hii' x.

pattern (mem k m2); rewrite Hm2.

(* UGLY, see with Matthieu *)

destruct mem; rewrite Hii'; auto.

apply fold_Equal with (eqA:=Equal); auto.

intros k k' Hk e e' He m m' Hm; simpl in *.

pattern (mem k m2); rewrite Hk.

destruct mem; rewrite ?Hk,?He,Hm; red; auto.

intros k k' e e' i Hneq x.

case_eq (mem k m2); case_eq (mem k' m2); intros; auto.

rewrite !add_o; do 2 destruct eq_dec; auto.

Add Parametric Morphism elt : (@diff elt) with signature Equal ==> Equal ==> Equal as diff_m.

intros m1 m1' Hm1 m2 m2' Hm2.

setoid_replace (diff m1 m2) with (diff m1' m2); unfold diff, filter.

apply fold_rel with (R:=Equal); try red; auto.

intros k e i i' H Hii' x.

pattern (mem k m2); rewrite Hm2.

destruct mem; simpl; rewrite Hii'; auto.

apply fold_Equal with (eqA:=Equal); auto.

intros k k' Hk e e' He m m' Hm; simpl in *.

pattern (mem k m2); rewrite Hk.

destruct mem; simpl; rewrite ?Hk,?He,Hm; red; auto.

intros k k' e e' i Hneq x.

case_eq (mem k m2); case_eq (mem k' m2); intros; simpl; auto.

rewrite !add_o; do 2 destruct eq_dec; auto.

End WProperties_fun.

(** * Same Properties for self-contained weak maps and for full maps *)

Module WProperties (M:WS) := WProperties_fun M.E M.

Module Properties := WProperties.

(** * Properties specific to maps with ordered keys *)

Module OrdProperties (M:S).

Module Import ME := OrderedTypeFacts M.E.

Module Import O:=KeyOrderedType M.E.

Module Import P:=Properties M.

Variable elt:Type.

Notation eqke := (@eqke elt).

Notation eqk := (@eqk elt).

Notation ltk := (@ltk elt).

Notation cardinal := (@cardinal elt).

Notation Equal := (@Equal elt).

Notation Add := (@Add elt).

Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.

Definition Below x (m:t elt) := forall y, In y m -> E.lt x y.

Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt), sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'.

apply SortA_equivlistA_eqlistA; auto with typeclass_instances.

Ltac clean_eauto := unfold O.eqke, O.ltk; simpl; intuition; eauto.

Definition gtb (p p':key*elt) := match E.compare (fst p) (fst p') with GT _ => true | _ => false end.

Definition leb p := fun p' => negb (gtb p p').

Definition elements_lt p m := List.filter (gtb p) (elements m).

Definition elements_ge p m := List.filter (leb p) (elements m).

Lemma gtb_1 : forall p p', gtb p p' = true <-> ltk p' p.

intros (x,e) (y,e'); unfold gtb, O.ltk; simpl.

destruct (E.compare x y); intuition; try discriminate; ME.order.

Lemma leb_1 : forall p p', leb p p' = true <-> ~ltk p' p.

intros (x,e) (y,e'); unfold leb, gtb, O.ltk; simpl.

destruct (E.compare x y); intuition; try discriminate; ME.order.

Lemma gtb_compat : forall p, Proper (eqke==>eq) (gtb p).

red; intros (x,e) (a,e') (b,e'') H; red in H; simpl in *; destruct H.

generalize (gtb_1 (x,e) (a,e'))(gtb_1 (x,e) (b,e'')); destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto.

unfold O.ltk in *; simpl in *; intros.

symmetry; rewrite H2.

apply ME.eq_lt with a; auto with ordered_type.

rewrite <- H1; auto.

unfold O.ltk in *; simpl in *; intros.

apply ME.eq_lt with b; auto.

rewrite <- H2; auto.

Lemma leb_compat : forall p, Proper (eqke==>eq) (leb p).

red; intros x a b H.

unfold leb; f_equal; apply gtb_compat; auto.

#[local] Hint Resolve gtb_compat leb_compat elements_3 : map.

Lemma elements_split : forall p m, elements m = elements_lt p m ++ elements_ge p m.

unfold elements_lt, elements_ge, leb; intros.

apply filter_split with (eqA:=eqk) (ltA:=ltk).

1-3: auto with typeclass_instances.

intros; destruct x; destruct y; destruct p.

rewrite gtb_1 in H; unfold O.ltk in H; simpl in *.

assert (~ltk (t1,e0) (k,e1)).

unfold gtb, O.ltk in *; simpl in *.

destruct (E.compare k t1); intuition; try discriminate; ME.order.

unfold O.ltk in *; simpl in *; ME.order.

Lemma elements_Add : forall m m' x e, ~In x m -> Add x e m m' -> eqlistA eqke (elements m') (elements_lt (x,e) m ++ (x,e):: elements_ge (x,e) m).

intros; unfold elements_lt, elements_ge.

apply sort_equivlistA_eqlistA.

apply (@SortA_app _ eqke).

auto with typeclass_instances.

apply (@filter_sort _ eqke).

1-3: auto with typeclass_instances.

constructor; auto with map.

apply (@filter_sort _ eqke).

1-3: auto with typeclass_instances.

rewrite (@InfA_alt _ eqke).

2-4: auto with typeclass_instances.

rewrite filter_InA in H1 by auto with map.

rewrite leb_1 in H2.

destruct y; unfold O.ltk in *; simpl in *.

rewrite <- elements_mapsto_iff in H1.

assert (~E.eq x t0).

exists e0; apply MapsTo_1 with t0; auto with ordered_type.

apply (@filter_sort _ eqke).

1-3: auto with typeclass_instances.

rewrite filter_InA in H1 by auto with map.

rewrite gtb_1 in H3.

destruct y; destruct x0; unfold O.ltk in *; simpl in *.

inversion_clear H2.

red in H4; simpl in *; destruct H4.

rewrite filter_InA in H4 by auto with map.

rewrite leb_1 in H4.

unfold O.ltk in *; simpl in *; ME.order.

red; intros a; destruct a.

rewrite InA_app_iff, InA_cons, 2 filter_InA, <-2 elements_mapsto_iff, leb_1, gtb_1, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by auto with map.

unfold O.eqke, O.ltk; simpl.

destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type.

elim H; exists e0; apply MapsTo_1 with t0; auto.

fold (~E.lt t0 x); auto with ordered_type.

Lemma elements_Add_Above : forall m m' x e, Above x m -> Add x e m m' -> eqlistA eqke (elements m') (elements m ++ (x,e)::nil).

apply sort_equivlistA_eqlistA.

apply (@SortA_app _ eqke).

auto with typeclass_instances.

inversion_clear H2.

destruct x0; destruct y.

rewrite <- elements_mapsto_iff in H1.

unfold O.eqke, O.ltk in *; simpl in *; destruct H3.

apply ME.lt_eq with x; auto with ordered_type.

apply H; firstorder.

red; intros a; destruct a.

rewrite InA_app_iff, InA_cons, InA_nil, <- 2 elements_mapsto_iff, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff.

unfold O.eqke; simpl.

intuition auto with relations.

destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.

generalize (H t0 H1).

Lemma elements_Add_Below : forall m m' x e, Below x m -> Add x e m m' -> eqlistA eqke (elements m') ((x,e)::elements m).

apply sort_equivlistA_eqlistA.

change (sort ltk (((x,e)::nil) ++ elements m)).

apply (@SortA_app _ eqke).

auto with typeclass_instances.

inversion_clear H1.

destruct y; destruct x0.

rewrite <- elements_mapsto_iff in H2.

unfold O.eqke, O.ltk in *; simpl in *; destruct H3.

apply ME.eq_lt with x; auto.

apply H; firstorder.

red; intros a; destruct a.

rewrite InA_cons, <- 2 elements_mapsto_iff, find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff.

unfold O.eqke; simpl.

intuition auto with relations.

destruct (E.eq_dec x t0) as [Heq|Hneq]; auto.

assert (In t0 m) by (exists e0; auto).

generalize (H t0 H1).

Lemma elements_Equal_eqlistA : forall (m m': t elt), Equal m m' -> eqlistA eqke (elements m) (elements m').

apply sort_equivlistA_eqlistA.

1-2: auto with map.

destruct x; do 2 rewrite <- elements_mapsto_iff.

do 2 rewrite find_mapsto_iff; rewrite H; split; auto.

Section Min_Max_Elt.

(** We emulate two [max_elt] and [min_elt] functions. *)

Fixpoint max_elt_aux (l:list (key*elt)) := match l with | nil => None | (x,e)::nil => Some (x,e) | (x,e)::l => max_elt_aux l end.

Definition max_elt m := max_elt_aux (elements m).

Lemma max_elt_Above : forall m x e, max_elt m = Some (x,e) -> Above x (remove x m).

rewrite remove_in_iff in H0.

rewrite elements_in_iff in H1.

unfold max_elt in *.

generalize (elements_3 m).

revert x e H y x0 H0 H1.

induction (elements m).

simpl; intros; try discriminate.

destruct a; destruct l; simpl in *.

injection H as [= -> ->].

inversion_clear H1.

red in H; simpl in *; intuition.

elim H0; eauto with ordered_type.

change (max_elt_aux (p::l) = Some (x,e)) in H.

generalize (IHl x e H); clear IHl; intros IHl.

inversion_clear H1; [ | inversion_clear H2; eauto ].

red in H3; simpl in H3; destruct H3.

destruct p as (p1,p2).

destruct (E.eq_dec p1 x) as [Heq|Hneq].

apply ME.lt_eq with p1; auto.

inversion_clear H2.

inversion_clear H5.

red in H2; simpl in H2; ME.order.

apply E.lt_trans with p1; auto.

inversion_clear H2.

inversion_clear H5.

red in H2; simpl in H2; ME.order.

eapply IHl; eauto with ordered_type.

econstructor; eauto.

red; eauto with ordered_type.

inversion H2; auto.

Lemma max_elt_MapsTo : forall m x e, max_elt m = Some (x,e) -> MapsTo x e m.

unfold max_elt in *.

rewrite elements_mapsto_iff.

induction (elements m).

simpl; try discriminate.

destruct a; destruct l; simpl in *.

injection H; intros; subst; constructor; red; auto with ordered_type.

constructor 2; auto.

Lemma max_elt_Empty : forall m, max_elt m = None -> Empty m.

unfold max_elt in *.

rewrite elements_Empty.

induction (elements m); auto.

destruct a; destruct l; simpl in *; try discriminate.

assert (H':=IHl H); discriminate.

Definition min_elt m : option (key*elt) := match elements m with | nil => None | (x,e)::_ => Some (x,e) end.

Lemma min_elt_Below : forall m x e, min_elt m = Some (x,e) -> Below x (remove x m).

unfold min_elt, Below; intros.

rewrite remove_in_iff in H0; destruct H0.

rewrite elements_in_iff in H1.

generalize (elements_3 m).

destruct (elements m).

destruct p; injection H as [= -> ->]; intros H4.

inversion_clear H1 as [? ? H2|? ? H2].

red in H2; destruct H2; simpl in *; ME.order.

inversion_clear H4.

rename H1 into H3.

rewrite (@InfA_alt _ eqke) in H3 by auto with typeclass_instances.

apply (H3 (y,x0)); auto.

Lemma min_elt_MapsTo : forall m x e, min_elt m = Some (x,e) -> MapsTo x e m.

unfold min_elt in *.

rewrite elements_mapsto_iff.

destruct (elements m).

simpl; try discriminate.

destruct p; simpl in *.

injection H; intros; subst; constructor; red; auto with ordered_type.

Lemma min_elt_Empty : forall m, min_elt m = None -> Empty m.

unfold min_elt in *.

rewrite elements_Empty.

destruct (elements m); auto.

destruct p; simpl in *; discriminate.

Section Induction_Principles.

Lemma map_induction_max : forall P : t elt -> Type, (forall m, Empty m -> P m) -> (forall m m', P m -> forall x e, Above x m -> Add x e m m' -> P m') -> forall m, P m.

intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.

apply X; apply cardinal_inv_1; auto.

case_eq (max_elt m); intros.

assert (Add k e (remove k m) m).

rewrite add_o; rewrite remove_o; destruct (eq_dec k y); eauto.

apply find_1; apply MapsTo_1 with k; auto.

apply max_elt_MapsTo; auto.

apply X0 with (remove k m) k e; auto with map.

assert (S n = S (cardinal (remove k m))).

eapply cardinal_2; eauto with map ordered_type.

inversion H1; auto.

eapply max_elt_Above; eauto.

apply X; apply max_elt_Empty; auto.

Lemma map_induction_min : forall P : t elt -> Type, (forall m, Empty m -> P m) -> (forall m m', P m -> forall x e, Below x m -> Add x e m m' -> P m') -> forall m, P m.

intros; remember (cardinal m) as n; revert m Heqn; induction n; intros.

apply X; apply cardinal_inv_1; auto.

case_eq (min_elt m); intros.

assert (Add k e (remove k m) m).

rewrite add_o; rewrite remove_o; destruct (eq_dec k y); eauto.

apply find_1; apply MapsTo_1 with k; auto.

apply min_elt_MapsTo; auto.

apply X0 with (remove k m) k e; auto.

assert (S n = S (cardinal (remove k m))).

eapply cardinal_2; eauto with map ordered_type.

inversion H1; auto.

eapply min_elt_Below; eauto.

apply X; apply min_elt_Empty; auto.

End Induction_Principles.

Section Fold_properties.

(** The following lemma has already been proved on Weak Maps, but with one additional hypothesis (some [transpose] fact). *)

Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A), Proper (E.eq==>eq==>eqA==>eqA) f -> Equal m1 m2 -> eqA (fold f m1 i) (fold f m2 i).

intros m1 m2 A eqA st f i Hf Heq.

rewrite 2 fold_spec_right.

apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.

intros (k,e) (k',e') (Hk,He) a a' Ha; simpl in *; apply Hf; auto.

apply eqlistA_rev.

apply elements_Equal_eqlistA.

Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f), Above x m1 -> Add x e m1 m2 -> eqA (fold f m2 i) (f x e (fold f m1 i)).

rewrite 2 fold_spec_right.

set (f':=uncurry f).

transitivity (fold_right f' i (rev (elements m1 ++ (x,e)::nil))).

apply fold_right_eqlistA with (eqA:=eqke) (eqB:=eqA); auto.

intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; unfold f'; simpl in *.

apply eqlistA_rev.

apply elements_Add_Above; auto.

rewrite distr_rev; simpl.

Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f), Below x m1 -> Add x e m1 m2 -> eqA (fold f m2 i) (fold f m1 (f x e i)).

Timings for FMapFacts.v