Library Map

Require Import Coqlib.
Require Import Coq.Logic.FunctionalExtensionality.

Hint Extern 4 (~( _ = _ )) => discriminate.

Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) =>
                  generalize X1 X2; decide equality.

Module Type MapSpec.

Parameter domain : Set.
Parameter image : Type.
Parameter beq_Domain : forall (x y : domain), {x = y} + {x <> y}.

End MapSpec.


Module MapFun(Spec : MapSpec).

Set Implicit Arguments.
Definition A : Set := Spec.domain.
Definition B := Spec.image.
Definition beq_A := Spec.beq_Domain.

Definition Map := A -> option B.

Definition emp : Map :=
  fun a : A => None.

Definition put : Map -> A -> B -> Map :=
  fun M a b =>
    fun x => if (beq_A x a) then (Some b) else M x.

Definition remove : Map -> A -> Map :=
  fun M a =>
    fun x => if (beq_A x a) then None else M x.

Definition maps_to : Map -> A -> B -> Prop :=
  fun M a b => M a = Some b.

Definition in_dom : A -> Map -> Prop :=
  fun a M => exists b : B, M a = Some b.

Definition not_in_dom : A -> Map -> Prop :=
  fun a M => M a = None.

Definition sgltonM : Map -> A -> B -> Prop :=
  fun M a b =>
    maps_to M a b /\ (forall (x : A), x <> a -> not_in_dom x M).

Definition sig : A -> B -> Map :=
  fun a b => put emp a b.

Definition sub_dom : Map -> Map -> Prop :=
  fun M M´ => forall (x : A), in_dom x M -> in_dom x M´.

Definition eqDom : Map -> Map -> Prop :=
  fun M M´ => sub_dom M M´ /\ sub_dom M´ M.

Definition merge : Map -> Map -> Map :=
  fun M1 M2 =>
    fun x =>
      match M1 x with
        None => M2 x
      | _ => M1 x
      end.

Definition disjoint : Map -> Map -> Prop :=
  fun M1 M2 =>
    forall (x : A), not_in_dom x M1 \/ not_in_dom x M2.

Definition disjUnion : Map -> Map -> Map -> Prop :=
  fun M´ M´´ M => disjoint M´ M´´ /\ (M = merge M´ M´´).

Definition disjUnion3 : Map -> Map -> Map -> Map -> Prop :=
  fun M1 M2 M3 M => exists M12, disjUnion M1 M2 M12 /\ disjUnion M12 M3 M.

Definition subseteq : Map -> Map -> Prop :=
  fun M1 M2 =>
    forall (x : A), in_dom x M1 -> M1 x = M2 x.

Definition compat : Map -> Map -> Prop :=
  fun M1 M2 =>
    forall (x : A) (y : B), maps_to M1 x y -> not_in_dom x M2 \/ maps_to M2 x y.

Lemma eq_get : forall (M M´ : Map) (x : A), M = M´ -> M x = M´ x.


Lemma put_get_eq :
  forall (M : Map) (x: A) (y : B), (put M x y) x = Some y.

Lemma put_noninterfere:
  forall (M : Map) (x x´ : A) (y : B), x <> x´ -> (put M x y) x´ = M x´.

Hint Resolve put_get_eq put_noninterfere: PMap.

Lemma put_unique :
  forall (M : Map) (x : A) (y y´ : B),
    put M x y = put M x y´
    -> y = y´.

Lemma remove_shrinks_dom:
  forall (M : Map) (x : A),
    forall (y : A), not_in_dom y M -> not_in_dom y (remove M x).

Lemma nid_remove:
  forall (M : Map) (x : A), not_in_dom x (remove M x).

Hint Resolve remove_shrinks_dom nid_remove : PMap.

Lemma remove_nothing:
  forall (M : Map) (x : A), not_in_dom x M -> M = (remove M x).

Lemma remove_cancel_put:
  forall (M : Map) (x : A) (y : B), remove (put M x y) x = remove M x.

Lemma put_cancel_remove:
  forall (M : Map) (x : A) (y : B), put (remove M x) x y = put M x y.

Lemma remove_ext_ext_remove:
  forall (M : Map) (x x´ : A) (y : B), x <> x´ -> remove (put M x y) x´ = put (remove M x´) x y.

Hint Resolve remove_nothing remove_cancel_put put_cancel_remove remove_ext_ext_remove : PMap.


Lemma in_not_notin :
  forall (x : A) (M : Map), in_dom x M -> ~ (not_in_dom x M).

Lemma notin_not_in:
  forall (x : A) (M : Map), not_in_dom x M -> ~ (in_dom x M).

Lemma not_in_notin:
  forall (x : A) (M : Map), ~ in_dom x M -> not_in_dom x M.

Lemma not_notin_in:
  forall (x : A) (M : Map), ~ not_in_dom x M -> in_dom x M.

Lemma in_or_notin:
  forall x M, in_dom x M \/ not_in_dom x M.

Hint Resolve in_not_notin notin_not_in not_in_notin not_notin_in in_or_notin : PMap.

Lemma disjoint_commut: forall M1 M2, disjoint M1 M2 -> disjoint M2 M1.

Hint Resolve disjoint_commut : PMap.

Lemma putA_presv_nidB :
  forall M x x´ y,
    not_in_dom x M -> x<>x´ -> not_in_dom x (put M x´ y).

Lemma extend_presv_disj_left:
  forall (M1 M2 : Map) (x : A) (y : B),
    disjoint M1 M2 -> not_in_dom x M2 -> disjoint (put M1 x y) M2.

Hint Resolve extend_presv_disj_left putA_presv_nidB : PMap.

Lemma extend_presv_disj_right:
  forall (M1 M2 : Map) (x : A) (y : B),
    disjoint M1 M2 -> not_in_dom x M1 -> disjoint M1 (put M2 x y).

Hint Resolve extend_presv_disj_right : PMap.

Lemma disj_exclusive_left :
  forall (x : A) (M M´ : Map),
    disjoint M M´ -> in_dom x M -> not_in_dom x M´.

Hint Resolve disj_exclusive_left : PMap.

Lemma disj_exclusive_right :
  forall (x : A) (M M´ : Map),
    disjoint M M´ -> in_dom x M´ -> not_in_dom x M.
Hint Resolve disj_exclusive_right : PMap.

Lemma update_presv_disj_left:
  forall (M1 M2 : Map) (x : A) (y : B),
    disjoint M1 M2 -> in_dom x M1 -> disjoint (put M1 x y) M2.

Hint Resolve update_presv_disj_left : PMap.

Lemma update_presv_disj_right:
  forall (M1 M2 : Map) (x : A) (y : B),
    disjoint M1 M2 -> in_dom x M2 -> disjoint M1 (put M2 x y).

Hint Resolve update_presv_disj_right : PMap.

Lemma remove_presv_disj_left:
  forall (M1 M2 : Map) (x : A),
    disjoint M1 M2 -> disjoint (remove M1 x) M2.

Hint Resolve remove_presv_disj_left : PMap.

Lemma remove_presv_disj_right:
  forall (M1 M2 : Map) (x : A),
    disjoint M1 M2 -> disjoint (remove M1 x) M2.

Hint Resolve remove_presv_disj_right : PMap.

Lemma notin_merge_distr_left :
  forall (M1 M2 : Map) (x : A),
    not_in_dom x (merge M1 M2) -> not_in_dom x M1.

Hint Resolve notin_merge_distr_left: PMap.

Lemma notin_merge_distr_right :
  forall (M1 M2 : Map) (x : A),
    not_in_dom x (merge M1 M2) -> not_in_dom x M2.
Hint Resolve notin_merge_distr_right: PMap.


Lemma merge_presv_indom_left:
  forall (M1 M2: Map) (x: A), in_dom x M1 -> in_dom x (merge M1 M2).

Lemma merge_presv_indom_right:
  forall (M1 M2: Map) (x: A), in_dom x M2 -> in_dom x (merge M1 M2).

Hint Resolve merge_presv_indom_left merge_presv_indom_right : PMap.

Lemma in_merge_left_or_right:
  forall (M1 M2: Map) (x: A), in_dom x (merge M1 M2) -> in_dom x M1 \/ in_dom x M2.

Hint Resolve in_merge_left_or_right : PMap.

Lemma in_merge_not_left_in_right:
  forall (M1 M2: Map) (x: A), in_dom x (merge M1 M2) -> not_in_dom x M1 -> in_dom x M2.
Hint Resolve in_merge_not_left_in_right: PMap.

Lemma in_merge_not_right_in_left:
  forall (M1 M2: Map) (x: A), in_dom x (merge M1 M2) -> not_in_dom x M2 -> in_dom x M1.
Hint Resolve in_merge_not_right_in_left: PMap.

Lemma in_merge_commut:
  forall (M1 M2: Map) (x: A), in_dom x (merge M1 M2) -> in_dom x (merge M2 M1).

Hint Resolve in_merge_commut : PMap.

Lemma not_in_merge_commut:
  forall (M1 M2: Map) (x: A), not_in_dom x (merge M1 M2) -> not_in_dom x (merge M2 M1).

Hint Resolve not_in_merge_commut : PMap.

Lemma notin_left_notin_right_notin_merge:
  forall (M1 M2 : Map) (x : A), not_in_dom x M1 -> not_in_dom x M2 -> not_in_dom x (merge M1 M2).

Hint Resolve notin_left_notin_right_notin_merge : PMap.
Lemma merge_extends_map:
  forall (M1 M2 : Map), subseteq M1 (merge M1 M2).

Hint Resolve merge_extends_map : PMap.

Lemma merge_assoc:
  forall M1 M2 M3, merge (merge M1 M2) M3 = merge M1 (merge M2 M3).

Hint Resolve merge_assoc : PMap.

Lemma in_left_in_merge:
  forall M1 M2 x y,
    maps_to M1 x y -> maps_to (merge M1 M2) x y.

Hint Resolve in_left_in_merge.

Lemma in_right_in_merge :
  forall M1 M2 x y,
    not_in_dom x M1 -> maps_to M2 x y -> maps_to (merge M1 M2) x y.

Hint Resolve in_right_in_merge.

Lemma put_merge_merge_put:
  forall (M1 M2 : Map) (x : A) (y : B),
    put (merge M1 M2) x y = merge (put M1 x y) M2.

Hint Resolve put_merge_merge_put : PMap.

Lemma remove_merge_merge_remove_right:
  forall (M1 M2 : Map) (x : A),
    not_in_dom x M1 -> remove (merge M1 M2) x = merge M1 (remove M2 x).

Lemma disj_remove_merge_merge_remove :
  forall (M1 M2 : Map) (x : A),
    disjoint M1 M2 -> in_dom x M1 -> remove (merge M1 M2) x = merge (remove M1 x) M2.

Hint Resolve remove_merge_merge_remove_right disj_remove_merge_merge_remove : PMap.

Lemma disj_merge_disj_left:
  forall M1 M2 M´ : Map, disjoint (merge M1 M2) M´ -> disjoint M1 M´.
Hint Resolve disj_merge_disj_left: PMap.

Lemma disj_merge_disj_right:
  forall M1 M2 M´ : Map, disjoint (merge M1 M2) M´ -> disjoint M2 M´.
Hint Resolve disj_merge_disj_right: PMap.

Lemma disj_x_merge_disj_left:
  forall M1 M2 M´ : Map, disjoint M´ (merge M1 M2) -> disjoint M´ M1.

Lemma disj_x_merge_disj_right:
  forall M1 M2 M´ : Map, disjoint M´ (merge M1 M2) -> disjoint M´ M2.

Hint Resolve disj_x_merge_disj_left disj_x_merge_disj_right: PMap.

Lemma disj_merge_commut : forall M1 M2 : Map, disjoint M1 M2 -> (merge M1 M2) = (merge M2 M1).

Hint Resolve disj_merge_commut : PMap.

Lemma disj_merge_disjUnion: forall M1 M2 : Map, disjoint M1 M2 -> disjUnion M1 M2 (merge M1 M2).

Hint Resolve disj_merge_disjUnion : PMap.
Lemma disj_merge_A:
  forall M1 M2 M3, disjoint M1 M2 -> disjoint M1 M3 -> disjoint M1 (merge M2 M3).
Hint Resolve disj_merge_A : PMap.

Lemma disj_merge_B:
  forall M1 M2 M3, disjoint M2 M1 -> disjoint M3 M1 -> disjoint (merge M2 M3) M1.

Hint Resolve disj_merge_B : PMap.

Lemma disj_merge_assoc_left_right:
  forall M1 M2 M3, disjoint M1 M2 -> disjoint (merge M1 M2) M3 -> disjoint M1 (merge M2 M3).

Lemma disj_merge_assoc_right_left:
  forall M1 M2 M3, disjoint M2 M3 -> disjoint M1 (merge M2 M3) -> disjoint (merge M1 M2) M3.

Lemma disj_merge_ABC_BAC:
  forall M1 M2 M3, disjoint M1 M2 -> merge (merge M1 M2) M3 = merge M2 (merge M1 M3).

Hint Resolve disj_merge_assoc_left_right disj_merge_assoc_right_left disj_merge_ABC_BAC : PMap.

Lemma disj_merge_ABC_CAB:
  forall (M_1 M_2 M_3 : Map),
    disjoint M_1 M_2 -> disjoint M_3 M_1 -> disjoint M_3 M_2 ->
    (merge (merge M_1 M_2) M_3) = (merge (merge M_3 M_1) M_2).

Hint Resolve disj_merge_ABC_CAB : PMap.

Lemma disj_emp : forall M, disjoint M emp.

Lemma disj_emp_B : forall M, disjoint emp M.

Lemma unit_emp_merge: forall M, merge M emp = M.

Hint Resolve disj_emp disj_emp_B unit_emp_merge : PMap.

Lemma unit_emp_merge_B : forall M, merge emp M = M.

Hint Resolve unit_emp_merge_B : PMap.

Lemma unit_emp_disjUnion: forall M, disjUnion M emp M.

Hint Resolve unit_emp_disjUnion : PMap.

Lemma emp_disjUnion_unique:
  forall M M´, disjUnion M emp M´ -> M = M´.

Hint Resolve emp_disjUnion_unique : PMap.

Lemma disjUnion_commut :
  forall M1 M2 M, disjUnion M1 M2 M -> disjUnion M2 M1 M.

Hint Resolve disjUnion_commut : PMap.

Lemma disjUnion_in_left:
  forall (M1 M2 M : Map) (x : A) (y : B),
    disjUnion M1 M2 M -> in_dom x M1 -> maps_to M x y -> maps_to M1 x y.

Lemma disjUnion_in_right:
  forall (M1 M2 M : Map) (x : A) (y : B),
    disjUnion M1 M2 M -> in_dom x M2 -> maps_to M x y -> maps_to M2 x y.

Hint Resolve disjUnion_in_left disjUnion_in_right: PMap.

Lemma disjUnion_assoc_left_right:
  forall M1 M2 M3 M, disjoint M1 M2 -> disjUnion (merge M1 M2) M3 M -> disjUnion M1 (merge M2 M3) M.

Hint Resolve disjUnion_assoc_left_right: PMap.

Lemma disjUnion_assoc_right_left:
  forall M1 M2 M3 M, disjoint M2 M3 -> disjUnion M1 (merge M2 M3) M -> disjUnion (merge M1 M2) M3 M.

Hint Resolve disjUnion_assoc_right_left: PMap.

Lemma disj_merge_unique :
  forall M1 M2 M3 M4, disjoint M1 M2 -> disjoint M3 M4 -> merge M1 M2 = merge M3 M4 -> M1 = M3 -> M2 = M4.

Hint Resolve disj_merge_unique : PMap.

Lemma disj_merge_unique_right :
  forall M1 M2 M3 M4, disjoint M1 M2 -> disjoint M3 M4 -> merge M1 M2 = merge M3 M4 -> M2 = M4 -> M1 = M3.

Lemma disjUnion_unique:
  forall M1 M2 M3 M4 M5,
    disjUnion M1 M2 M5 -> disjUnion M3 M4 M5 -> M1 = M3 -> M2 = M4.

Lemma disjUnion_equ:
   forall M1 M2 M3 M4 M5,
     disjUnion M1 M3 M4 -> disjUnion M2 M3 M5 -> M1 = M2 -> M4 = M5.

Hint Resolve disj_merge_unique_right disjUnion_unique disjUnion_equ: PMap.

Lemma disjUnion_reshuffle:
  forall M M1 M2 M1´ M2´ M11,
      disjUnion M1 M2 M -> disjUnion M1´ M2´ M -> disjUnion M11 M2´ M1
      -> disjUnion M11 M2 M1´.

Lemma eqDom_refl: forall M, eqDom M M.

Lemma eqDom_sym: forall M1 M2, eqDom M1 M2 -> eqDom M2 M1.

Lemma subDom_trans: forall M1 M2 M3, sub_dom M1 M2 -> sub_dom M2 M3 -> sub_dom M1 M3.

Lemma eqDom_trans : forall M1 M2 M3, eqDom M1 M2 -> eqDom M2 M3 -> eqDom M1 M3.

Hint Resolve eqDom_refl eqDom_sym subDom_trans eqDom_trans: PMap.

Lemma subDom_update: forall (M : Map) (x : A) (y : B), sub_dom M (put M x y).

Lemma subDom_inDom_update :
  forall (M : Map) (x : A) (y : B), in_dom x M -> sub_dom (put M x y) M.

Lemma eqDom_indom_update_eq :
  forall (M : Map) (x : A) (y : B), in_dom x M -> eqDom M (put M x y).

Hint Resolve subDom_update subDom_inDom_update eqDom_indom_update_eq : PMap.

Lemma eqDom_merge:
  forall M1 M2 M3 M4, merge M1 M2 = merge M3 M4 -> eqDom M1 M3 -> M1 = M3.

Lemma eqDom_disjUnion_left:
  forall (M1 M2 M3 M4 M : Map),
    disjUnion M1 M2 M -> disjUnion M3 M4 M -> eqDom M1 M3 -> M1 = M3.

Lemma eqDom_disjUnion_right:
  forall M1 M2 M3 M4 M,
    disjUnion M1 M2 M -> disjUnion M3 M4 M -> eqDom M1 M3 -> M2 = M4.
Hint Resolve eqDom_merge eqDom_disjUnion_left eqDom_disjUnion_right: PMap.

Lemma eqDom_notin_presv:
  forall (M1 M2 : Map) (x : A), eqDom M1 M2 -> not_in_dom x M1 -> not_in_dom x M2.

Lemma eqDom_disj_presv:
  forall (M1 M2 M : Map), eqDom M1 M2 -> disjoint M1 M -> disjoint M2 M.
Hint Resolve eqDom_notin_presv eqDom_disj_presv: PMap.

Lemma disjUnion_presv_in_dom:
  forall (M1 M2 M : Map) (x : A), in_dom x M1 -> disjUnion M1 M2 M -> in_dom x M.

Lemma disjUnion_presv_eqDom:
  forall (M1 M2 M3 M4 M M´ : Map),
    disjUnion M1 M2 M -> disjUnion M3 M4 M´ -> eqDom M1 M3 -> eqDom M2 M4 -> eqDom M M´.
Hint Resolve disjUnion_presv_in_dom disjUnion_presv_eqDom: PMap.

Lemma remove_left_presv_disjUnion_left:
  forall (M1 M2 M : Map) (x : A),
    disjUnion M1 M2 M -> in_dom x M1 -> disjUnion (remove M1 x) M2 (remove M x).

Hint Resolve remove_left_presv_disjUnion_left : PMap.

Lemma remove_left_presv_disjUnion_right:
  forall (M1 M2 M : Map) (x : A),
    disjUnion M1 M2 M -> in_dom x M2 -> disjUnion M1 (remove M2 x) (remove M x).

Hint Resolve remove_left_presv_disjUnion_right : PMap.

Lemma extend_presv_disjUnion_left:
  forall (M1 M2 M : Map) (x : A) (y : B),
    disjUnion M1 M2 M -> not_in_dom x M2 -> disjUnion (put M1 x y) M2 (put M x y).

Hint Resolve extend_presv_disjUnion_left : PMap.

Lemma extend_presv_disjUnion_right:
  forall (M1 M2 M : Map) (x : A) (y : B),
    disjUnion M1 M2 M -> not_in_dom x M1 -> disjUnion M1 (put M2 x y) (put M x y).

Hint Resolve extend_presv_disjUnion_right : PMap.

Lemma update_presv_disjUnion_left:
  forall (M1 M2 M : Map) (x : A) (y : B),
    disjUnion M1 M2 M -> in_dom x M1 -> disjUnion (put M1 x y) M2 (put M x y).

Hint Resolve update_presv_disjUnion_left : PMap.

Lemma update_presv_disjUnion_right:
  forall (M1 M2 M : Map) (x : A) (y : B),
    disjUnion M1 M2 M -> in_dom x M2 -> disjUnion M1 (put M2 x y) (put M x y).

Hint Resolve update_presv_disjUnion_right : PMap.

Lemma disjoint_merge_subseteq:
  forall M_1 M_2 M, disjoint M_1 M_2 -> subseteq M_1 M -> subseteq M_2 M -> subseteq (merge M_1 M_2) M.
Hint Resolve disjoint_merge_subseteq : PMap.

Lemma disjUnion_subseteq_left:
  forall M_1 M_2 M, disjUnion M_1 M_2 M -> subseteq M_1 M.

Lemma disjUnion_subseteq_right:
  forall M_1 M_2 M, disjUnion M_1 M_2 M -> subseteq M_2 M.

Lemma split_sglton_free:
  forall M x y, maps_to M x y -> disjUnion (put emp x y) (remove M x) M.
Hint Resolve disjUnion_subseteq_left disjUnion_subseteq_right split_sglton_free : PMap.

Lemma ext_emp_sglton:
  forall x y, sgltonM (put emp x y) x y.

Hint Resolve ext_emp_sglton.


Lemma subseteq_transitivity:
  forall M M´ M´´, subseteq M M´ -> subseteq M´ M´´ -> subseteq M M´´.

Hint Resolve subseteq_transitivity: PMap.

Lemma subset_unique_map:
  forall M M´ x y, subseteq M M´ -> maps_to M x y -> maps_to M´ x y.
Hint Resolve subset_unique_map: PMap.

Definition minus (M M´ : Map) : Map :=
  fun x =>
    match M´ x with
      None => M x
    | Some _ => None
    end.

Lemma minus_disjoint:
  forall M M´, disjoint M´ (minus M M´).
Hint Resolve minus_disjoint : PMap.

Lemma minus_disjUnion:
  forall M M´, subseteq M´ M -> disjUnion M´ (minus M M´) M.
Hint Resolve minus_disjUnion: PMap.

Lemma subseteq_split:
  forall M´ M, subseteq M´ M -> exists M´´, disjUnion M´ M´´ M.
Hint Resolve subseteq_split : PMap.

Lemma ext_in_dom:
  forall x y M, in_dom x (put M x y).

Hint Resolve ext_in_dom : PMap.

Lemma ext_mapsto:
  forall x y M, maps_to (put M x y) x y.

Hint Resolve ext_mapsto.

Lemma mapsto_indom:
  forall x y M, maps_to M x y -> in_dom x M.

Lemma ext_presv_mapsto:
  forall M x x´ y y´,
    x <> x´ -> maps_to (put M x y) x´ y´ -> maps_to M x´ y´.
Hint Resolve mapsto_indom ext_presv_mapsto: PMap.

Lemma put_xy_commut:
  forall M x x´ y y´,
    x <> x´ -> put (put M x y) x´ y´ = put (put M x´ y´) x y.

Lemma put_xx_update:
  forall M x y y´,
    put (put M x y) x y´ = put M x y´.

Hint Resolve put_xy_commut put_xx_update: PMap.

Lemma removeX_presv_Y:
  forall M x x´ y,
    x <> x´ -> maps_to M x´ y -> maps_to (remove M x) x´ y.
Hint Resolve removeX_presv_Y : PMap.


Lemma mapsto_put : forall m a b,
  maps_to (put m a b) a b.
Implicit Arguments mapsto_put [].

Lemma mapsto_put_eq : forall m a b b´,
  maps_to (put m a b) a b´
  -> b = b´.
Implicit Arguments mapsto_put_eq [m a b b´].

Lemma mapsto_put_neq : forall m a a´ b b´,
  maps_to (put m a b) a´ b´
  -> a <> a´
  -> maps_to m a´ b´.
Implicit Arguments mapsto_put_neq [m a a´ b b´].

Lemma mapsto_mapsto_put : forall m a b a´ b´,
  maps_to m a b
  -> a <> a´
  -> maps_to (put m a´ b´) a b.
Implicit Arguments mapsto_mapsto_put [m a b a´].

Lemma mapsto_subseteq_mapsto : forall m m´ a b,
  maps_to m a b
  -> subseteq m m´
  -> maps_to m´ a b.
Implicit Arguments mapsto_subseteq_mapsto [m m´ a b].

Ltac map_solve :=
  match goal with

    | H : maps_to ?m ?a ?b,
      H0 : ?a <> ?a´
      |- maps_to (put ?m ?a´ ?b´) ?a ?b =>
        apply (mapsto_mapsto_put b´ H H0)

    | H : maps_to ?m ?a ?b,
      H0 : ?a´ <> ?a
      |- maps_to (put ?m ?a´ ?b´) ?a ?b =>
        let Hn := fresh "H" in
          (assert (Hn : a <> a´);
          [auto | apply (mapsto_mapsto_put b´ H Hn)])

    | H : maps_to ?m ?a ?b,
      H0 : ?a´ <> ?a
      |- maps_to (put (remove ?m ?a´)?a´ ?b´) ?a ?b =>
        let Hn := fresh "H" in
          (assert (Hn : a <> a´);
          [auto |
            rewrite put_cancel_remove;
            apply (mapsto_mapsto_put b´ H Hn)])

    | H : maps_to ?m ?a ?b,
      H0 : ?a <> ?a´
      |- maps_to (put (remove ?m ?a´)?a´ ?b´) ?a ?b =>
          rewrite put_cancel_remove;
            apply (mapsto_mapsto_put b´ H H0)

    | H : maps_to ?m ?a ?b,
      H0 : subseteq ?m ?m´
      |- maps_to ?m´ ?a ?b =>
        apply (mapsto_subseteq_mapsto H H0)

    | H : maps_to (put ?m ?a ?b) ?a´ ?b´,
      H0 : ?a <> ?a´
      |- maps_to ?m ?a´ ?b´ =>
        apply (mapsto_put_neq H H0)

    | H : maps_to (put ?m ?a ?b) ?a´ ?b´,
      H0 : ?a´ <> ?a
      |- maps_to ?m ?a´ ?b´ =>
        let Hn := fresh "H" in
          (assert (Hn : a <> a´);
          [auto | apply (mapsto_put_neq H Hn)])

    | H : maps_to (put ?m ?a ?b) ?a ?b´
      |- ?b = ?b´ => apply (mapsto_put_eq H)
        
    | H : maps_to (put ?m ?a ?b) ?a ?b´
      |- ?b´ = ?b =>
        pose (mapsto_put_eq H); subst b´; trivial
          
    | |- maps_to (put ?m ?a ?b) ?a ?b =>
      apply (@mapsto_put m a b)

  end.

End MapFun.