Lvc.Constr.MapBasics

Require Export Setoid Coq.Classes.Morphisms.
Require Import EqDec Computable Util AutoIndTac.
Require Export CSet Containers.SetDecide.

Set Implicit Arguments.

Section feq.
  Variable X : Type.
  Variable Y : Type.
  Variable R : relation Y.

  Definition feq (f g:XY)
    := x, R (f x) (g x).

  Global Instance feq_reflexive `{Reflexive _ R}
  : Reflexive feq.
  hnf; intros. hnf; intros. reflexivity.
  Qed.

  Global Instance feq_symmetric `{Symmetric _ R}
  : Symmetric feq.
  hnf; intros. hnf; intros. symmetry. eapply H0; eauto.
  Qed.

  Global Instance feq_transitive `{Transitive Y R}
  : Transitive feq.
  hnf; intros. hnf; intros. transitivity (y x0); eauto.
  Qed.

  Global Instance feq_equivalence `{Equivalence Y R}
  : Equivalence feq.
  constructor; eauto using feq_reflexive, feq_symmetric, feq_transitive.
  Qed.

  Definition fpeq `{OrderedType X} `{OrderedType Y} (f g:XY)
    := feq f g Proper (_eq ==> _eq) f Proper (_eq ==> _eq) g.


End feq.

Arguments feq {X} {Y} {R} f g.

Notation "f ≡ g" := (@feq _ _ eq f g) (no associativity, at level 70) : fmap_scope.

Lemma equiv_nequiv_combine W `{OrderedType W} (x y z:W)
  : x === yy =/= zx =/= z.
Proof.
  intros. intro. eapply H1. transitivity x. symmetry; assumption. assumption.
Qed.

Ltac eqs :=
  repeat (match goal with
    | [H : ?l === ?k, : ?l =/= ?k |- _ ]
      ⇒ exfalso; eapply ; eauto
    | [H : ?l === ?k, : ?k === ?j |- _ ] ⇒
       match goal with
         | [ : l === j |- _ ] ⇒ fail 1
         | [ |- _ ] ⇒ match l with jfail 2 end
         | [ |- _ ] ⇒ assert (l === j) by (transitivity k; eauto)
       end
    | [H : ?l === ?k, : ?k =/= ?l |- _ ]
      ⇒ exfalso; eapply ; symmetry; eauto
    | [H : ?l === ?k, : ~?k === ?l |- _ ]
      ⇒ exfalso; eapply ; symmetry; eauto
    | [H : ?l === ?k, : ?k =/= ?j |- _ ]
      ⇒ match goal with
           | [ : l =/= j |- _ ] ⇒ fail 1
           | [ |- _ ] ⇒ assert (l =/= j) by (eapply equiv_nequiv_combine; eauto)
         end
    | [H : ~?l === ?k |- _ ] ⇒
      match goal with
        | [ : l =/= k |- _ ] ⇒ fail 1
        | [ |- _ ] ⇒ assert (l =/= k) by (intro; eapply H; eauto); clear H
      end
    | [H : ?l === ?k |- _ ] ⇒
      match goal with
        | [ : k === l |- _ ] ⇒ fail 1
        | [ |- _ ] ⇒ assert (k === l) by (symmetry; eauto)
      end
    | [H : ?l =/= ?k |- _ ] ⇒
      match goal with
        | [ : k =/= l |- _ ] ⇒ fail 1
        | [ |- _ ] ⇒ assert (k =/= l) by (symmetry; eauto)
      end
    | [ |- _ ] ⇒ reflexivity
    | [ |- _ ] ⇒ symmetry; eassumption
  end).


Section MapUpdate.
  Variable X Y : Type.
  Context `{OrderedType X}.

  Definition update (f:XY) (x:X) (y:Y) :=
    fun if [x === ] then y else f .

  Ltac eqdec :=
    match goal with
      | [ |- context[@decision_procedure ?P _ ] ] ⇒ decide(P); try eqs
      end.

  Lemma lookup_equiv f x y
    : x === → (update f x y) === y.
  Proof.
    intros. eqs. unfold update. eqdec.
  Qed.

  Lemma lookup_nequiv f x y
    : x =/= → (update f x y) === f .
  Proof.
    intros. unfold update. eqdec.
  Qed.
End MapUpdate.

Notation "f [ w <- x ]" := (update f w x) (at level 29, left associativity) : fmap_scope.

Ltac lookup_eq_tac :=
  match goal with
    | [H : ?x === ? |- context[update ?f ?x ?y ?] ]
      ⇒ rewrite (lookup_equiv f x y H)
    | [H : ?x === ?, : context[update ?f ?x ?y ?] |- _ ]
      ⇒ rewrite (lookup_equiv f x y H) in

  end.

Ltac lookup_neq_tac :=
  match goal with
    | [H : ?x =/= ? |- context[update ?f ?x ?y ?] ]
      ⇒ rewrite (lookup_nequiv f y H)
    | [H : ?x =/= ?, : context[update ?f ?x ?y ?] |- _ ]
      ⇒ rewrite (lookup_nequiv f y H) in
  end.



Tactic Notation "simplify" "lookup'" :=
  repeat (repeat (subst || lookup_eq_tac || lookup_neq_tac); eqs).

Ltac lud :=
  repeat (simplify lookup´ || match goal with
    | [ x: _, : _ |- context[update ?f ?x ?y ?] ]
      ⇒ match goal with
          | [ : x === |- _ ] ⇒ fail 1
          | [ : ¬x === |- _ ] ⇒ fail 1
          | [ : x =/= |- _ ] ⇒ fail 1
          | [ |- _ ] ⇒ decide(x === )
          end
    | [ x: _, : _, H : context[update ?f ?x ?y ?] |- _ ]
      ⇒ match goal with
          | [ : x === |- _ ] ⇒ fail 1
          | [ : ¬x === |- _ ] ⇒ fail 1
          | [ : x =/= |- _ ] ⇒ fail 1
          | [ |- _ ] ⇒ decide(x === )
          end
  end).

Section UpdateFacts.
  Open Scope fmap_scope.

  Variable X Y : Type.
  Context `{OrderedType X}.

  Lemma update_commute (m : XY) x y :
    x =/= m[x <- y][ <- ] m[ <- ][x <- y].
  Proof.
    intros ? x´´; lud.
  Qed.

  Lemma update_shadow (m : XY) (x : X) (y : Y) :
    (m[x <- y][x <- ]) === (m[x <- ]).
  Proof.
    intro l; lud.
  Qed.

  Lemma update_repeat (m : XY) (x : X) (y : Y) :
    m x = ym[x <- y] x = y.
  Proof.
    intros; lud.
  Qed.


End UpdateFacts.