Lvc.Alpha.RenameApart_Partition

Require Import CSet Util Map SetOperations.
Require Import Env IL Alpha Fresh Annotation OptionR.
Require Import Liveness.Liveness Coherence Restrict RenamedApart RenameApart_Liveness.
Require Import LabelsDefined PairwiseDisjoint AppExpFree.
Require Import InfinitePartition MapSep AnnP FreshGen.

Set Implicit Arguments.

Lemma bnd_update_list p ϱ k lv Z G
      (BDN:part_bounded var (part_1 p) k lv)
      (incl: of_list Z ⊆ lv)
      (SEP:sep var p (lv \ of_list Z) ϱ)
      (incl2 : map ϱ (lv \ of_list Z) ⊆ G)
      (UNIQ:NoDupA eq Z)
  : part_bounded var (part_1 p) k
                 (lookup_set ϱ (lv \ of_list Z)
                             ∪ of_list (fst (fresh_list_stable (stable_fresh_part p) G Z))).
Proof.
  unfold part_bounded, lookup_set in ×.
  rewrite filter_union; eauto.
  rewrite <- sep_filter_map_comm; eauto using sep_incl with cset.
  rewrite filter_difference; eauto.
  rewrite union_cardinal_inter.
  rewrite cardinal_filter_part; eauto.
  setoid_rewrite cardinal_1 at 3.
  - pose proof (@cardinal_map _ _ _ _
                              (filter (part_1 p) lv \ filter (part_1 p) (of_list Z)) ϱ _).
    rewrite cardinal_difference' in H.
    + assert (cardinal (filter (part_1 p) (of_list Z)) ≤ cardinal (filter (part_1 p) lv)). {
        rewrite incl; eauto.
      }
      omega.
    + rewrite incl; eauto.
  - eapply empty_is_empty_2.
    eapply disj_intersection.
    hnf; intros. eapply (@fresh_list_stable_spec var _).
    cset_tac.
    rewrite <- incl2. cset_tac.
Qed.

Lemma sep_update_list p ϱ (Z:list var) (lv:set var) G
      (ND:NoDupA eq Z) (SEP:sep nat p (lv \ of_list Z) ϱ) (incl:of_list Z [<=] lv)
  : sep nat p lv
        (ϱ [Z <-- fst (fresh_list_stable (stable_fresh_part p) G Z)]).
Proof.
  hnf; split; intros; decide (x ∈ of_list Z).
  - edestruct update_with_list_lookup_in_list; try eapply i; dcr.
    Focus 2.
    rewrite H4. cset_tac'.
    exploit (@fresh_list_stable_get var _); try eapply H3; eauto; dcr.
    subst. get_functional. eapply least_fresh_part_1; eauto.
    eauto with len.
  - rewrite lookup_set_update_not_in_Z; eauto.
    eapply SEP; cset_tac.
  - edestruct update_with_list_lookup_in_list; try eapply i; dcr.
    Focus 2.
    rewrite H4. cset_tac'.
    exploit (@fresh_list_stable_get var _); try eapply H3; eauto; dcr.
    dcr. subst. get_functional. eapply least_fresh_part_2; eauto.
    eauto with len.
  - rewrite lookup_set_update_not_in_Z; eauto.
    eapply SEP; cset_tac.
Qed.