Commit 3e206cd0 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Make changes related to dfrac generalization

parent e4746602
......@@ -7,11 +7,11 @@ lemma.
**Changes in `algebra`:**
* Authorative elements of the `view`, `auth` and `gset_bij` cameras are
parameterized by a [discardable fraction](iris/algebra/dfrac.v) instead of a
fraction. 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".
* 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`).
......@@ -19,10 +19,10 @@ 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
/\b(auth|view)_auth_frac_op\b/! s/\b(auth|view)_(auth|both)_frac_(\w*)\b/\1_\2_dfrac_\3/g
/\bgset_bij_auth_frac/gset_bij_auth_dfrac/g
/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
/\bgbij_both_frac_valid\b/bij_both_dfrac_valid/g
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
```
......
......@@ -176,43 +176,43 @@ Section lemmas.
Qed.
(** Composition and validity *)
Lemma gmap_view_auth_dfrac_op p q m :
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. by rewrite /gmap_view_auth -dfrac_op_own view_auth_dfrac_op. Qed.
Global Instance gmap_view_auth_dfrac_is_op q q1 q2 m :
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_dfrac_op_invN n p m1 q m2 :
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_dfrac_op_invN. Qed.
Lemma gmap_view_auth_dfrac_op_inv p m1 q m2 :
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_dfrac_op_inv. Qed.
Lemma gmap_view_auth_dfrac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
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_dfrac_op_inv_L, _. Qed.
Lemma gmap_view_auth_dfrac_valid m q : gmap_view_auth q m (q 1)%Qp.
Lemma gmap_view_auth_frac_valid m q : gmap_view_auth q m (q 1)%Qp.
Proof.
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_dfrac_valid. done. Qed.
Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
Lemma gmap_view_auth_dfrac_op_validN n q1 q2 m1 m2 :
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_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_dfrac_op_valid q1 q2 m1 m2 :
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_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_dfrac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
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.
Proof. unfold_leibniz. apply gmap_view_auth_dfrac_op_valid. Qed.
Proof. unfold_leibniz. apply gmap_view_auth_frac_op_valid. Qed.
Lemma gmap_view_auth_op_validN n m1 m2 :
{n} (gmap_view_auth 1 m1 gmap_view_auth 1 m2) False.
......@@ -260,7 +260,7 @@ Section lemmas.
(gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2) (dq1 dq2) v1 = v2.
Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
Lemma gmap_view_both_dfrac_validN n q m k dq v :
Lemma gmap_view_both_frac_validN n q m k dq v :
{n} (gmap_view_auth q m gmap_view_frag k dq v)
(q 1)%Qp dq m !! k {n} Some v.
Proof.
......@@ -271,8 +271,8 @@ Section lemmas.
Lemma gmap_view_both_validN n m k dq v :
{n} (gmap_view_auth 1 m gmap_view_frag k dq v)
dq m !! k {n} Some v.
Proof. rewrite gmap_view_both_dfrac_validN. naive_solver done. Qed.
Lemma gmap_view_both_dfrac_valid q m k dq v :
Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
Lemma gmap_view_both_frac_valid q m k dq v :
(gmap_view_auth q m gmap_view_frag k dq v)
(q 1)%Qp dq m !! k Some v.
Proof.
......@@ -286,14 +286,14 @@ Section lemmas.
+ apply Hm.
+ revert n. apply equiv_dist. apply Hm.
Qed.
Lemma gmap_view_both_dfrac_valid_L `{!LeibnizEquiv V} q m k dq v :
Lemma gmap_view_both_frac_valid_L `{!LeibnizEquiv V} q m k dq v :
(gmap_view_auth q m gmap_view_frag k dq v)
q dq m !! k = Some v.
Proof. unfold_leibniz. apply gmap_view_both_dfrac_valid. Qed.
Proof. unfold_leibniz. apply gmap_view_both_frac_valid. Qed.
Lemma gmap_view_both_valid m k dq v :
(gmap_view_auth 1 m gmap_view_frag k dq v)
dq m !! k Some v.
Proof. rewrite gmap_view_both_dfrac_valid. naive_solver done. Qed.
Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
(* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
have [inv_L] lemmas instead that just have an equality on the RHS. *)
Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
......
......@@ -23,7 +23,7 @@ Section mono_nat.
Global Instance mono_nat_lb_core_id n : CoreId (mono_nat_lb n).
Proof. apply _. Qed.
Lemma mono_nat_auth_dfrac_op q1 q2 n :
Lemma mono_nat_auth_frac_op q1 q2 n :
mono_nat_auth q1 n mono_nat_auth q2 n mono_nat_auth (q1 + q2) n.
Proof.
rewrite /mono_nat_auth -dfrac_op_own auth_auth_dfrac_op.
......@@ -57,7 +57,7 @@ Section mono_nat.
Lemma mono_nat_auth_valid n : mono_nat_auth 1 n.
Proof. by apply auth_both_valid. Qed.
Lemma mono_nat_auth_dfrac_op_valid q1 q2 n1 n2 :
Lemma mono_nat_auth_frac_op_valid q1 q2 n1 n2 :
(mono_nat_auth q1 n1 mono_nat_auth q2 n2) (q1 + q2 1)%Qp n1 = n2.
Proof.
rewrite /mono_nat_auth (comm _ ({#q2} _)) -!assoc (assoc _ ( _)).
......@@ -68,7 +68,7 @@ Section mono_nat.
Qed.
Lemma mono_nat_auth_op_valid n1 n2 :
(mono_nat_auth 1 n1 mono_nat_auth 1 n2) False.
Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
Proof. rewrite mono_nat_auth_frac_op_valid. naive_solver. Qed.
Lemma mono_nat_both_frac_valid q n m :
(mono_nat_auth q n mono_nat_lb m) (q 1)%Qp m n.
......
......@@ -394,7 +394,7 @@ Section cmra.
split.
- intros [[[[dqf agf]|] bf]
[[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
+ split; [left; apply (cmra_included_l dq1)|]. apply to_agree_includedN. by exists agf.
+ split; [left; apply: cmra_included_l|]. apply to_agree_includedN. by exists agf.
+ split; [right; done|]. by apply (inj to_agree).
- intros [[[? ->]| ->] ->].
+ rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.
......
......@@ -53,7 +53,7 @@ Section mono_nat.
Global Instance mono_nat_auth_own_fractional γ n :
Fractional (λ q, mono_nat_auth_own γ q n).
Proof. unseal. intros p q. rewrite -own_op mono_nat_auth_dfrac_op //. Qed.
Proof. unseal. intros p q. rewrite -own_op mono_nat_auth_frac_op //. Qed.
Global Instance mono_nat_auth_own_as_fractional γ q n :
AsFractional (mono_nat_auth_own γ q n) (λ q, mono_nat_auth_own γ q n) q.
Proof. split; [auto|apply _]. Qed.
......@@ -64,7 +64,7 @@ Section mono_nat.
(q1 + q2 1)%Qp n1 = n2.
Proof.
unseal. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_dfrac_op_valid; done.
iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_frac_op_valid; done.
Qed.
Lemma mono_nat_auth_own_exclusive γ n1 n2 :
mono_nat_auth_own γ 1 n1 - mono_nat_auth_own γ 1 n2 - False.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment