(* iris/algebra/coPset.v *)
From stdpp Require Export sets coPset
From iris.algebra Require Export cmra
From iris.algebra Require Import updates local_updates
From iris.prelude Require Import options

Local InstancecoPset_valid_instance : Valid coPset := λ _, True.

Local InstancecoPset_unit_instance : Unit coPset := (∅ : coPset).

Local InstancecoPset_op_instance : Op coPset := union.

Local InstancecoPset_pcore_instance : PCore coPset := Some.

Lemma coPset_opX Y : X ⋅ Y = X ∪ Y.
  Proof. done. Qed.

Lemma coPset_coreX : core X = X.
  Proof. done. Qed.

Lemma coPset_includedX Y : X ≼ Y ↔ X ⊆ Y.
  Proof.
    split.
    - intros [Z ->]. rewrite coPset_op. set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
  Qed.

Lemma coPset_ra_mixin: RAMixin coPset.
  Proof.
    apply ra_total_mixin; eauto.
    - solve_proper.
    - solve_proper.
    - solve_proper.
    - intros X1 X2 X3. by rewrite !coPset_op assoc_L.
    - intros X1 X2. by rewrite !coPset_op comm_L.
    - intros X. by rewrite coPset_core idemp_L.
  Qed.
  Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.

Global InstancecoPset_cmra_discrete : CmraDiscrete coPsetR.
  Proof. apply discrete_cmra_discrete. Qed.

Lemma coPset_ucmra_mixin: UcmraMixin coPset.
  Proof. split; [done | | done]. intros X. by rewrite coPset_op left_id_L. Qed.
  Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.

Lemma coPset_opMX mY : X ⋅? mY = X ∪ default ∅ mY.
  Proof using SI. destruct mY; by rewrite /= ?right_id_L. Qed.

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

Lemma coPset_local_updateX Y X' : X ⊆ X' → (X,Y) ~l~> (X',X').
  Proof.
    intros (Z&->&?)%subseteq_disjoint_union_L.
    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
    split; first done. rewrite coPset_op. set_solver.
  Qed.

Inductive coPset_disj:=
  | CoPset : coPset → coPset_disj
  | CoPsetInvalid : coPset_disj.

Local Argumentsop _ _ !_ !_ /.
  Canonical Structure coPset_disjO := leibnizO coPset_disj.

Local InstancecoPset_disj_valid_instance : Valid coPset_disj := λ X,
    match X with CoPset _ => True | CoPsetInvalid => False end.

Local InstancecoPset_disj_unit_instance : Unit coPset_disj := CoPset ∅.

Local InstancecoPset_disj_op_instance : Op coPset_disj := λ X Y,
    match X, Y with
    | CoPset X, CoPset Y => if decide (X ## Y) then CoPset (X ∪ Y) else CoPsetInvalid
    | _, _ => CoPsetInvalid
    end.

Local InstancecoPset_disj_pcore_instance : PCore coPset_disj := λ _, Some ε.

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

Lemma coPset_disj_includedX Y : CoPset X ≼ CoPset Y ↔ X ⊆ Y.
  Proof.
    split.
    - move=> [[Z|]]; simpl; try case_decide; set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L.
      exists (CoPset Z). coPset_disj_solve.
  Qed.

Lemma coPset_disj_valid_inv_lX Y :
    ✓ (CoPset X ⋅ Y) → ∃ Y', Y = CoPset Y' ∧ X ## Y'.
  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.

Lemma coPset_disj_unionX Y : X ## Y → CoPset X ⋅ CoPset Y = CoPset (X ∪ Y).
  Proof. intros. by rewrite /= decide_True. Qed.

Lemma coPset_disj_valid_opX Y : ✓ (CoPset X ⋅ CoPset Y) ↔ X ## Y.
  Proof. simpl. case_decide; by split. Qed.

Lemma coPset_disj_ra_mixin: RAMixin coPset_disj.
  Proof.
    apply ra_total_mixin; eauto.
    - intros [?|]; destruct 1; coPset_disj_solve.
    - by constructor.
    - by destruct 1.
    - intros [X1|] [X2|] [X3|]; coPset_disj_solve.
    - intros [X1|] [X2|]; coPset_disj_solve.
    - intros [X|]; coPset_disj_solve.
    - exists (CoPset ∅); coPset_disj_solve.
    - intros [X1|] [X2|]; coPset_disj_solve.
  Qed.
  Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.

Global InstancecoPset_disj_cmra_discrete : CmraDiscrete coPset_disjR.
  Proof. apply discrete_cmra_discrete. Qed.

Lemma coPset_disj_ucmra_mixin: UcmraMixin coPset_disj.
  Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
  Canonical Structure coPset_disjUR := Ucmra coPset_disj coPset_disj_ucmra_mixin.