Move fragment trick into algebra layer. Clean up proofs.

iris/algebra/lib/bij_view.v

@@ -10,7 +10,9 @@ The fragments compose by set union, which means that fragments are their own
 core, ownership of a fragment is persistent, and the authoritative element can
 only grow (in that it can only map more pairs (a,b)). *)
 
-From iris.algebra Require Import view gset updates.
+(** view needs to be exported for the canonical instances *)
+From iris.algebra Require Export view gset.
+From iris.algebra Require Import updates.
 From iris.prelude Require Import options.
 
 Section partial_bijection.
@@ -25,7 +27,6 @@ Section partial_bijection.
     (∀ b', (a, b') ∈ L → b' = b) ∧ (∀ a', (a', b) ∈ L → a' = a).
 
   (* Properties of [gset_bijective]. *)
-
   Lemma gset_bijective_empty : gset_bijective (∅ : gset (A * B)).
   Proof. by intros ?? []%not_elem_of_empty. Qed.
 
@@ -72,126 +73,90 @@ Section bij.
     n2 ≤ n1 →
     bij_view_rel_raw n2 bijL2 L2.
   Proof.
-    rewrite /bij_view_rel_raw.
-    intros [HL1sub ?].
-    intros <-%(discrete_iff _ _)%leibniz_equiv HL2sub%gset_included _.
-    split; [|done].
-    by trans L1.
+    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.
-  Proof. intros _. hnf; auto. Qed.
+  Proof. by intros _. Qed.
 
   Local Lemma bij_view_rel_raw_unit n :
     ∃ bijL, bij_view_rel_raw n bijL ε.
-  Proof. exists ∅. hnf; eauto using gset_bijective_empty. Qed.
+  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.
+    ViewRel bij_view_rel_raw
+            bij_view_rel_raw_mono bij_view_rel_raw_valid bij_view_rel_raw_unit.
 
   Global Instance bij_view_rel_discrete : ViewRelDiscrete bij_view_rel.
-  Proof.
-    intros ???. intros [Hsub Hbij].
-    split; auto.
-  Qed.
+  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).
+    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_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} (L : gset (A * B)) : bij_view A B :=
+  ●V L ⋅ ◯V L.
+Definition bij_elem `{Countable A, Countable B} (a : A) (b : B) : bij_view A B :=
+  ◯V {[a, b]}.
 
 Section bij.
-  Context {A B : Type} `{Countable A, Countable B}.
+  Context `{Countable A, Countable B}.
   Implicit Types (a:A) (b:B).
   Implicit Types (L : gset (A*B)).
 
-  Definition bij_auth L : bij_view A B := ●V L.
-  Definition bij_subrel L : bij_view A B := ◯V L.
-  Definition bij_elem a b : bij_view A B := bij_subrel {[a, b]}.
-
-  Global Instance bij_subrel_core_id L : CoreId (bij_subrel L).
-  Proof. apply _. Qed.
-
   Global Instance bij_elem_core_id a b : CoreId (bij_elem a b).
   Proof. apply _. Qed.
 
-  Lemma bij_subrel_insert L a b :
-    bij_subrel ({[a, b]} ∪ L) = bij_elem a b ⋅ bij_subrel L.
-  Proof.
-    rewrite /bij_elem /bij_subrel.
-    rewrite -view_frag_op //.
-  Qed.
-
   Lemma bij_auth_valid L : ✓ bij_auth L ↔ gset_bijective L.
   Proof.
-    rewrite /bij_auth.
-    rewrite view_auth_valid.
-    setoid_rewrite bij_view_rel_iff.
-    split; [naive_solver eauto using O|].
-    intros; split; [ apply empty_subseteq | done ].
-  Qed.
-
-  Lemma bij_auth_valid_empty : ✓ bij_auth ∅.
-  Proof.
-    rewrite bij_auth_valid.
-    apply gset_bijective_empty.
-  Qed.
-
-  Lemma bij_both_subrel_valid L L' :
-    ✓ (bij_auth L ⋅ bij_subrel L') ↔ gset_bijective L ∧ L' ⊆ L.
-  Proof.
-    rewrite view_both_valid.
+    rewrite /bij_auth view_both_valid.
     setoid_rewrite bij_view_rel_iff.
     naive_solver eauto using O.
   Qed.
 
+  Lemma bij_auth_valid_empty : ✓ bij_auth (A:=A) (B:=B) ∅.
+  Proof. apply bij_auth_valid, gset_bijective_empty. Qed.
+
   Lemma bij_both_el_valid L a b :
     ✓ (bij_auth L ⋅ bij_elem a b) ↔ gset_bijective L ∧ (a, b) ∈ L.
   Proof.
-    rewrite /bij_elem bij_both_subrel_valid.
-    rewrite elem_of_subseteq_singleton //.
-  Qed.
-
-  Lemma bij_subrel_valid L : ✓ bij_subrel L ↔ gset_bijective L.
-  Proof.
-    rewrite view_frag_valid.
+    rewrite /bij_auth /bij_elem -assoc -view_frag_op view_both_valid.
     setoid_rewrite bij_view_rel_iff.
-    split; [|by eauto].
-    intros Hrel; destruct (Hrel 0) as [L' [? ?]].
-    eauto using subseteq_gset_bijective.
+    set_solver by eauto using O.
   Qed.
 
   Lemma bij_elem_agree a1 b1 a2 b2 :
     ✓ (bij_elem a1 b1 ⋅ bij_elem a2 b2) → (a1 = a2 ↔ b1 = b2).
   Proof.
-    rewrite /bij_elem.
-    rewrite -view_frag_op gset_op_union.
-    rewrite bij_subrel_valid.
-    apply gset_bijective_pair.
+    rewrite /bij_elem -view_frag_op gset_op_union view_frag_valid.
+    setoid_rewrite bij_view_rel_iff. intros. apply gset_bijective_pair.
+    naive_solver eauto using subseteq_gset_bijective, O.
+  Qed.
+
+  Lemma bij_view_included L a b : (a,b) ∈ L → bij_elem a b ≼ bij_auth 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 bij_auth_extend L a b :
     (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
-    bij_auth L ~~> bij_auth (({[(a, b)]} : gset (A * B)) ∪ L) ⋅ bij_elem a b.
+    bij_auth L ~~> bij_auth ({[(a, b)]} ∪ L).
   Proof.
-    intros.
-    apply view_update_alloc.
-    intros n bijL.
+    intros. apply view_update=> n bijL.
     rewrite !bij_view_rel_iff gset_op_union.
-    intros [Hsub Hbij].
-    split.
-    - apply union_mono_l; auto.
-    - eauto using gset_bijective_extend.
+    set_solver by eauto using gset_bijective_extend.
   Qed.
-
-  Lemma bij_auth_extend' {L} a b :
-    ¬(∃ b', (a, b') ∈ L) → ¬(∃ a', (a', b) ∈ L) →
-    bij_auth L ~~> bij_auth (({[(a, b)]} : gset (A * B)) ∪ L) ⋅ bij_elem a b.
-  Proof. by intros ??; apply bij_auth_extend; naive_solver. Qed.
 End bij.

iris/base_logic/lib/bij.v

@@ -18,150 +18,109 @@ that the set of associations only grows; this is captured by the persistence of
 
 This library is a logical, ownership-based wrapper around bij_view.v. *)
 
-From iris.algebra Require Import view gset lib.bij_view.
+From iris.algebra.lib Require Import bij_view.
 From iris.base_logic.lib Require Import own.
 From iris.proofmode Require Import tactics.
 From iris.prelude Require Import options.
 
-Section bij.
-  Context {A B : Type}.
-  Context `{Countable A, Countable B}.
-
-  (* The uCMRA we need. *)
-  Class bijG Σ :=
-    BijG { bijG_inG :> inG Σ (bij_viewR A B); }.
+(* The uCMRA we need. *)
+Class bijG A B `{Countable A, Countable B} Σ :=
+  BijG { bijG_inG :> inG Σ (bij_viewR A B); }.
 
-  Definition bijΣ : gFunctors := #[ GFunctor (bij_viewR A B) ].
-  Global Instance subG_bijΣ Σ : subG bijΣ Σ → bijG Σ.
-  Proof. solve_inG. Qed.
+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.
 
-  Context `{!bijG Σ}.
+Section bij.
+  Context `{bijG A B Σ}.
   Implicit Types (L: gsetO (A * B)).
   Implicit Types (a:A) (b:B).
 
-  Definition bij_own_auth_def γ L : iProp Σ := own γ (bij_auth L ⋅ bij_subrel L).
+  Definition bij_own_auth_def γ L : iProp Σ := own γ (bij_auth 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.
+  Definition bij_own_auth_eq :
+    @bij_own_auth = @bij_own_auth_def := seal_eq bij_own_auth_aux.
 
   Definition bij_own_elem_def γ a 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.
-
-  Local Ltac unseal :=
-    rewrite ?bij_own_auth_eq /bij_own_auth_def ?bij_own_elem_eq /bij_own_elem_def.
+  Definition bij_own_elem_eq :
+    @bij_own_elem = @bij_own_elem_def := seal_eq bij_own_elem_aux.
 
   Global Instance bij_own_auth_timeless γ L : Timeless (bij_own_auth γ L).
-  Proof. unseal. apply _. Qed.
+  Proof. rewrite bij_own_auth_eq. apply _. Qed.
 
   Global Instance bij_own_elem_timeless γ a b : Timeless (bij_own_elem γ a b).
-  Proof. unseal. apply _. Qed.
+  Proof. rewrite bij_own_elem_eq. apply _. Qed.
 
   Global Instance bij_own_elem_persistent γ a b : Persistent (bij_own_elem γ a b).
-  Proof. unseal. apply _. Qed.
+  Proof. rewrite bij_own_elem_eq. apply _. Qed.
 
-  Local Lemma bij_own_subrel_to_big_sepS γ L :
-    own γ (bij_subrel L) -∗ [∗ set] ab ∈ L, own γ (bij_elem ab.1 ab.2).
+  Lemma bij_own_bijective γ L :
+    bij_own_auth γ L -∗ ⌜gset_bijective L⌝.
   Proof.
-    induction L as [|[a b] L] using set_ind_L.
-    - rewrite big_sepS_empty. by iIntros "_".
-    - rewrite bij_subrel_insert own_op.
-      rewrite big_sepS_insert //=.
-      rewrite IHL //.
+    rewrite bij_own_auth_eq. iIntros "Hauth".
+    iDestruct (own_valid with "Hauth") as %?%bij_auth_valid; done.
   Qed.
 
-  Lemma bij_own_alloc L :
-    gset_bijective L →
-    ⊢ |==> ∃ γ, bij_own_auth γ L ∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
+  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.
-    unseal.
-    intros Hbij.
-    iMod (own_alloc (bij_auth L ⋅ bij_subrel L)) as (γ) "[Hauth #Hsub]".
-    { apply bij_both_subrel_valid; auto. }
-    iModIntro. iExists γ.
-    rewrite own_op. iFrame "Hsub ∗".
-    iApply bij_own_subrel_to_big_sepS; auto.
+    rewrite bij_own_elem_eq. iIntros "Hel1 Hel2".
+    by iDestruct (own_valid_2 with "Hel1 Hel2") as %?%bij_elem_agree.
   Qed.
 
-  Lemma bij_own_alloc_empty : ⊢ |==> ∃ γ, bij_own_auth γ ∅.
+  Lemma bij_get_elem γ L a b :
+    (a, b) ∈ L →
+    bij_own_auth γ L -∗ bij_own_elem γ a b.
   Proof.
-    iMod (bij_own_alloc ∅) as (γ) "[Hauth _]";
-      eauto using gset_bijective_empty.
+    intros. rewrite bij_own_auth_eq bij_own_elem_eq.
+    by apply own_mono, bij_view_included.
   Qed.
-
-  Lemma bij_own_bijective γ L :
-    bij_own_auth γ L -∗ ⌜gset_bijective L⌝.
+  Lemma bij_get_big_sepS_elem γ L :
+    bij_own_auth γ L -∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
   Proof.
-    unseal.
-    rewrite own_op.
-    iIntros "[Hauth _]".
-    iDestruct (own_valid with "Hauth") as %?%bij_auth_valid; done.
+    iIntros "Hauth". iApply big_sepS_forall. iIntros ([a b] ?) "/=".
+    by iApply bij_get_elem.
   Qed.
 
-  Lemma bij_own_elem_of γ L a b :
-    (a, b) ∈ L →
-    bij_own_auth γ L -∗ bij_own_elem γ a b.
+  Lemma bij_own_alloc L :
+    gset_bijective L →
+    ⊢ |==> ∃ γ, bij_own_auth γ L ∗ [∗ set] ab ∈ L, bij_own_elem γ ab.1 ab.2.
   Proof.
-    unseal.
-    iIntros (Hel) "[_ Hfrag]".
-    iDestruct (bij_own_subrel_to_big_sepS with "Hfrag") as "Hels".
-    iDestruct (big_sepS_elem_of _ _ _ Hel with "Hels") as "$".
-  Qed.
+    intro. iAssert (∃ γ, bij_own_auth γ 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 γ ∅.
+  Proof. iMod (bij_own_alloc ∅) as (γ) "[Hauth _]"; by auto. Qed.
 
   Lemma bij_own_extend γ L a b :
-    (∀ y, (a, y) ∉ L) → (∀ x, (x, b) ∉ L) →
-    bij_own_auth γ L ==∗
-    bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
+    (∀ b', (a, b') ∉ L) → (∀ a', (a', b) ∉ L) →
+    bij_own_auth γ L ==∗ bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
   Proof.
-    unseal.
-    iIntros (Ha Hb) "[HL Hfrag]".
-    rewrite own_op.
-    iMod (own_update with "HL") as "HL".
-    { apply (bij_auth_extend a b); eauto. }
-    iModIntro.
-    iDestruct "HL" as "[$ #Hsub]".
-    iFrame "Hsub".
-    rewrite bij_subrel_insert own_op; iFrame "#∗".
+    iIntros (??) "Hauth".
+    iAssert (bij_own_auth γ ({[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 :
-    (∀ y, bij_own_elem γ a y -∗ False) -∗
-    (∀ x, bij_own_elem γ x b -∗ False) -∗
-    bij_own_auth γ L ==∗
-    bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
+    (∀ b', bij_own_elem γ a b' -∗ False) -∗
+    (∀ a', bij_own_elem γ a' b -∗ False) -∗
+    bij_own_auth γ L ==∗ bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
   Proof.
     iIntros "Ha Hb HL".
-    iAssert (⌜∀ y, (a, y) ∉ L⌝)%I as %Ha.
-    { iIntros (y Hel).
-      iApply ("Ha" $! y).
-      iApply (bij_own_elem_of with "HL"); eauto. }
-    iAssert (⌜∀ x, (x, b) ∉ L⌝)%I as %Hb.
-    { iIntros (x Hel).
-      iApply ("Hb" $! x).
-      iApply (bij_own_elem_of with "HL"); eauto. }
-    iApply (bij_own_extend with "HL"); eauto.
-  Qed.
-
-  Lemma bij_own_extend' γ L a b :
-    ¬(∃ y, (a, y) ∈ L) → ¬(∃ x, (x, b) ∈ L) →
-    bij_own_auth γ L ==∗
-    bij_own_auth γ ({[(a, b)]} ∪ L) ∗ bij_own_elem γ a b.
-  Proof.
-    intros.
-    iApply bij_own_extend; naive_solver.
-  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.
-    unseal.
-    iIntros "Hel1 Hel2".
-    iDestruct (own_valid_2 with "Hel1 Hel2") as %?%bij_elem_agree.
-    auto.
+    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.
-
-Arguments bijG A B {_ _ _ _} _ : assert.
-Arguments bijΣ A B {_ _ _ _} : assert.