Lvc.Coherence.Restrict

Require Import CSet Util Get Drop Var Map Infra.Relations AllInRel.

Set Implicit Arguments.

Definition restr (G:set var) (o:option (set var)) :=
  match o with
    | None ⇒ None
    | Some G´ ⇒ if [G´ ⊆ G] then Some G´ else None
  end.

Lemma restr_iff G o G´
  : restr G o = Some G´ ↔ G´ ⊆ G ∧ o = Some G´.

Lemma restr_idem G o G´
  : G´ ⊆ G → restr G´ (restr G o) = restr G´ o.

Lemma restr_comm o G G´
  : restr G´ (restr G o) = restr G (restr G´ o).

Instance restr_morphism
  : Proper (Equal ==> option_eq Equal ==> option_eq Equal) restr.

Instance restr_morphism_eq
  : Proper (Equal ==> eq ==> eq) restr.

Definition restrict (DL:list (option (set var))) (G:set var)
  := List.map (restr G) DL.

Lemma restrict_idem DL G G´
  : G ⊆ G´ → restrict (restrict DL G´) G = restrict DL G.

Lemma restrict_incl G G´ DL
 : G´ ⊆ G → restrict (Some G´::DL) G = Some G´::restrict DL G.

Lemma restrict_not_incl G G´ DL
 : ¬G´ ⊆ G → restrict (Some G´::DL) G = None::restrict DL G.

Lemma restrict_comm DL G G´
: restrict (restrict DL G) G´ = restrict (restrict DL G´) G.

Instance restrict_morphism
  : Proper (PIR2 (option_eq Equal) ==>
                    Equal ==> PIR2 (option_eq Equal)) restrict.

Instance restrict_morphism_eq
  : Proper (eq ==> Equal ==> eq) restrict.

Fixpoint bounded (DL:list (option (set var))) (G:set var) :=
  match DL with
    | nil ⇒ True
    | Some G´::DL ⇒ G´ ⊆ G ∧ bounded DL G
    | None::DL ⇒ bounded DL G
  end.

Instance bounded_morphism_subset
  : Proper (eq ==> Subset ==> impl) bounded.

Instance bounded_morphism
  : Proper (eq ==> Equal ==> iff) bounded.

Lemma bounded_get DL G G´ n
  : bounded DL G → get DL n (Some G´) → G´ ⊆ G.

Lemma bounded_restrict DL G´ G
  : G´ ⊆ G → bounded (restrict DL G´) G.

Lemma bounded_restrict_eq DL G´ G
  : G ⊆ G´ → bounded DL G → restrict DL G´ = DL.

Lemma restrict_subset2 DL DL´ G G´
: PIR2 (fstNoneOrR (flip Subset)) DL DL´
  → G ⊆ G´
  → PIR2 (fstNoneOrR (flip Subset)) (restrict DL G) (restrict DL´ G´).

Lemma restrict_subset DL DL´ G G´
: PIR2 (fstNoneOrR Equal) DL DL´
  → G ⊆ G´
  → PIR2 (fstNoneOrR Equal) (restrict DL G) (restrict DL´ G´).

Lemma restr_comp_meet G o G´
  : restr G´ (restr G o) = restr (G ∩ G´) o.

Lemma restrict_comp_meet DL G G´
  : restrict (restrict DL G) G´ = restrict DL (G ∩ G´).

Definition lookup_set_option (ϱ:var→var) (x:option (set var)) : option (set var):=
  match x with
    | None ⇒ None
    | Some x ⇒ Some (lookup_set ϱ x)
  end.

Definition map_lookup (ϱ:var → var) := List.map (lookup_set_option ϱ).

Definition live_global (p:set var × list var) := Some (fst p \ of_list (snd p)).
Definition live_globals (Lv:list (set var × list var)) := List.map live_global Lv.

Lemma bounded_map_lookup G (ϱ: var → var) DL
  : bounded DL G → bounded (map_lookup ϱ DL) (lookup_set ϱ G).

Lemma restrict_incl_ext DL G G´ D
: bounded DL D
   → G ∩ D [=] G´ ∩ D
   → restrict DL G = restrict DL G´.

Lemma list_eq_special DL ϱ A B A´
: A ⊆ B
  → lookup_set ϱ A ⊆ A´
  → PIR2 (fstNoneOrR Equal)
         (map_lookup ϱ (restrict DL A))
         (restrict (map_lookup ϱ (restrict DL B)) A´).

Lemma list_eq_fstNoneOrR_incl DL ϱ A B
: A ⊆ B →
  PIR2 (fstNoneOrR Equal)
       (map_lookup ϱ (restrict DL A))
       (map_lookup ϱ (restrict DL B)).

Lemma restrict_app L L´ s
: restrict (L++L´) s = restrict L s ++ restrict L´ s.

Lemma restrict_length L s
: length (restrict L s) = length L.

Lemma bounded_app L L´ s
: bounded (L++L´) s ↔ bounded L s ∧ bounded L´ s.

Inductive fstNoneOrR´ {X Y:Type} (R:X→Y→Prop)
  : option X → Y → Prop :=
| fstNone´ (y:Y) : fstNoneOrR´ R None y
| bothR´ (x:X) (y:Y) : R x y → fstNoneOrR´ R (Some x) y
.

Definition eqReq := (fstNoneOrR´ (fun (s : set var) (t : set var × list var) ⇒
                                   s [=] fst t \ of_list (snd t))).

Lemma restrict_eqReq DL DL´ G
: PIR2 eqReq DL DL´
  → PIR2 eqReq (restrict DL G) DL´.

Lemma restrict_get DL lv n s
: get (restrict DL lv) n ⎣ s ⎦
  → get DL n (Some s) ∧ s ⊆ lv.