Skip to content

GitLab

Commit 170c4eb3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Consistently use name `gset_bij`.

parent cd3b7b88
Hide whitespace changes
Inline Side-by-side
_CoqProject
View file @ 170c4eb3
......@@ -50,7 +50,7 @@ iris/algebra/lib/ufrac_auth.v
iris/algebra/lib/frac_agree.v
iris/algebra/lib/gmap_view.v
iris/algebra/lib/mono_nat.v
iris/algebra/lib/bij_view.v
iris/algebra/lib/gset_bij.v
iris/si_logic/siprop.v
iris/si_logic/bi.v
iris/bi/notation.v
......@@ -100,7 +100,7 @@ iris/base_logic/lib/fancy_updates_from_vs.v
iris/base_logic/lib/proph_map.v
iris/base_logic/lib/ghost_var.v
iris/base_logic/lib/mono_nat.v
iris/base_logic/lib/bij.v
iris/base_logic/lib/gset_bij.v
iris/program_logic/adequacy.v
iris/program_logic/lifting.v
iris/program_logic/weakestpre.v
......
iris/algebra/lib/bij_view.v → iris/algebra/lib/gset_bij.v
View file @ 170c4eb3
......@@ -15,7 +15,7 @@ From iris.algebra Require Export view gset.
From iris.algebra Require Import updates.
From iris.prelude Require Import options.
Section partial_bijection.
Section gset_bijective.
Context `{Countable A, Countable B}.
Implicit Types (a : A) (b : B).
......@@ -56,139 +56,138 @@ Section partial_bijection.
L' ⊆ L →
gset_bijective L'.
Proof. rewrite /gset_bijective. set_solver. Qed.
End gset_bijective.
End partial_bijection.
Section bij.
Section gset_bij_view_rel.
Context `{Countable A, Countable B}.
Implicit Types (bijL : gset (A * B)) (L : gsetUR (A * B)).
Local Definition bij_view_rel_raw (n : nat) bijL L: Prop :=
Local Definition gset_bij_view_rel_raw (n : nat) bijL L: Prop :=
L ⊆ bijL ∧ gset_bijective bijL.
Local Lemma bij_view_rel_raw_mono n1 n2 bijL1 bijL2 L1 L2 :
bij_view_rel_raw n1 bijL1 L1 →
Local Lemma gset_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 →
bij_view_rel_raw n2 bijL2 L2.
gset_bij_view_rel_raw n2 bijL2 L2.
Proof.
intros [??] <-%(discrete_iff _ _)%leibniz_equiv ?%gset_included _.
split; [|done]. by trans L1.
Qed.
Local Lemma bij_view_rel_raw_valid n bijL L :
bij_view_rel_raw n bijL L → ✓{n}L.
Local Lemma gset_bij_view_rel_raw_valid n bijL L :
gset_bij_view_rel_raw n bijL L → ✓{n}L.
Proof. by intros _. Qed.
Local Lemma bij_view_rel_raw_unit n :
∃ bijL, bij_view_rel_raw n bijL ε.
Local Lemma gset_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 bij_view_rel : view_rel (gsetO (A * B)) (gsetUR (A * B)) :=
ViewRel bij_view_rel_raw
bij_view_rel_raw_mono bij_view_rel_raw_valid bij_view_rel_raw_unit.
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 Instance bij_view_rel_discrete : ViewRelDiscrete bij_view_rel.
Global Instance gset_bij_view_rel_discrete : ViewRelDiscrete gset_bij_view_rel.
Proof. intros n bijL L [??]. split; auto. Qed.
Local Lemma bij_view_rel_iff n bijL L :
bij_view_rel n bijL L ↔ L ⊆ bijL ∧ gset_bijective bijL.
Local Lemma gset_bij_view_rel_iff n bijL L :
gset_bij_view_rel n bijL L ↔ L ⊆ bijL ∧ gset_bijective bijL.
Proof. done. Qed.
End bij.
Definition bij_view A B `{Countable A, Countable B} :=
view (bij_view_rel_raw (A:=A) (B:=B)).
Definition bij_viewO A B `{Countable A, Countable B} : ofeT :=
viewO (bij_view_rel (A:=A) (B:=B)).
Definition bij_viewR A B `{Countable A, Countable B} : cmraT :=
viewR (bij_view_rel (A:=A) (B:=B)).
Definition bij_viewUR A B `{Countable A, Countable B} : ucmraT :=
viewUR (bij_view_rel (A:=A) (B:=B)).
Definition bij_auth `{Countable A, Countable B}
(q : Qp) (L : gset (A * B)) : bij_view A B := ●V{q} L ⋅ ◯V L.
Definition bij_elem `{Countable A, Countable B}
(a : A) (b : B) : bij_view A B := ◯V {[a, b]}.
Section bij.
End gset_bij_view_rel.
Definition gset_bij A B `{Countable A, Countable B} :=
view (gset_bij_view_rel_raw (A:=A) (B:=B)).
Definition gset_bijO A B `{Countable A, Countable B} : ofeT :=
viewO (gset_bij_view_rel (A:=A) (B:=B)).
Definition gset_bijR A B `{Countable A, Countable B} : cmraT :=
viewR (gset_bij_view_rel (A:=A) (B:=B)).
Definition gset_bijUR A B `{Countable A, Countable B} : ucmraT :=
viewUR (gset_bij_view_rel (A:=A) (B:=B)).
Definition gset_bij_auth `{Countable A, Countable B}
(q : Qp) (L : gset (A * B)) : gset_bij A B := ●V{q} L ⋅ ◯V L.
Definition gset_bij_elem `{Countable A, Countable B}
(a : A) (b : B) : gset_bij A B := ◯V {[a, b]}.
Section gset_bij.
Context `{Countable A, Countable B}.
Implicit Types (a:A) (b:B).
Implicit Types (L : gset (A*B)).
Global Instance bij_elem_core_id a b : CoreId (bij_elem a b).
Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
Proof. apply _. Qed.
Lemma bij_auth_frac_op q1 q2 L :
bij_auth q1 L ⋅ bij_auth q2 L ≡ bij_auth (q1 + q2) L.
Lemma gset_bij_auth_frac_op q1 q2 L :
gset_bij_auth q1 L ⋅ gset_bij_auth q2 L ≡ gset_bij_auth (q1 + q2) L.
Proof.
rewrite /bij_auth view_auth_frac_op.
rewrite /gset_bij_auth view_auth_frac_op.
rewrite (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
by rewrite -core_id_dup (comm _ (◯V _)).
Qed.
Lemma bij_auth_frac_valid q L : ✓ bij_auth q L ↔ ✓ q ∧ gset_bijective L.
Lemma gset_bij_auth_frac_valid q L : ✓ gset_bij_auth q L ↔ ✓ q ∧ gset_bijective L.
Proof.
rewrite /bij_auth view_both_frac_valid.
setoid_rewrite bij_view_rel_iff.
rewrite /gset_bij_auth view_both_frac_valid.
setoid_rewrite gset_bij_view_rel_iff.
naive_solver eauto using O.
Qed.
Lemma bij_auth_valid L : ✓ bij_auth 1 L ↔ gset_bijective L.
Proof. rewrite bij_auth_frac_valid. naive_solver by done. Qed.
Lemma gset_bij_auth_valid L : ✓ gset_bij_auth 1 L ↔ gset_bijective L.
Proof. rewrite gset_bij_auth_frac_valid. naive_solver by done. Qed.
Lemma bij_auth_empty_frac_valid q : ✓ bij_auth (A:=A) (B:=B) q ∅ ↔ ✓ q.
Lemma gset_bij_auth_empty_frac_valid q : ✓ gset_bij_auth (A:=A) (B:=B) q ∅ ↔ ✓ q.
Proof.
rewrite bij_auth_frac_valid. naive_solver eauto using gset_bijective_empty.
rewrite gset_bij_auth_frac_valid. naive_solver eauto using gset_bijective_empty.
Qed.
Lemma bij_auth_empty_valid : ✓ bij_auth (A:=A) (B:=B) 1 ∅.
Proof. by apply bij_auth_empty_frac_valid. Qed.
Lemma gset_bij_auth_empty_valid : ✓ gset_bij_auth (A:=A) (B:=B) 1 ∅.
Proof. by apply gset_bij_auth_empty_frac_valid. Qed.
Lemma bij_auth_frac_op_valid q1 q2 L1 L2 :
✓ (bij_auth q1 L1 ⋅ bij_auth q2 L2)
Lemma gset_bij_auth_frac_op_valid q1 q2 L1 L2 :
✓ (gset_bij_auth q1 L1 ⋅ gset_bij_auth q2 L2)
↔ ✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1.
Proof.
rewrite /bij_auth (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
rewrite /gset_bij_auth (comm _ (●V{q2} _)) -!assoc (assoc _ (◯V _)).
rewrite -view_frag_op (comm _ (◯V _)) assoc. split.
- move=> /cmra_valid_op_l /view_auth_frac_op_valid.
setoid_rewrite bij_view_rel_iff. naive_solver eauto using 0.
setoid_rewrite gset_bij_view_rel_iff. naive_solver eauto using 0.
- intros (?&->&?). rewrite -core_id_dup -view_auth_frac_op.
apply view_both_frac_valid. setoid_rewrite bij_view_rel_iff. naive_solver.
apply view_both_frac_valid. setoid_rewrite gset_bij_view_rel_iff. naive_solver.
Qed.
Lemma bij_auth_op_valid L1 L2 :
✓ (bij_auth 1 L1 ⋅ bij_auth 1 L2) ↔ False.
Proof. rewrite bij_auth_frac_op_valid. naive_solver. Qed.
Lemma gset_bij_auth_op_valid L1 L2 :
✓ (gset_bij_auth 1 L1 ⋅ gset_bij_auth 1 L2) ↔ False.
Proof. rewrite gset_bij_auth_frac_op_valid. naive_solver. Qed.
Lemma bij_both_frac_valid q L a b :
✓ (bij_auth q L ⋅ bij_elem a b) ↔ ✓ q ∧ gset_bijective L ∧ (a, b) ∈ L.
✓ (gset_bij_auth q L ⋅ gset_bij_elem a b) ↔ ✓ q ∧ gset_bijective L ∧ (a, b) ∈ L.
Proof.
rewrite /bij_auth /bij_elem -assoc -view_frag_op view_both_frac_valid.
setoid_rewrite bij_view_rel_iff.
rewrite /gset_bij_auth /gset_bij_elem -assoc -view_frag_op view_both_frac_valid.
setoid_rewrite gset_bij_view_rel_iff.
set_solver by eauto using O.
Qed.
Lemma bij_both_valid L a b :
✓ (bij_auth 1 L ⋅ bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
✓ (gset_bij_auth 1 L ⋅ gset_bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
Proof. rewrite bij_both_frac_valid. naive_solver by done. Qed.
Lemma bij_elem_agree a1 b1 a2 b2 :
✓ (bij_elem a1 b1 ⋅ bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
Lemma gset_bij_elem_agree a1 b1 a2 b2 :
✓ (gset_bij_elem a1 b1 ⋅ gset_bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
Proof.
rewrite /bij_elem -view_frag_op gset_op_union view_frag_valid.
setoid_rewrite bij_view_rel_iff. intros. apply gset_bijective_pair.
rewrite /gset_bij_elem -view_frag_op gset_op_union view_frag_valid.
setoid_rewrite gset_bij_view_rel_iff. intros. apply gset_bijective_pair.
naive_solver eauto using subseteq_gset_bijective, O.
Qed.
Lemma bij_view_included q L a b : (a,b) ∈ L → bij_elem a b ≼ bij_auth q L.
Lemma bij_view_included q L a b : (a,b) ∈ L → gset_bij_elem a b ≼ gset_bij_auth q L.
Proof.
intros. etrans; [|apply cmra_included_r].
apply view_frag_mono, gset_included. set_solver.
Qed.
Lemma bij_auth_extend L a b :
Lemma gset_bij_auth_extend L a b :
(∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
bij_auth 1 L ~~> bij_auth 1 ({[(a, b)]} ∪ L).
gset_bij_auth 1 L ~~> gset_bij_auth 1 ({[(a, b)]} ∪ L).
Proof.
intros. apply view_update=> n bijL.
rewrite !bij_view_rel_iff gset_op_union.
rewrite !gset_bij_view_rel_iff gset_op_union.
set_solver by eauto using gset_bijective_extend.
Qed.
End bij.
End gset_bij.
iris/base_logic/lib/bij.v deleted 100644 → 0
View file @ cd3b7b88
(** Propositions for reasoning about monotone partial bijections.
This library provides two propositions [bij_own_auth γ L] and [bij_own_elem γ a b], where [L]
is a bijection between types [A] and [B] represented by a set of associations
[gset (A*B)]. The idea is that [bij_own_auth γ L] is an authoritative bijection [L]
while [bij_own_elem γ a b] is a persistent resource saying [L] associates a and b.
The main use case is in a logical relation-based proof where [L] maintains the
association between locations [A] in one execution and [B] in another (perhaps
of different types, if the logical relation relates two different semantics).
The association [L] is always bijective, so that if [a] is mapped to [b], there
should be no other mappings for either [a] or [b]; the [bij_own_extend] update
theorem enforces that new mappings respect this property, and [bij_own_elem_agree]
allows the user to exploit bijectivity. The bijection grows monotonically, so
that the set of associations only grows; this is captured by the persistence of
[bij_own_elem].
This library is a logical, ownership-based wrapper around bij_view.v. *)
From iris.algebra.lib Require Import bij_view.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Import own.
From iris.proofmode Require Import tactics.
From iris.prelude Require Import options.
(* The uCMRA we need. *)
Class bijG A B `{Countable A, Countable B} Σ :=
BijG { bijG_inG :> inG Σ (bij_viewR A B); }.
Definition bijΣ A B `{Countable A, Countable B}: gFunctors :=
#[ GFunctor (bij_viewR A B) ].
Global Instance subG_bijΣ `{Countable A, Countable B} Σ :
subG (bijΣ A B) Σ → bijG A B Σ.
Proof. solve_inG. Qed.
Definition bij_own_auth_def `{bijG A B Σ} (γ : gname)
(q : Qp) (L : gset (A * B)) : iProp Σ := own γ (bij_auth q L).
Definition bij_own_auth_aux : seal (@bij_own_auth_def). Proof. by eexists. Qed.
Definition bij_own_auth := unseal bij_own_auth_aux.
Definition bij_own_auth_eq :
@bij_own_auth = @bij_own_auth_def := seal_eq bij_own_auth_aux.
Arguments bij_own_auth {_ _ _ _ _ _ _ _}.
Definition bij_own_elem_def `{bijG A B Σ} (γ : gname)
(a : A) (b : B) : iProp Σ := own γ (bij_elem a b).
Definition bij_own_elem_aux : seal (@bij_own_elem_def). Proof. by eexists. Qed.
Definition bij_own_elem := unseal bij_own_elem_aux.
Definition bij_own_elem_eq :
@bij_own_elem = @bij_own_elem_def := seal_eq bij_own_elem_aux.
Arguments bij_own_elem {_ _ _ _ _ _ _ _}.
Section bij.
Context `{bijG A B Σ}.
Implicit Types (L : gset (A * B)) (a : A) (b : B).
Global Instance bij_own_auth_timeless γ q L : Timeless (bij_own_auth γ q L).
Proof. rewrite bij_own_auth_eq. apply _. Qed.
Global Instance bij_own_elem_timeless γ a b : Timeless (bij_own_elem γ a b).
Proof. rewrite bij_own_elem_eq. apply _. Qed.
Global Instance bij_own_elem_persistent γ a b : Persistent (bij_own_elem γ a b).
Proof. rewrite bij_own_elem_eq. apply _. Qed.
Global Instance bij_own_auth_fractional γ L : Fractional (λ q, bij_own_auth γ q L).
Proof. intros p q. rewrite bij_own_auth_eq -own_op bij_auth_frac_op //. Qed.
Global Instance bij_own_auth_as_fractional γ q L :
AsFractional (bij_own_auth γ q L) (λ q, bij_own_auth γ q L) q.
Proof. split; [auto|apply _]. Qed.
Lemma bij_own_auth_agree γ q1 q2 L1 L2 :
bij_own_auth γ q1 L1 -∗ bij_own_auth γ q2 L2 -∗
⌜✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1⌝.
Proof.
rewrite bij_own_auth_eq. iIntros "H1 H2".
by iDestruct (own_valid_2 with "H1 H2") as %?%bij_auth_frac_op_valid.
Qed.
Lemma bij_own_auth_exclusive γ L1 L2 :
bij_own_auth γ 1 L1 -∗ bij_own_auth γ 1 L2 -∗ False.
Proof.
iIntros "H1 H2".
by iDestruct (bij_own_auth_agree with "H1 H2") as %[[] _].
Qed.
Lemma bij_own_valid γ q L :
bij_own_auth γ q L -∗ ⌜✓ q ∧ gset_bijective L⌝.
Proof.
rewrite bij_own_auth_eq. iIntros "Hauth".
by iDestruct (own_valid with "Hauth") as %?%bij_auth_frac_valid.
Qed.
Lemma bij_own_elem_agree γ L a a' b b' :
bij_own_elem γ a b -∗ bij_own_elem γ a' b' -∗
⌜a = a' ↔ b = b'⌝.
Proof.
rewrite bij_own_elem_eq. iIntros "Hel1 Hel2".
by iDestruct (own_valid_2 with "Hel1 Hel2") as %?%bij_elem_agree.
Qed.
Lemma bij_get_elem γ q L a b :
(a, b) ∈ L →
bij_own_auth γ q L -∗ bij_own_elem γ a b.
Proof.
intros. rewrite bij_own_auth_eq bij_own_elem_eq.
by apply own_mono, bij_view_included.
Qed.
Lemma bij_get_big_sepS_elem γ q L :
bij_own_auth γ q L -∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
Proof.
iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
by iApply bij_get_elem.
Qed.
Lemma bij_own_alloc L :
gset_bijective L →
⊢ |==> ∃ γ, bij_own_auth γ 1 L ∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
Proof.
intro. iAssert (∃ γ, bij_own_auth γ 1 L)%I with "[>]" as (γ) "Hauth".
{ rewrite bij_own_auth_eq. iApply own_alloc. by apply bij_auth_valid. }
iExists γ. iModIntro. iSplit; [done|]. by iApply bij_get_big_sepS_elem.
Qed.
Lemma bij_own_alloc_empty :
⊢ |==> ∃ γ, bij_own_auth γ 1 ∅.
Proof. iMod (bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
Lemma bij_own_extend γ L a b :
(∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
bij_own_auth γ 1 L ==∗ bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
Proof.
iIntros (??) "Hauth".
iAssert (bij_own_auth γ 1 ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
{ rewrite bij_own_auth_eq. iApply (own_update with "Hauth").
by apply bij_auth_extend. }
iModIntro. iSplit; [done|]. iApply (bij_get_elem with "Hauth"). set_solver.
Qed.
Lemma bij_own_extend_internal γ L a b :
(∀ b', bij_own_elem γ a b' -∗ False) -∗
(∀ a', bij_own_elem γ a' b -∗ False) -∗
bij_own_auth γ 1 L ==∗ bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
Proof.
iIntros "Ha Hb HL".
iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.
{ iIntros (b' ?). iApply ("Ha" $! b'). by iApply bij_get_elem. }
iAssert ⌜∀ a', (a', b) ∉ L⌝%I as %?.
{ iIntros (a' ?). iApply ("Hb" $! a'). by iApply bij_get_elem. }
by iApply (bij_own_extend with "HL").
Qed.
End bij.
iris/base_logic/lib/gset_bij.v 0 → 100644
View file @ 170c4eb3
(** Propositions for reasoning about monotone partial bijections.
This library provides two propositions [gset_bij_own_auth γ L] and [gset_bij_own_elem γ a b], where [L]
is a bijection between types [A] and [B] represented by a set of associations
[gset (A*B)]. The idea is that [gset_bij_own_auth γ L] is an authoritative bijection [L]
while [gset_bij_own_elem γ a b] is a persistent resource saying [L] associates a and b.
The main use case is in a logical relation-based proof where [L] maintains the
association between locations [A] in one execution and [B] in another (perhaps
of different types, if the logical relation relates two different semantics).
The association [L] is always bijective, so that if [a] is mapped to [b], there
should be no other mappings for either [a] or [b]; the [gset_bij_own_extend] update
theorem enforces that new mappings respect this property, and [gset_bij_own_elem_agree]
allows the user to exploit bijectivity. The bijection grows monotonically, so
that the set of associations only grows; this is captured by the persistence of
[gset_bij_own_elem].
This library is a logical, ownership-based wrapper around gset_bij. *)
From iris.algebra.lib Require Import gset_bij.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Import own.
From iris.proofmode Require Import tactics.
From iris.prelude Require Import options.
(* The uCMRA we need. *)
Class gset_bijG A B `{Countable A, Countable B} Σ :=
GsetBijG { gset_bijG_inG :> inG Σ (gset_bijR A B); }.
Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
#[ GFunctor (gset_bijR A B) ].
Global Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
subG (gset_bijΣ A B) Σ → gset_bijG A B Σ.
Proof. solve_inG. Qed.
Definition gset_bij_own_auth_def `{gset_bijG A B Σ} (γ : gname)
(q : Qp) (L : gset (A * B)) : iProp Σ := own γ (gset_bij_auth q L).
Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def). Proof. by eexists. Qed.
Definition gset_bij_own_auth := unseal gset_bij_own_auth_aux.
Definition gset_bij_own_auth_eq :
@gset_bij_own_auth = @gset_bij_own_auth_def := seal_eq gset_bij_own_auth_aux.
Arguments gset_bij_own_auth {_ _ _ _ _ _ _ _}.
Definition gset_bij_own_elem_def `{gset_bijG A B Σ} (γ : gname)
(a : A) (b : B) : iProp Σ := own γ (gset_bij_elem a b).
Definition gset_bij_own_elem_aux : seal (@gset_bij_own_elem_def). Proof. by eexists. Qed.
Definition gset_bij_own_elem := unseal gset_bij_own_elem_aux.
Definition gset_bij_own_elem_eq :
@gset_bij_own_elem = @gset_bij_own_elem_def := seal_eq gset_bij_own_elem_aux.
Arguments gset_bij_own_elem {_ _ _ _ _ _ _ _}.
Section gset_bij.
Context `{gset_bijG A B Σ}.
Implicit Types (L : gset (A * B)) (a : A) (b : B).
Global Instance gset_bij_own_auth_timeless γ q L :
Timeless (gset_bij_own_auth γ q L).
Proof. rewrite gset_bij_own_auth_eq. apply _. Qed.
Global Instance gset_bij_own_elem_timeless γ a b :
Timeless (gset_bij_own_elem γ a b).
Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
Global Instance gset_bij_own_elem_persistent γ a b :
Persistent (gset_bij_own_elem γ a b).
Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
Global Instance gset_bij_own_auth_fractional γ L :
Fractional (λ q, gset_bij_own_auth γ q L).
Proof.
intros p q. rewrite gset_bij_own_auth_eq -own_op gset_bij_auth_frac_op //.
Qed.
Global Instance gset_bij_own_auth_as_fractional γ q L :
AsFractional (gset_bij_own_auth γ q L) (λ q, gset_bij_own_auth γ q L) q.
Proof. split; [auto|apply _]. Qed.
Lemma gset_bij_own_auth_agree γ q1 q2 L1 L2 :
gset_bij_own_auth γ q1 L1 -∗ gset_bij_own_auth γ q2 L2 -∗
⌜✓ (q1 + q2)%Qp ∧ L1 = L2 ∧ gset_bijective L1⌝.
Proof.
rewrite gset_bij_own_auth_eq. iIntros "H1 H2".
by iDestruct (own_valid_2 with "H1 H2") as %?%gset_bij_auth_frac_op_valid.
Qed.
Lemma gset_bij_own_auth_exclusive γ L1 L2 :
gset_bij_own_auth γ 1 L1 -∗ gset_bij_own_auth γ 1 L2 -∗ False.
Proof.
iIntros "H1 H2".
by iDestruct (gset_bij_own_auth_agree with "H1 H2") as %[[] _].
Qed.
Lemma gset_bij_own_valid γ q L :
gset_bij_own_auth γ q L -∗ ⌜✓ q ∧ gset_bijective L⌝.
Proof.
rewrite gset_bij_own_auth_eq. iIntros "Hauth".
by iDestruct (own_valid with "Hauth") as %?%gset_bij_auth_frac_valid.
Qed.
Lemma gset_bij_own_elem_agree γ L a a' b b' :
gset_bij_own_elem γ a b -∗ gset_bij_own_elem γ a' b' -∗
⌜a = a' ↔ b = b'⌝.
Proof.
rewrite gset_bij_own_elem_eq. iIntros "Hel1 Hel2".
by iDestruct (own_valid_2 with "Hel1 Hel2") as %?%gset_bij_elem_agree.
Qed.
Lemma bij_get_elem γ q L a b :
(a, b) ∈ L →
gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b.
Proof.
intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
by apply own_mono, bij_view_included.
Qed.
Lemma bij_get_big_sepS_elem γ q L :
gset_bij_own_auth γ q L -∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
Proof.
iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
by iApply bij_get_elem.
Qed.
Lemma gset_bij_own_alloc L :
gset_bijective L →
⊢ |==> ∃ γ, gset_bij_own_auth γ 1 L ∗ [∗ set] ab ∈ L, gset_bij_own_elem γ ab.1 ab.2.
Proof.
intro. iAssert (∃ γ, gset_bij_own_auth γ 1 L)%I with "[>]" as (γ) "Hauth".
{ rewrite gset_bij_own_auth_eq. iApply own_alloc. by apply gset_bij_auth_valid. }
iExists γ. iModIntro. iSplit; [done|]. by iApply bij_get_big_sepS_elem.
Qed.
Lemma gset_bij_own_alloc_empty :
⊢ |==> ∃ γ, gset_bij_own_auth γ 1 ∅.
Proof. iMod (gset_bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
Lemma gset_bij_own_extend γ L a b :
(∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
gset_bij_own_auth γ 1 L ==∗
gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
Proof.
iIntros (??) "Hauth".
iAssert (gset_bij_own_auth γ 1 ({[a, b]} ∪ L)) with "[> Hauth]" as "Hauth".
{ rewrite gset_bij_own_auth_eq. iApply (own_update with "Hauth").
by apply gset_bij_auth_extend. }
iModIntro. iSplit; [done|]. iApply (bij_get_elem with "Hauth"). set_solver.
Qed.
Lemma gset_bij_own_extend_internal γ L a b :
(∀ b', gset_bij_own_elem γ a b' -∗ False) -∗
(∀ a', gset_bij_own_elem γ a' b -∗ False) -∗
gset_bij_own_auth γ 1 L ==∗
gset_bij_own_auth γ 1 ({[(a, b)]} ∪ L) ∗ gset_bij_own_elem γ a b.
Proof.
iIntros "Ha Hb HL".
iAssert ⌜∀ b', (a, b') ∉ L⌝%I as %?.
{ iIntros (b' ?). iApply ("Ha" $! b'). by iApply bij_get_elem. }
iAssert ⌜∀ a', (a', b) ∉ L⌝%I as %?.
{ iIntros (a' ?). iApply ("Hb" $! a'). by iApply bij_get_elem. }
by iApply (gset_bij_own_extend with "HL").
Qed.
End gset_bij.