Lvc.Infra.MapSep

Require Import Util CSet InfiniteSubset InfinitePartition MapAgreement
        MapUpdate StableFresh.

Definition sep X `{OrderedType X} (p:inf_partition X) (G:set X) (ϱ:X X) :=
  ( x, x G part_1 p x part_1 p (ϱ x))
   ( x, x G part_2 p x part_2 p (ϱ x)).

Instance sep_morphism_impl X `{OrderedType X}
  : Proper (eq Equal eq impl) (sep X).
Proof.
  unfold Proper, respectful, impl. intros ? p ? x ? EQ ? ϱ ? SEP; subst.
  destruct SEP; split; intros.
  - eapply ; eauto. rewrite EQ; eauto.
  - eapply ; eauto. rewrite EQ; eauto.
Qed.


Instance sep_morphism_iff X `{OrderedType X}
  : Proper (eq Equal eq iff) (sep X).
Proof.
  unfold Proper, respectful; intros; subst.
  split; rewrite ; eauto.
Qed.


Instance sep_morphism_Subset_impl X `{OrderedType X}
  : Proper (eq Subset eq flip impl) (sep X).
Proof.
  unfold Proper, respectful, flip, impl; intros; subst.
  destruct ; split; intros; eauto.
Qed.


Instance sep_morphism_Subset_impl' X `{OrderedType X}
  : Proper (eq flip Subset eq impl) (sep X).
Proof.
  unfold Proper, respectful, flip, impl; intros; subst.
  destruct ; split; intros; eauto.
Qed.


Lemma sep_incl X `{OrderedType X} p lv lv' ϱ
  : sep X p lv ϱ
     lv' lv
     sep X p lv' ϱ.
Proof.
  intros A B. rewrite B; eauto.
Qed.


Lemma sep_agree X `{OrderedType X} p D ϱ ϱ'
  : agree_on eq D ϱ ϱ'
     sep X p D ϱ
     sep X p D ϱ'.
Proof.
  intros AGR [GT LE]; split; intros.
  - rewrite AGR; eauto.
  - rewrite AGR; eauto.
Qed.


Hint Resolve sep_incl sep_agree.

Lemma sep_filter_map_comm X `{OrderedType X} p (ϱ:X X)
      `{Proper _ (_eq _eq) ϱ} lv
  : sep X p lv ϱ
     map ϱ (filter (part_1 p) lv) [=] filter (part_1 p) (map ϱ lv).
Proof.
  intros [GT LE].
  assert (Proper (_eq eq) (part_1 p)) by eapply (part_1 p).
  cset_tac'.
  - eexists x; cset_tac'.
    pose proof (part_dich p x).
    pose proof (part_disj p (ϱ x)).
    rewrite in .
    cset_tac.
Qed.


Definition part_bounded X `{OrderedType X} (p:inf_subset X) (k:) : X Prop
  := fun acardinal (filter p a) k.

Instance filter_params
  : Params filter 1.

Instance part_bounded_impl X `{OrderedType X} p k
  : Proper (flip Subset impl) (part_bounded X p k).
Proof.
  unfold Proper, respectful, impl, flip, part_bounded; intros.
  rewrite . eauto.
Qed.


Instance part_bounded_iff X `{OrderedType X} p k
  : Proper (Equal iff) (part_bounded X p k).
Proof.
  unfold Proper, respectful, impl, flip, part_bounded; split;
  rewrite ; eauto.
Qed.


Lemma part_bounded_sep X `{OrderedType X} p ϱ
      `{Proper _ (_eq _eq) ϱ} k lv
  (BND:part_bounded X (part_1 p) k lv)
  (SEP:sep X p lv ϱ)
  : part_bounded X (part_1 p) k (lookup_set ϱ lv).
Proof.
  unfold part_bounded in ×.
  unfold lookup_set. rewrite sep_filter_map_comm; eauto.
  rewrite cardinal_map; eauto.
Qed.


Lemma sep_update_list X `{OrderedType X} p ϱ (Z:list X) (lv:set X) G
      (SEP:sep X p (lv \ of_list Z) ϱ) (incl:of_list Z [<=] lv)
  : sep X 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 . cset_tac'.
    exploit (@fresh_list_stable_get X _); try eapply ; eauto; dcr.
    subst. get_functional. eapply least_fresh_part_1; eauto.
    rewrite . 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 . cset_tac'.
    exploit (@fresh_list_stable_get X _); try eapply ; eauto; dcr.
    dcr. subst. get_functional. eapply least_fresh_part_2; eauto.
    rewrite . eauto.
    eauto with len.
  - rewrite lookup_set_update_not_in_Z; eauto.
    eapply SEP; cset_tac.
Qed.