Library MapFacts

Require Import FMaps.

Module MyMapFacts (M : S).

Module MapFacts := Facts M.

Include MapFacts.

Section MapsTo_In.

Variable A : Type.

Lemma MapsTo_In : forall x (e : A) m,
M.MapsTo x e m ->
M.In x m.

Proof.
  intros. rewrite MapFacts.in_find_iff.
  rewrite MapFacts.find_mapsto_iff in H. congruence.
Qed.

Lemma In_MapsTo : forall x m,
M.In x m ->
exists e : A, M.MapsTo x e m.

Proof.
  intros. rewrite MapFacts.in_find_iff in H.
  case_eq (M.find x m); intros.
    exists a. rewrite MapFacts.find_mapsto_iff. assumption.
    congruence.
Qed.

Lemma Mapsto_In : forall v (m : M.t A),
M.In v m <-> exists x, M.MapsTo v x m.

Proof.
intros. rewrite in_find_iff.
case_eq (M.find v m); intros.
split; intros.
exists a. rewrite find_mapsto_iff. auto.
congruence.
split; intros.
congruence.
destruct H0. rewrite find_mapsto_iff in H0. congruence.
Qed.

End MapsTo_In.

Section Submap.

Variable A : Type.

Definition SubMap m1 m2 := forall k (v : A),
M.find k m1 = Some v -> M.find k m2 = Some v.

End Submap.

Section general_associative_fold.

Variable A B : Type.
Variable eqA : A -> A -> Prop.
Variables eqB : B -> B -> Prop.
Hypothesis eqA_refl : forall a, eqA a a.
Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.

Lemma fold_left_compat : forall f l e e',
eqA e e' ->
(forall (e1 e2: A) (a : B), eqA e1 e2 -> eqA (f e1 a) (f e2 a)) ->
eqA (fold_left f l e) (fold_left f l e').

Proof.
  intro f;induction l;simpl.
    auto.
    intros e e' H H0.
    apply (IHl (f e a) (f e' a)).
      apply H0;assumption.
      assumption.
Qed.

Lemma fold_left_assoc : forall f,
(forall (y z : B) (s : A), eqA (f (f s y) z) (f (f s z) y)) ->
(forall (e1 e2 : A) (a : B), eqA e1 e2 -> eqA (f e1 a) (f e2 a)) ->
(forall l x a, eqA (fold_left f (a :: l) x) (f (fold_left f l x) a)).

Proof.
  induction l; intros.
  simpl. apply eqA_refl.
  simpl. simpl in IHl.
    assert (eqA (f (f x a0) a) (f (f x a) a0)).
    apply H. eapply eqA_trans. apply (fold_left_compat _ _ _ _ H1).
  auto.
  apply IHl.
Qed.

Lemma fold_left_assoc_map_find_nodup : forall l f x h,
NoDupA eqB (h :: l) ->
(forall (y z : B) s, ~eqB y z -> eqA (f (f s y) z) (f (f s z) y)) ->
(forall (e1 e2 : A) a, eqA e1 e2 -> eqA (f e1 a) (f e2 a)) ->
eqA (fold_left f (h :: l) x) (f (fold_left f l x) h).

Proof.
  induction l; simpl; intros.
  auto.
  apply eqA_trans with (y := fold_left f (h :: l) (f x a)). simpl.
    apply (fold_left_compat f l (f (f x h) a) (f (f x a) h)). apply H0.
      intro. inversion H; subst.
      elim H5. left. auto.
      assumption.
    apply IHl.
      constructor. inversion H; subst. intro. elim H4. right. auto.
      inversion H; subst. inversion H5; subst. auto.
      assumption.
      assumption.
Qed.

End general_associative_fold.

Section associative_fold_maps.

Variable A B : Type.
Variable eqA : A -> A -> Prop.
Hypothesis eqA_refl : forall a, eqA a a.
Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.


Inductive eq_map_option : option A -> option A -> Prop :=
|None_eq : eq_map_option None None
|Some_eq : forall m m', eqA m m' -> eq_map_option (Some m) (Some m').

Definition EqualMap m1 m2 := forall x, eq_map_option (M.find x m1) (M.find x m2).

Lemma EqualMap_refl : forall m, EqualMap m m.

Proof.
  unfold EqualMap. intros m x.
  destruct (M.find x m).
    constructor. apply eqA_refl.
    constructor.
Qed.

Lemma EqualMap_trans : forall m1 m2 m3,
EqualMap m1 m2 ->
EqualMap m2 m3 ->
EqualMap m1 m3.

Proof.
intros m1 m2 m3 H H0. unfold EqualMap in *.
intro x.
generalize (H x). clear H. intro H.
generalize (H0 x). clear H0. intro H0.
destruct (M.find x m1).
  inversion H. subst.
  rewrite <-H2 in H0.
  destruct (M.find x m3).
    constructor. inversion H0. subst.
    eapply eqA_trans; eauto.
    inversion H0.
  destruct (M.find x m3).
    inversion H0. inversion H. subst. rewrite <-H4 in H1. inversion H1.
    constructor.
Qed.

Lemma add_add_Eq : forall x y (fx fy : A) m,
~M.E.eq x y ->
M.Equal (M.add x fx (M.add y fy m))
             (M.add y fy (M.add x fx m)).

Proof.
  unfold M.Equal; intros.
  destruct (M.E.eq_dec y0 x).
    rewrite MapFacts.add_eq_o.
      rewrite MapFacts.add_neq_o.
        rewrite MapFacts.add_eq_o. reflexivity.
        auto.
      intro. elim H. rewrite <-e. auto.
    auto.
    rewrite MapFacts.add_neq_o.
      destruct (M.E.eq_dec y0 y).
        rewrite MapFacts.add_eq_o.
          rewrite MapFacts.add_eq_o. reflexivity.
          auto.
        auto.
      repeat (try rewrite MapFacts.add_neq_o; auto).
    auto.
Qed.

Lemma fold_left_assoc_map : forall l (f : M.t A -> B -> M.t A) x h,
(forall (y z : B) s, EqualMap (f (f s y) z) (f (f s z) y)) ->
(forall e1 e2 a, EqualMap e1 e2 -> EqualMap (f e1 a) (f e2 a)) ->
EqualMap (fold_left f (h :: l) x) (f (fold_left f l x) h).

Proof.
  intros. apply fold_left_assoc.
    exact EqualMap_refl.
    exact EqualMap_trans.
    assumption.
    assumption.
Qed.


Lemma fold_invariant : forall (f : A -> B -> A) l a P,
P a ->
(forall x t, In x l -> P t -> P (f t x)) ->
P (fold_left f l a).

Proof.
  induction l; intros.
    simpl. auto.
    simpl. apply IHl.
      apply X0.
        left. auto.
        auto.
    intros. apply X0.
      right. auto.
      auto.
Qed.

Lemma fold_invariant2 : forall (f : A -> B -> A) l a P P',
(P' a -> P a) ->
(forall x t, In x l -> (P' t -> P t) -> P (f t x)) ->
P' (fold_left f l a) -> P (fold_left f l a).

Proof.
  induction l; intros.
    simpl. auto.
    simpl. apply IHl with (P' := P').
      intros. apply X0.
        left. auto.
        auto.
    intros. apply X0.
      right. auto.
      auto. auto.
Qed.

Lemma fold_invariant_cons : forall (f : A -> B -> A) x l a P,
P (f a x) ->
(forall x t, In x l -> P t -> P (f t x)) ->
P (fold_left f (x :: l) a).

Proof.
  intros. simpl. apply fold_invariant; auto.
Qed.

End associative_fold_maps.

End MyMapFacts.