(* iris/algebra/lib/gset_bij.v *)
From iris.algebra Require Export view gset
From iris.algebra Require Import updates
From iris.prelude Require Import options

Definition gset_bijective(L : gset (A * B)) :=
    ∀ a b, (a, b) ∈ L →
    (∀ b', (a, b') ∈ L → b' = b) ∧ (∀ a', (a', b) ∈ L → a' = a).

Lemma gset_bijective_empty: gset_bijective (∅ : gset (A * B)).
  Proof. by intros ?? []%not_elem_of_empty. Qed.

Lemma gset_bijective_extendL a b :
    gset_bijective L →
    (∀ b', (a, b') ∉ L) →
    (∀ a', (a', b) ∉ L) →
    gset_bijective ({[(a, b)]} ∪ L).
  Proof. rewrite /gset_bijective. set_solver. Qed.

Lemma gset_bijective_eq_iffL (a1 a2 : A) (b1 b2 : B) :
    gset_bijective L →
    (a1, b1) ∈ L →
    (a2, b2) ∈ L →
    a1 = a2 ↔ b1 = b2.
  Proof. rewrite /gset_bijective. set_solver. Qed.

Lemma gset_bijective_paira1 b1 a2 b2 :
    gset_bijective {[(a1, b1); (a2, b2)]} →
    (a1 = a2 ↔ b1 = b2).
  Proof. rewrite /gset_bijective. set_solver. Qed.

Lemma subseteq_gset_bijectiveL L' :
    gset_bijective L →
    L' ⊆ L →
    gset_bijective L'.
  Proof. rewrite /gset_bijective. set_solver. Qed.

Local Definitiongset_bij_view_rel_raw (n : SI) bijL L: Prop :=
    L ⊆ bijL ∧ gset_bijective bijL.

Local Lemmagset_bij_view_rel_raw_mono n1 n2 bijL1 bijL2 L1 L2 :
    gset_bij_view_rel_raw n1 bijL1 L1 →
    bijL1 ≡{n2}≡ bijL2 →
    L2 ≼{n2} L1 →
    (n2 ≤ n1)%sidx →
    gset_bij_view_rel_raw n2 bijL2 L2.
  Proof.
    intros [??] <-%(discrete_iff _ _ _)%leibniz_equiv ?%gset_included _.
    split; [|done]. by trans L1.
  Qed.

Local Lemmagset_bij_view_rel_raw_valid n bijL L :
    gset_bij_view_rel_raw n bijL L → ✓{n}L.
  Proof. by intros _. Qed.

Local Lemmagset_bij_view_rel_raw_unit n :
    ∃ bijL, gset_bij_view_rel_raw n bijL ε.
  Proof. exists ∅. split; eauto using gset_bijective_empty. Qed.
  Canonical Structure gset_bij_view_rel : view_rel (gsetO (A * B)) (gsetUR (A * B)) :=
    ViewRel gset_bij_view_rel_raw gset_bij_view_rel_raw_mono
            gset_bij_view_rel_raw_valid gset_bij_view_rel_raw_unit.

Global Instancegset_bij_view_rel_discrete : ViewRelDiscrete gset_bij_view_rel.
  Proof. intros n bijL L [??]. split; auto. Qed.

Local Lemmagset_bij_view_rel_iff n bijL L :
    gset_bij_view_rel n bijL L ↔ L ⊆ bijL ∧ gset_bijective bijL.
  Proof. done. Qed.

Definition gset_bij{SI : sidx} A B `{Countable A, Countable B} :=
  view (gset_bij_view_rel_raw (A:=A) (B:=B)).

Definition gset_bijO{SI : sidx} A B `{Countable A, Countable B} : ofe :=
  viewO (gset_bij_view_rel (A:=A) (B:=B)).

Definition gset_bijR{SI : sidx} A B `{Countable A, Countable B} : cmra :=
  viewR (gset_bij_view_rel (A:=A) (B:=B)).

Definition gset_bijUR{SI : sidx} A B `{Countable A, Countable B} : ucmra :=
  viewUR (gset_bij_view_rel (A:=A) (B:=B)).

Definition gset_bij_auth{SI : sidx} `{Countable A, Countable B}
  (dq : dfrac) (L : gset (A * B)) : gset_bij A B := ●V{dq} L ⋅ ◯V L.

Definition gset_bij_elem{SI : sidx} `{Countable A, Countable B}
  (a : A) (b : B) : gset_bij A B := ◯V {[ (a, b) ]}.

Global Instancegset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
  Proof. apply _. Qed.

Lemma gset_bij_auth_dfrac_opdq1 dq2 L :
    gset_bij_auth dq1 L ⋅ gset_bij_auth dq2 L ≡ gset_bij_auth (dq1 ⋅ dq2) L.
  Proof.
    rewrite /gset_bij_auth view_auth_dfrac_op.
    rewrite (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
    by rewrite -core_id_dup (comm _ (◯V _)).
  Qed.

Lemma gset_bij_auth_dfrac_validdq L : ✓ gset_bij_auth dq L ↔ ✓ dq ∧ gset_bijective L.
  Proof.
    rewrite /gset_bij_auth view_both_dfrac_valid.
    setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. naive_solver.
  Qed.

Lemma gset_bij_auth_validL : ✓ gset_bij_auth (DfracOwn 1) L ↔ gset_bijective L.
  Proof. rewrite gset_bij_auth_dfrac_valid. naive_solver by done. Qed.

Lemma gset_bij_auth_empty_dfrac_validdq : ✓ gset_bij_auth (A:=A) (B:=B) dq ∅ ↔ ✓ dq.
  Proof.
    rewrite gset_bij_auth_dfrac_valid. naive_solver eauto using gset_bijective_empty.
  Qed.

Lemma gset_bij_auth_empty_valid: ✓ gset_bij_auth (A:=A) (B:=B) (DfracOwn 1) ∅.
  Proof. by apply gset_bij_auth_empty_dfrac_valid. Qed.

Lemma gset_bij_auth_dfrac_op_validdq1 dq2 L1 L2 :
    ✓ (gset_bij_auth dq1 L1 ⋅ gset_bij_auth dq2 L2)
    ↔ ✓ (dq1 ⋅ dq2) ∧ L1 = L2 ∧ gset_bijective L1.
  Proof.
    rewrite /gset_bij_auth (comm _ (●V{dq2} _)) -!assoc (assoc _ (◯V _)).
    rewrite -view_frag_op (comm _ (◯V _)) assoc. split.
    - move=> /cmra_valid_op_l /view_auth_dfrac_op_valid.
      setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. naive_solver.
    - intros (?&->&?). rewrite -core_id_dup -view_auth_dfrac_op.
      apply view_both_dfrac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
  Qed.

Lemma gset_bij_auth_op_validL1 L2 :
    ✓ (gset_bij_auth (DfracOwn 1) L1 ⋅ gset_bij_auth (DfracOwn 1) L2) ↔ False.
  Proof. rewrite gset_bij_auth_dfrac_op_valid. naive_solver. Qed.

Lemma bij_both_dfrac_validdq L a b :
    ✓ (gset_bij_auth dq L ⋅ gset_bij_elem a b) ↔ ✓ dq ∧ gset_bijective L ∧ (a, b) ∈ L.
  Proof.
    rewrite /gset_bij_auth /gset_bij_elem -assoc -view_frag_op view_both_dfrac_valid.
    setoid_rewrite gset_bij_view_rel_iff. pose 0ᵢ. set_solver.
  Qed.

Lemma bij_both_validL a b :
    ✓ (gset_bij_auth (DfracOwn 1) L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
  Proof. rewrite bij_both_dfrac_valid. naive_solver by done. Qed.

Lemma gset_bij_elem_agreea1 b1 a2 b2 :
    ✓ (gset_bij_elem a1 b1 ⋅ gset_bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
  Proof.
    rewrite /gset_bij_elem -view_frag_op gset_op view_frag_valid.
    setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
    pose 0ᵢ. naive_solver eauto using subseteq_gset_bijective.
  Qed.

Lemma bij_view_includeddq L a b :
    (a,b) ∈ L → gset_bij_elem a b ≼ gset_bij_auth dq L.
  Proof.
    intros. etrans; [|apply cmra_included_r].
    apply view_frag_mono, gset_included. set_solver.
  Qed.

Lemma gset_bij_auth_extend{L} a b :
    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
    gset_bij_auth (DfracOwn 1) L ~~> gset_bij_auth (DfracOwn 1) ({[(a, b)]} ∪ L).
  Proof.
    intros. apply view_update=> n bijL.
    rewrite !gset_bij_view_rel_iff gset_op.
    set_solver by eauto using gset_bijective_extend.
  Qed.