Require Import FMaps.
Require Import Common.
Require Import BoolView.

Module MyMapProps (X : FMapInterface.S).
  Include FMapFacts.Properties X.
  Include F.

  Import X.

  Lemma mapsto_in: ∀ T x (y: T) d, MapsTo x y d → In x d.
  Proof. intros. ∃ y. assumption. Qed.

  Lemma in_add_1: ∀ T x (y: T) d, In x (add x y d).
  Proof. intros. ∃ y. auto with map. Qed.

  Lemma in_add_2: ∀ T x y (z: T) d, In x d → In x (add y z d).
  Proof.
    intros. destruct (E.eq_dec y x).
     ∃ z. auto with map.
     destruct H as [w ?]. ∃ w. auto with map.
  Qed.

  Hint Resolve mapsto_in in_add_1 in_add_2 : map.

  Inductive find_spec_ind A k s : option A → Prop :=
  | find_spec_1 : ∀ x, MapsTo k x s → find_spec_ind A k s (Some x)
  | find_spec_2 : ¬In k s → find_spec_ind A k s (None).

  Lemma find_spec : ∀ A k s, find_spec_ind A k s (find k s).
  Proof.
    intros. case_eq (find k s); intros; constructor; auto with map.
    intros [x Hx]. apply find_1 in Hx. rewrite H in Hx. discriminate.
  Qed.

  Instance find_view : Type_View find := {type_view := find_spec}.

  Ltac find_analyse :=
    repeat type_view find.

  Ltac find_tac :=
     repeat (
       match goal with
         | |- ?x = ?x ⇒ reflexivity
           
         | H : @MapsTo _ ?s ?x1 ?eps, H' : @MapsTo _ ?s ?x2 ?eps |- _ ⇒
           let H'' := fresh in
             assert (H'' : x1 = x2) by (eapply MapsTo_fun; eauto); clear H'; destruct H''
         | H : @MapsTo _ ?s ?x (@add _ ?t ?y ?eps) |- _ ⇒
           revert H; map_iff; intros [[? ?] | [? ?]]
| H : @MapsTo _ ?x ?b (@map _ _ ?f ?m) |- _ ⇒
           rewrite map_mapsto_iff in H;
             destruct H as [?x [?H ?H]]
| H : ~(@In _ ?x (@map _ _ ?f ?m)) |- _ ⇒ rewrite map_in_iff in H
         | H : @In _ ?x (map ?f ?m) |- _ ⇒ rewrite map_in_iff in H
         | H : ¬ (@In _ ?k (@add _ ?k ?y ?s)) |- _ ⇒ exfalso; apply H; clear H; map_iff; firstorder
         | H : ¬ (@In _ ?k (@add _ ?k' ?y ?s)), H' : @MapsTo _ ?k ?x ?s |- _ ⇒
           exfalso; apply H; clear H; map_iff; firstorder
         | H : ¬ (@In _ ?k ?s), H' : @MapsTo _ ?k ?x ?s |- _ ⇒
           exfalso; apply H; clear H; map_iff; firstorder
         | H : ¬ (@In _ ?k (@add _ ?k' ?y ?s)) |- _ ⇒ revert H; rewrite add_in_iff; intro H
         | H : ?s = ?s |- _ ⇒ clear H
         | H : ?s ≠ ?s |- _ ⇒ elim H; reflexivity
         | H : ?s = ?t |- _ ⇒ subst
       end); trivial.

End MyMapProps.