Lvc.Constr.MapLookup

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

Set Implicit Arguments.

Section MapLookup.
  Open Scope fmap_scope.
  Variable X : Type.
  Context `{OrderedType X}.
  Variable Y : Type.


  Definition lookup_set `{OrderedType Y} (m:X → Y) (s:set X) : set Y :=
    SetConstructs.map m s.

  Lemma lookup_set_spec `{OrderedType Y} (m:X → Y) s y `{Proper _ (_eq ==> _eq) m}
  : y ∈ lookup_set m s ↔ ∃ x, x ∈ s ∧ y === m x.

  Lemma lookup_set_helper `{OrderedType Y} (m:X → Y) s x `{Proper _ (_eq ==> _eq) m}
  : x ∈ s → m x ∈ lookup_set m s.

  Lemma lookup_set_incl `{OrderedType Y} s t (m:X → Y) `{Proper _ (_eq ==> _eq) m}
  : s ⊆ t → (lookup_set m s) ⊆ (lookup_set m t).

  Lemma lookup_set_union `{OrderedType Y} s t (m:X → Y) `{Proper _ (_eq ==> _eq) m}
  : (lookup_set m (s ∪ t)) [=] (lookup_set m s ∪ lookup_set m t).

  Lemma lookup_set_minus_incl `{OrderedType Y}
        (s t:set X) (m:X → Y) `{Proper _ (_eq ==> _eq) m}
  : lookup_set m s \ (lookup_set m t) ⊆ lookup_set m (s \ t).

End MapLookup.


Lemma lookup_set_on_id {X} `{OrderedType X} (s t : set X)
  : s ⊆ t → (lookup_set (fun x ⇒ x) s) ⊆ t.

Global Instance lookup_set_morphism {X} `{OrderedType X} {Y} `{OrderedType Y} {f:X→Y}
 `{Proper _ (_eq ==> _eq) f}
  : Proper (Subset ==> Subset) (lookup_set f).

Global Instance lookup_set_morphism_eq {X} `{OrderedType X} {Y} `{OrderedType Y} {f:X→Y}
 `{Proper _ (_eq ==> _eq) f}
  : Proper (Equal ==> Equal) (lookup_set f).

Lemma lookup_set_singleton {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
  `{Proper _ (_eq ==> _eq) f} x
  : lookup_set f {{x}} [=] {{f x}}.

Lemma lookup_set_singleton´ {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
  `{Proper _ (_eq ==> _eq) f} x
  : lookup_set f (singleton x) [=] singleton (f x).

Lemma lookup_set_single X `{OrderedType X} Y `{OrderedType Y} (ϱ:X→Y)
      `{Proper _ (_eq ==> _eq) ϱ} D D´ v
: v ∈ D
  → lookup_set ϱ D ⊆ D´
  → {{ ϱ v }} ⊆ D´.

Lemma lookup_set_add X `{OrderedType X} Y `{OrderedType Y} x s (m:X → Y) `{Proper _ (_eq ==> _eq) m}
: (lookup_set m {x; s}) [=] {m x; lookup_set m s}.

Ltac set_tac :=
  repeat cset_tac;
  match goal with
    | [ H : context [ In ?y (lookup_set ?f ?s) ] |- _ ] ⇒
      rewrite (@lookup_set_spec _ _ _ _ f s y) in H
    | [ |- context [ In ?y (lookup_set ?f ?s) ]] ⇒
      rewrite (@lookup_set_spec _ _ _ _ f s y)
  end.

Lemma lookup_set_empty X `{OrderedType X} Y `{OrderedType Y} (ϱ:X→Y)
      `{Proper _ (_eq ==> _eq) ϱ}
: lookup_set ϱ {} [=] {}.

Hint Extern 20 (lookup_set ?ϱ {} [=] {}) ⇒ eapply lookup_set_empty; eauto.
Hint Extern 20 ({} [=] lookup_set ?ϱ {}) ⇒ symmetry; eapply lookup_set_empty; eauto.

Hint Extern 20 (lookup_set ?ϱ (singleton ?v) [=] singleton (?ϱ ?v)) ⇒ eapply lookup_set_singleton´; eauto.
Hint Extern 20 (singleton (?ϱ ?v) [=] lookup_set ?ϱ (singleton ?v)) ⇒ symmetry; eapply lookup_set_singleton´; eauto.