Library iris.algebra.gset

From stdpp Require Export sets gmap mapset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates big_op.
From iris.prelude Require Import options.

Section gset.
  Context `{Countable K}.
  Implicit Types X Y : gset K.

  Canonical Structure gsetO := discreteO (gset K).

  Local Instance gset_valid_instance : Valid (gset K) := λ _, True.
  Local Instance gset_unit_instance : Unit (gset K) := ( : gset K).
  Local Instance gset_op_instance : Op (gset K) := union.
  Local Instance gset_pcore_instance : PCore (gset K) := λ X, Some X.

  Lemma gset_op X Y : X Y = X Y.
  Proof. done. Qed.
  Lemma gset_core X : core X = X.
  Proof. done. Qed.
  Lemma gset_included X Y : X Y X Y.
    - intros [Z ->]. rewrite gset_op. set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L. by Z.

  Lemma gset_ra_mixin : RAMixin (gset K).
    apply ra_total_mixin; apply _ || eauto; [].
    intros X. by rewrite gset_core idemp_L.
  Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.

  Global Instance gset_cmra_discrete : CmraDiscrete gsetR.
  Proof. apply discrete_cmra_discrete. Qed.

  Lemma gset_ucmra_mixin : UcmraMixin (gset K).
  Proof. split; [ done | | done ]. intros X. by rewrite gset_op left_id_L. Qed.
  Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.

  Lemma gset_opM X mY : X ⋅? mY = X default mY.
  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.

  Lemma gset_update X Y : X ~~> Y.
  Proof. done. Qed.

  Lemma gset_local_update X Y X' : X X' (X,Y) ¬l~> (X',X').
    intros (Z&->&?)%subseteq_disjoint_union_L.
    rewrite local_update_unital_discreteZ' _ /leibniz_equiv_iff→.
    split; [done|]. rewrite gset_op. set_solver.

  Global Instance gset_core_id X : CoreId X.
  Proof. by apply core_id_total; rewrite gset_core. Qed.

  Lemma big_opS_singletons X :
    ([^op set] x X, {[ x ]}) = X.
    induction X as [|x X Hx IH] using set_ind_L.
    - rewrite big_opS_empty. done.
    - unfold_leibniz. rewrite big_opS_insert // IH //.

End gset.

Global Arguments gsetO _ {_ _}.
Global Arguments gsetR _ {_ _}.
Global Arguments gsetUR _ {_ _}.

Inductive gset_disj K `{Countable K} :=
  | GSet : gset K gset_disj K
  | GSetBot : gset_disj K.
Global Arguments GSet {_ _ _} _.
Global Arguments GSetBot {_ _ _}.

Section gset_disj.
  Context `{Countable K}.
  Local Arguments op _ _ !_ !_ /.
  Local Arguments cmra_op _ !_ !_ /.
  Local Arguments ucmra_op _ !_ !_ /.

  Canonical Structure gset_disjO := leibnizO (gset_disj K).

  Local Instance gset_disj_valid_instance : Valid (gset_disj K) := λ X,
    match X with GSet _True | GSetBotFalse end.
  Local Instance gset_disj_unit_instance : Unit (gset_disj K) := GSet .
  Local Instance gset_disj_op_instance : Op (gset_disj K) := λ X Y,
    match X, Y with
    | GSet X, GSet Yif decide (X ## Y) then GSet (X Y) else GSetBot
    | _, _GSetBot
  Local Instance gset_disj_pcore_instance : PCore (gset_disj K) := λ _, Some ε.

  Ltac gset_disj_solve :=
    repeat (simpl || case_decide);
    first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto.

  Lemma gset_disj_included X Y : GSet X GSet Y X Y.
    - move⇒ [[Z|]]; simpl; try case_decide; set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L.
       (GSet Z). gset_disj_solve.
  Lemma gset_disj_valid_inv_l X Y : (GSet X Y) Y', Y = GSet Y' X ## Y'.
  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
  Lemma gset_disj_union X Y : X ## Y GSet X GSet Y = GSet (X Y).
  Proof. intros. by rewrite /= decide_True. Qed.
  Lemma gset_disj_valid_op X Y : (GSet X GSet Y) X ## Y.
  Proof. simpl. case_decide; by split. Qed.

  Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
    apply ra_total_mixin; eauto.
    - intros [?|]; destruct 1; gset_disj_solve.
    - by constructor.
    - by destruct 1.
    - intros [X1|] [X2|] [X3|]; gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
    - intros [X|]; gset_disj_solve.
    - (GSet ); gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
  Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.

  Global Instance gset_disj_cmra_discrete : CmraDiscrete gset_disjR.
  Proof. apply discrete_cmra_discrete. Qed.

  Lemma gset_disj_ucmra_mixin : UcmraMixin (gset_disj K).
  Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
  Canonical Structure gset_disjUR := Ucmra (gset_disj K) gset_disj_ucmra_mixin.

  Local Arguments op _ _ _ _ : simpl never.

  Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K Prop) X :
    ( Y, X Y j, j Y P j)
    ( i, i X P i Q (GSet ({[i]} X)))
    GSet X ~~>: Q.
    intros Hfresh HQ.
    apply cmra_discrete_updateP⇒ ? /gset_disj_valid_inv_l [Y [->?]].
    destruct (Hfresh (X Y)) as (i&?&?); first set_solver.
     (GSet ({[ i ]} X)); split.
    - apply HQ; set_solver by eauto.
    - apply gset_disj_valid_op. set_solver by eauto.
  Lemma gset_disj_alloc_updateP_strong' P X :
    ( Y, X Y j, j Y P j)
    GSet X ~~>: λ Y, i, Y = GSet ({[ i ]} X) i X P i.
  Proof. eauto using gset_disj_alloc_updateP_strong. Qed.

  Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K Prop) :
    ( Y : gset K, j, j Y P j)
    ( i, P i Q (GSet {[i]})) GSet ~~>: Q.
    intros. apply (gset_disj_alloc_updateP_strong P); eauto.
    intros i; rewrite right_id_L; auto.
  Lemma gset_disj_alloc_empty_updateP_strong' P :
    ( Y : gset K, j, j Y P j)
    GSet ~~>: λ Y, i, Y = GSet {[ i ]} P i.
  Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.

  Section fresh_updates.
    Local Set Default Proof Using "Type*".
    Context `{!Infinite K}.

    Lemma gset_disj_alloc_updateP (Q : gset_disj K Prop) X :
      ( i, i X Q (GSet ({[i]} X))) GSet X ~~>: Q.
      intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
      intros Y ?; (fresh Y). split; [|done]. apply is_fresh.
    Lemma gset_disj_alloc_updateP' X :
      GSet X ~~>: λ Y, i, Y = GSet ({[ i ]} X) i X.
    Proof. eauto using gset_disj_alloc_updateP. Qed.

    Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K Prop) :
      ( i, Q (GSet {[i]})) GSet ~~>: Q.
      intro. apply gset_disj_alloc_updateP. intros i; rewrite right_id_L; auto.
    Lemma gset_disj_alloc_empty_updateP' : GSet ~~>: λ Y, i, Y = GSet {[ i ]}.
    Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
  End fresh_updates.

  Lemma gset_disj_dealloc_local_update X Y :
    (GSet X, GSet Y) ¬l~> (GSet (X Y), GSet ).
    apply local_update_total_valid_ _ /gset_disj_included HYX.
    rewrite local_update_unital_discrete⇒ -[Xf|] _ /leibniz_equiv_iff //=.
    rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done].
    by rewrite difference_union_distr_l_L
      difference_diag_L !left_id_L difference_disjoint_L.
  Lemma gset_disj_dealloc_empty_local_update X Z :
    (GSet Z GSet X, GSet Z) ¬l~> (GSet X, GSet ).
    apply local_update_total_valid⇒ /gset_disj_valid_op HZX _ _.
    assert (X = (Z X) Z) as HX by set_solver.
    rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update.
  Lemma gset_disj_dealloc_op_local_update X Y Z :
    (GSet Z GSet X, GSet Z GSet Y) ¬l~> (GSet X,GSet Y).
    rewrite -{2}(left_id ε _ (GSet Y)).
    apply op_local_update_frame, gset_disj_dealloc_empty_local_update.

  Lemma gset_disj_alloc_op_local_update X Y Z :
    Z ## X (GSet X,GSet Y) ¬l~> (GSet Z GSet X, GSet Z GSet Y).
    intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op.
  Lemma gset_disj_alloc_local_update X Y Z :
    Z ## X (GSet X,GSet Y) ¬l~> (GSet (Z X), GSet (Z Y)).
    intros. apply local_update_total_valid_ _ /gset_disj_included ?.
    rewrite -!gset_disj_union //; last set_solver.
    auto using gset_disj_alloc_op_local_update.
  Lemma gset_disj_alloc_empty_local_update X Z :
    Z ## X (GSet X, GSet ) ¬l~> (GSet (Z X), GSet Z).
    intros. rewrite -{2}(right_id_L _ union Z).
    apply gset_disj_alloc_local_update; set_solver.
End gset_disj.

Global Arguments gset_disjO _ {_ _}.
Global Arguments gset_disjR _ {_ _}.
Global Arguments gset_disjUR _ {_ _}.