From 170c4eb3f3b1977e50a7aee13f48d1ee118ed469 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Nov 2020 10:58:07 +0100
Subject: [PATCH] Consistently use name `gset_bij`.

---
 _CoqProject                                 |   4 +-
 iris/algebra/lib/{bij_view.v => gset_bij.v} | 137 +++++++++--------
 iris/base_logic/lib/bij.v                   | 148 -------------------
 iris/base_logic/lib/gset_bij.v              | 156 ++++++++++++++++++++
 4 files changed, 226 insertions(+), 219 deletions(-)
 rename iris/algebra/lib/{bij_view.v => gset_bij.v} (51%)
 delete mode 100644 iris/base_logic/lib/bij.v
 create mode 100644 iris/base_logic/lib/gset_bij.v

diff --git a/_CoqProject b/_CoqProject
index e03c587d6..534926fad 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -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
diff --git a/iris/algebra/lib/bij_view.v b/iris/algebra/lib/gset_bij.v
similarity index 51%
rename from iris/algebra/lib/bij_view.v
rename to iris/algebra/lib/gset_bij.v
index 07638c08e..d929be38a 100644
--- a/iris/algebra/lib/bij_view.v
+++ b/iris/algebra/lib/gset_bij.v
@@ -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.
diff --git a/iris/base_logic/lib/bij.v b/iris/base_logic/lib/bij.v
deleted file mode 100644
index 0afec803c..000000000
--- a/iris/base_logic/lib/bij.v
+++ /dev/null
@@ -1,148 +0,0 @@
-(** 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.
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
new file mode 100644
index 000000000..1b7a8484f
--- /dev/null
+++ b/iris/base_logic/lib/gset_bij.v
@@ -0,0 +1,156 @@
+(** 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.
-- 
GitLab