Commit 5b0fd25d authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'dfrac-view' into 'master'

Generalize frac to dfrac in auth and view camera

Closes #395

See merge request iris/iris!622
parents 672648b8 3e206cd0
......@@ -3,6 +3,29 @@ way the logic is used on paper. We also document changes in the Coq
development; every API-breaking change should be listed, but not every new
lemma.
## Iris master
**Changes in `algebra`:**
* Generalize the authorative elements of the `view`, `auth` and `gset_bij`
cameras to be parameterized by a [discardable fraction](iris/algebra/dfrac.v)
(`dfrac`) instead of a fraction (`frac`). Normal fractions are now denoted
`●{#q} a` and `●V{#q} a`. Lemmas affected by this have been renamed such that
the "frac" in their name has been changed into "dfrac".
The following `sed` script helps adjust your code to the renaming (on macOS,
replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
```
sed -i -E -f- $(find theories -name "*.v") <<EOF
# auth and view renames from frac to dfrac
s/\b(auth|view)_(auth|both)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
EOF
```
## Iris 3.4.0
The highlights and most notable changes of this release are as follows:
......
From iris.algebra Require Export view.
From iris.algebra Require Export view frac.
From iris.algebra Require Import proofmode_classes big_op.
From iris.prelude Require Import options.
(** The authoritative camera with fractional authoritative elements *)
(** The authoritative camera has 2 types of elements: the authoritative
element [●{q} a] and the fragment [◯ b] (of which there can be several). To
enable sharing of the authoritative element [●{q} a], it is equiped with a
fraction [q]. Updates are only possible with the full authoritative element
[● a] (syntax for [●{1} a]]), while fractional authoritative elements have
agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
(** The authoritative camera has 2 types of elements: the authoritative element
[●{dq} a] and the fragment [◯ b] (of which there can be several). To enable
sharing of the authoritative element [●{dq} a], it is equiped with a
discardable fraction [dq]. Updates are only possible with the full
authoritative element [● a] (syntax for [●{#1} a]]), while fractional
authoritative elements have agreement, i.e., [✓ (●{dq1} a1 ⋅ ●{dq2} a2) → a1 ≡
a2]. *)
(** * Definition of the view relation *)
(** The authoritative camera is obtained by instantiating the view camera. *)
......@@ -61,7 +62,7 @@ Definition authO (A : ucmra) : ofe := viewO (A:=A) (B:=A) auth_view_rel.
Definition authR (A : ucmra) : cmra := viewR (A:=A) (B:=A) auth_view_rel.
Definition authUR (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.
Definition auth_auth {A: ucmra} : Qp A auth A := view_auth.
Definition auth_auth {A: ucmra} : dfrac A auth A := view_auth.
Definition auth_frag {A: ucmra} : A auth A := view_frag.
Typeclasses Opaque auth_auth auth_frag.
......@@ -69,9 +70,13 @@ Typeclasses Opaque auth_auth auth_frag.
Global Instance: Params (@auth_auth) 2 := {}.
Global Instance: Params (@auth_frag) 1 := {}.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Notation "●{ dq } a" := (auth_auth dq a) (at level 20, format "●{ dq } a").
Notation "●{# q } a" := (auth_auth (DfracOwn q) a) (at level 20, format "●{# q } a").
Notation "●□ a" := (auth_auth (DfracDiscarded) a) (at level 20).
Notation "● a" := (auth_auth (DfracOwn 1) a) (at level 20).
Notation "◯ a" := (auth_frag a) (at level 20).
Notation "●{ q } a" := (auth_auth q a) (at level 20, format "●{ q } a").
Notation "● a" := (auth_auth 1 a) (at level 20).
(** * Laws of the authoritative camera *)
(** We omit the usual [equivI] lemma because it is hard to state a suitably
......@@ -81,10 +86,12 @@ Section auth.
Context {A : ucmra}.
Implicit Types a b : A.
Implicit Types x y : auth A.
Implicit Types q : frac.
Implicit Types dq : dfrac.
Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
Global Instance auth_auth_ne dq : NonExpansive (@auth_auth A dq).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_auth_proper q : Proper (() ==> ()) (@auth_auth A q).
Global Instance auth_auth_proper dq : Proper (() ==> ()) (@auth_auth A dq).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
Proof. rewrite /auth_frag. apply _. Qed.
......@@ -102,8 +109,8 @@ Section auth.
Global Instance auth_ofe_discrete : OfeDiscrete A OfeDiscrete (authO A).
Proof. apply _. Qed.
Global Instance auth_auth_discrete q a :
Discrete a Discrete (ε : A) Discrete ({q} a).
Global Instance auth_auth_discrete dq a :
Discrete a Discrete (ε : A) Discrete ({dq} a).
Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_discrete a : Discrete a Discrete ( a).
Proof. rewrite /auth_frag. apply _. Qed.
......@@ -111,10 +118,12 @@ Section auth.
Proof. apply _. Qed.
(** Operation *)
Lemma auth_auth_frac_op p q a : {p + q} a {p} a {q} a.
Lemma auth_auth_dfrac_op dq1 dq2 a : {dq1 dq2} a {dq1} a {dq2} a.
Proof. apply view_auth_dfrac_op. Qed.
Lemma auth_auth_frac_op q1 q2 a : {#(q1 + q2)} a {#q1} a {#q2} a.
Proof. apply view_auth_frac_op. Qed.
Global Instance auth_auth_frac_is_op q q1 q2 a :
IsOp q q1 q2 IsOp' ({q} a) ({q1} a) ({q2} a).
Global Instance auth_auth_dfrac_is_op dq dq1 dq2 a :
IsOp dq dq1 dq2 IsOp' ({dq} a) ({dq1} a) ({dq2} a).
Proof. rewrite /auth_auth. apply _. Qed.
Lemma auth_frag_op a b : (a b) = a b.
......@@ -146,22 +155,22 @@ Section auth.
Proof. apply (big_opMS_commute _). Qed.
(** Validity *)
Lemma auth_auth_frac_op_invN n p a q b : {n} ({p} a {q} b) a {n} b.
Proof. apply view_auth_frac_op_invN. Qed.
Lemma auth_auth_frac_op_inv p a q b : ({p} a {q} b) a b.
Proof. apply view_auth_frac_op_inv. Qed.
Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
({p} a {q} b) a = b.
Proof. by apply view_auth_frac_op_inv_L. Qed.
Lemma auth_auth_frac_validN n q a : {n} ({q} a) (q 1)%Qp {n} a.
Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
Lemma auth_auth_dfrac_op_invN n dq1 a dq2 b : {n} ({dq1} a {dq2} b) a {n} b.
Proof. apply view_auth_dfrac_op_invN. Qed.
Lemma auth_auth_dfrac_op_inv dq1 a dq2 b : ({dq1} a {dq2} b) a b.
Proof. apply view_auth_dfrac_op_inv. Qed.
Lemma auth_auth_dfrac_op_inv_L `{!LeibnizEquiv A} dq1 a dq2 b :
({dq1} a {dq2} b) a = b.
Proof. by apply view_auth_dfrac_op_inv_L. Qed.
Lemma auth_auth_dfrac_validN n dq a : {n} ({dq} a) dq {n} a.
Proof. by rewrite view_auth_dfrac_validN auth_view_rel_unit. Qed.
Lemma auth_auth_validN n a : {n} ( a) {n} a.
Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.
Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
{n} ({q1} a1 {q2} a2) (q1 + q2 1)%Qp a1 {n} a2 {n} a1.
Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
Lemma auth_auth_dfrac_op_validN n dq1 dq2 a1 a2 :
{n} ({dq1} a1 {dq2} a2) (dq1 dq2) a1 {n} a2 {n} a1.
Proof. by rewrite view_auth_dfrac_op_validN auth_view_rel_unit. Qed.
Lemma auth_auth_op_validN n a1 a2 : {n} ( a1 a2) False.
Proof. apply view_auth_op_validN. Qed.
......@@ -180,15 +189,15 @@ Section auth.
Lemma auth_frag_op_validN_2 n b1 b2 : {n} (b1 b2) {n} ( b1 b2).
Proof. apply auth_frag_op_validN. Qed.
Lemma auth_both_frac_validN n q a b :
{n} ({q} a b) (q 1)%Qp b {n} a {n} a.
Proof. apply view_both_frac_validN. Qed.
Lemma auth_both_dfrac_validN n dq a b :
{n} ({dq} a b) dq b {n} a {n} a.
Proof. apply view_both_dfrac_validN. Qed.
Lemma auth_both_validN n a b : {n} ( a b) b {n} a {n} a.
Proof. apply view_both_validN. Qed.
Lemma auth_auth_frac_valid q a : ({q} a) (q 1)%Qp a.
Lemma auth_auth_dfrac_valid dq a : ({dq} a) dq a.
Proof.
rewrite view_auth_frac_valid !cmra_valid_validN.
rewrite view_auth_dfrac_valid !cmra_valid_validN.
by setoid_rewrite auth_view_rel_unit.
Qed.
Lemma auth_auth_valid a : ( a) a.
......@@ -197,10 +206,10 @@ Section auth.
by setoid_rewrite auth_view_rel_unit.
Qed.
Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
({q1} a1 {q2} a2) (q1 + q2 1)%Qp a1 a2 a1.
Lemma auth_auth_dfrac_op_valid dq1 dq2 a1 a2 :
({dq1} a1 {dq2} a2) (dq1 dq2) a1 a2 a1.
Proof.
rewrite view_auth_frac_op_valid !cmra_valid_validN.
rewrite view_auth_dfrac_op_valid !cmra_valid_validN.
setoid_rewrite auth_view_rel_unit. done.
Qed.
Lemma auth_auth_op_valid a1 a2 : ( a1 a2) False.
......@@ -227,10 +236,10 @@ Section auth.
(** These lemma statements are a bit awkward as we cannot possibly extract a
single witness for [b ≼ a] from validity, we have to make do with one witness
per step-index, i.e., [∀ n, b ≼{n} a]. *)
Lemma auth_both_frac_valid q a b :
({q} a b) (q 1)%Qp ( n, b {n} a) a.
Lemma auth_both_dfrac_valid dq a b :
({dq} a b) dq ( n, b {n} a) a.
Proof.
rewrite view_both_frac_valid. apply and_iff_compat_l. split.
rewrite view_both_dfrac_valid. apply and_iff_compat_l. split.
- intros Hrel. split.
+ intros n. by destruct (Hrel n).
+ apply cmra_valid_validN=> n. by destruct (Hrel n).
......@@ -238,35 +247,35 @@ Section auth.
Qed.
Lemma auth_both_valid a b :
( a b) ( n, b {n} a) a.
Proof. rewrite auth_both_frac_valid. naive_solver. Qed.
Proof. rewrite auth_both_dfrac_valid. split; [naive_solver|done]. Qed.
(* The reverse direction of the two lemmas below only holds if the camera is
discrete. *)
Lemma auth_both_frac_valid_2 q a b : (q 1)%Qp a b a ({q} a b).
Lemma auth_both_dfrac_valid_2 dq a b : dq a b a ({dq} a b).
Proof.
intros. apply auth_both_frac_valid.
intros. apply auth_both_dfrac_valid.
naive_solver eauto using cmra_included_includedN.
Qed.
Lemma auth_both_valid_2 a b : a b a ( a b).
Proof. intros ??. by apply auth_both_frac_valid_2. Qed.
Proof. intros ??. by apply auth_both_dfrac_valid_2. Qed.
Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} q a b :
({q} a b) (q 1)%Qp b a a.
Lemma auth_both_dfrac_valid_discrete `{!CmraDiscrete A} dq a b :
({dq} a b) dq b a a.
Proof.
rewrite auth_both_frac_valid. setoid_rewrite <-cmra_discrete_included_iff.
rewrite auth_both_dfrac_valid. setoid_rewrite <-cmra_discrete_included_iff.
naive_solver eauto using O.
Qed.
Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
( a b) b a a.
Proof. rewrite auth_both_frac_valid_discrete. naive_solver. Qed.
Proof. rewrite auth_both_dfrac_valid_discrete. split; [naive_solver|done]. Qed.
(** Inclusion *)
Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
{p1} a1 {n} {p2} a2 b (p1 p2)%Qp a1 {n} a2.
Proof. apply view_auth_frac_includedN. Qed.
Lemma auth_auth_frac_included p1 p2 a1 a2 b :
{p1} a1 {p2} a2 b (p1 p2)%Qp a1 a2.
Proof. apply view_auth_frac_included. Qed.
Lemma auth_auth_dfrac_includedN n dq1 dq2 a1 a2 b :
{dq1} a1 {n} {dq2} a2 b (dq1 dq2 dq1 = dq2) a1 {n} a2.
Proof. apply view_auth_dfrac_includedN. Qed.
Lemma auth_auth_dfrac_included dq1 dq2 a1 a2 b :
{dq1} a1 {dq2} a2 b (dq1 dq2 dq1 = dq2) a1 a2.
Proof. apply view_auth_dfrac_included. Qed.
Lemma auth_auth_includedN n a1 a2 b :
a1 {n} a2 b a1 {n} a2.
Proof. apply view_auth_includedN. Qed.
......@@ -274,21 +283,23 @@ Section auth.
a1 a2 b a1 a2.
Proof. apply view_auth_included. Qed.
Lemma auth_frag_includedN n p a b1 b2 :
b1 {n} {p} a b2 b1 {n} b2.
Lemma auth_frag_includedN n dq a b1 b2 :
b1 {n} {dq} a b2 b1 {n} b2.
Proof. apply view_frag_includedN. Qed.
Lemma auth_frag_included p a b1 b2 :
b1 {p} a b2 b1 b2.
Lemma auth_frag_included dq a b1 b2 :
b1 {dq} a b2 b1 b2.
Proof. apply view_frag_included. Qed.
(** The weaker [auth_both_included] lemmas below are a consequence of the
[auth_auth_included] and [auth_frag_included] lemmas above. *)
Lemma auth_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
{p1} a1 b1 {n} {p2} a2 b2 (p1 p2)%Qp a1 {n} a2 b1 {n} b2.
Proof. apply view_both_frac_includedN. Qed.
Lemma auth_both_frac_included p1 p2 a1 a2 b1 b2 :
{p1} a1 b1 {p2} a2 b2 (p1 p2)%Qp a1 a2 b1 b2.
Proof. apply view_both_frac_included. Qed.
Lemma auth_both_dfrac_includedN n dq1 dq2 a1 a2 b1 b2 :
{dq1} a1 b1 {n} {dq2} a2 b2
(dq1 dq2 dq1 = dq2) a1 {n} a2 b1 {n} b2.
Proof. apply view_both_dfrac_includedN. Qed.
Lemma auth_both_dfrac_included dq1 dq2 a1 a2 b1 b2 :
{dq1} a1 b1 {dq2} a2 b2
(dq1 dq2 dq1 = dq2) a1 a2 b1 b2.
Proof. apply view_both_dfrac_included. Qed.
Lemma auth_both_includedN n a1 a2 b1 b2 :
a1 b1 {n} a2 b2 a1 {n} a2 b1 {n} b2.
Proof. apply view_both_includedN. Qed.
......@@ -314,11 +325,13 @@ Section auth.
intros. etrans; first exact: auth_update_alloc.
exact: cmra_update_op_l.
Qed.
Lemma auth_update_auth_persist dq a : {dq} a ~~> ●□ a.
Proof. apply view_update_auth_persist. Qed.
Lemma auth_update_frac_alloc q a b `{!CoreId b} :
b a {q} a ~~> {q} a b.
Lemma auth_update_dfrac_alloc dq a b `{!CoreId b} :
b a {dq} a ~~> {dq} a b.
Proof.
intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
intros Ha%(core_id_extract _ _). apply view_update_dfrac_alloc=> n bf [??].
split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
Qed.
......
......@@ -153,7 +153,7 @@ Section dfrac.
- by destruct (Qp_add_id_free q q2).
- by destruct (Qp_add_id_free q q1).
Qed.
Global Instance frac_id_free q : IdFree (DfracOwn q).
Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
Proof. intros [q'| |q'] _ [=]. by apply (Qp_add_id_free q q'). Qed.
Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
Proof. by constructor. Qed.
......
......@@ -77,7 +77,7 @@ Section frac_auth.
Lemma frac_auth_auth_validN n a : {n} (F a) {n} a.
Proof.
rewrite auth_auth_frac_validN Some_validN. split.
rewrite auth_auth_dfrac_validN Some_validN. split.
- by intros [?[]].
- intros. by split.
Qed.
......
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export view gmap dfrac.
From iris.algebra Require Export view gmap frac dfrac.
From iris.algebra Require Import local_updates proofmode_classes big_op.
From iris.prelude Require Import options.
......@@ -12,7 +12,7 @@ persistent read-only ownership of a key.
The key frame-preserving updates are [gmap_view_alloc] to allocate a new key,
[gmap_view_update] to update a key given full ownership of the corresponding
fragment, and [gmap_view_freeze] to make a key read-only by discarding any
fragment, and [gmap_view_persist] to make a key read-only by discarding any
fraction of the corresponding fragment. Crucially, the latter does not require
owning the authoritative element.
......@@ -138,7 +138,7 @@ Section definitions.
Context {K : Type} `{Countable K} {V : ofe}.
Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
V{q} m.
V{#q} m.
Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
V {[k := (dq, to_agree v)]}.
End definitions.
......@@ -178,24 +178,24 @@ Section lemmas.
(** Composition and validity *)
Lemma gmap_view_auth_frac_op p q m :
gmap_view_auth (p + q) m gmap_view_auth p m gmap_view_auth q m.
Proof. apply view_auth_frac_op. Qed.
Proof. by rewrite /gmap_view_auth -dfrac_op_own view_auth_dfrac_op. Qed.
Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
IsOp q q1 q2 IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
Proof. rewrite /gmap_view_auth. apply _. Qed.
Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
{n} (gmap_view_auth p m1 gmap_view_auth q m2) m1 {n} m2.
Proof. apply view_auth_frac_op_invN. Qed.
Proof. apply view_auth_dfrac_op_invN. Qed.
Lemma gmap_view_auth_frac_op_inv p m1 q m2 :
(gmap_view_auth p m1 gmap_view_auth q m2) m1 m2.
Proof. apply view_auth_frac_op_inv. Qed.
Proof. apply view_auth_dfrac_op_inv. Qed.
Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
(gmap_view_auth p m1 gmap_view_auth q m2) m1 = m2.
Proof. apply view_auth_frac_op_inv_L, _. Qed.
Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
Lemma gmap_view_auth_frac_valid m q : gmap_view_auth q m (q 1)%Qp.
Proof.
rewrite view_auth_frac_valid. intuition eauto using gmap_view_rel_unit.
rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_valid m : gmap_view_auth 1 m.
Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
......@@ -203,12 +203,12 @@ Section lemmas.
Lemma gmap_view_auth_frac_op_validN n q1 q2 m1 m2 :
{n} (gmap_view_auth q1 m1 gmap_view_auth q2 m2) (q1 + q2)%Qp m1 {n} m2.
Proof.
rewrite view_auth_frac_op_validN. intuition eauto using gmap_view_rel_unit.
rewrite view_auth_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
(gmap_view_auth q1 m1 gmap_view_auth q2 m2) (q1 + q2 1)%Qp m1 m2.
Proof.
rewrite view_auth_frac_op_valid. intuition eauto using gmap_view_rel_unit.
rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_frac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
(gmap_view_auth q1 m1 gmap_view_auth q2 m2) (q1 + q2)%Qp m1 = m2.
......@@ -265,7 +265,7 @@ Section lemmas.
(q 1)%Qp dq m !! k {n} Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag.
rewrite view_both_frac_validN gmap_view_rel_lookup.
rewrite view_both_dfrac_validN gmap_view_rel_lookup.
naive_solver.
Qed.
Lemma gmap_view_both_validN n m k dq v :
......@@ -277,7 +277,7 @@ Section lemmas.
(q 1)%Qp dq m !! k Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag.
rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.
rewrite view_both_dfrac_valid. setoid_rewrite gmap_view_rel_lookup.
split=>[[Hq Hm]|[Hq Hm]].
- split; first done. split.
+ apply (Hm 0%nat).
......
......@@ -106,7 +106,7 @@ Definition gset_bijUR A B `{Countable A, Countable B} : ucmra :=
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.
(dq : dfrac) (L : gset (A * B)) : gset_bij A B := V{dq} L V L.
Definition gset_bij_elem `{Countable A, Countable B}
(a : A) (b : B) : gset_bij A B := V {[a, b]}.
......@@ -114,59 +114,60 @@ Section gset_bij.
Context `{Countable A, Countable B}.
Implicit Types (a:A) (b:B).
Implicit Types (L : gset (A*B)).
Implicit Types dq : dfrac.
Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
Proof. apply _. Qed.
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.
Lemma gset_bij_auth_dfrac_op dq1 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_frac_op.
rewrite (comm _ (V{q2} _)) -!assoc (assoc _ (V _)).
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_frac_valid q L : gset_bij_auth q L q gset_bijective L.
Lemma gset_bij_auth_dfrac_valid dq L : gset_bij_auth dq L dq gset_bijective L.
Proof.
rewrite /gset_bij_auth view_both_frac_valid.
rewrite /gset_bij_auth view_both_dfrac_valid.
setoid_rewrite gset_bij_view_rel_iff.
naive_solver eauto using O.
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 gset_bij_auth_valid L : 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_frac_valid q : gset_bij_auth (A:=A) (B:=B) q q.
Lemma gset_bij_auth_empty_dfrac_valid dq : gset_bij_auth (A:=A) (B:=B) dq dq.
Proof.
rewrite gset_bij_auth_frac_valid. naive_solver eauto using gset_bijective_empty.
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) 1 .
Proof. by apply gset_bij_auth_empty_frac_valid. 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_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.
Lemma gset_bij_auth_dfrac_op_valid dq1 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{q2} _)) -!assoc (assoc _ (V _)).
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_frac_op_valid.
- move=> /cmra_valid_op_l /view_auth_dfrac_op_valid.
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 gset_bij_view_rel_iff. 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_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.
(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_frac_valid q L a b :
(gset_bij_auth q L gset_bij_elem a b) q gset_bijective L (a, b) L.
Lemma bij_both_dfrac_valid dq 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_frac_valid.
rewrite /gset_bij_auth /gset_bij_elem -assoc -view_frag_op view_both_dfrac_valid.
setoid_rewrite gset_bij_view_rel_iff.
set_solver by eauto using O.
Qed.
Lemma bij_both_valid L a b :
(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.
(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_agree a1 b1 a2 b2 :
(gset_bij_elem a1 b1 gset_bij_elem a2 b2) (a1 = a2 b1 = b2).
......@@ -176,8 +177,8 @@ Section gset_bij.
naive_solver eauto using subseteq_gset_bijective, O.
Qed.
Lemma bij_view_included q L a b :
(a,b) L gset_bij_elem a b gset_bij_auth q L.
Lemma bij_view_included dq 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.
......@@ -185,7 +186,7 @@ Section gset_bij.
Lemma gset_bij_auth_extend {L} a b :
( b', (a, b') L) ( a', (a', b) L)
gset_bij_auth 1 L ~~> gset_bij_auth 1 ({[(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.
......
......@@ -14,7 +14,7 @@ fragment at the same value so that lemma [mono_nat_included], which states that