From 7ff11e3928f42668a0b3958ba4f194c546b1f4ee Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Sat, 3 Oct 2020 19:41:25 +0200
Subject: [PATCH] Add dfrac
---
CHANGELOG.md | 2 +
_CoqProject | 1 +
theories/algebra/dfrac.v | 197 +++++++++++++++++++++++++++++++++++++++
theories/algebra/frac.v | 5 +-
4 files changed, 201 insertions(+), 4 deletions(-)
create mode 100644 theories/algebra/dfrac.v
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 735ea509d..c2d9876df 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,8 @@ With this release, we dropped support for Coq 8.9.
have been removed, in particular: `auth_equivI`, `auth_validI`,
`auth_included`, `auth_valid_discrete`, and `auth_both_op`. For validity, use
`auth_auth_valid*`, `auth_frag_valid*`, or `auth_both_valid*` instead.
+* Add the camera of discardable fractions `dfrac`. This is a generalization of
+ the normal fractional camera. See `theories/algebra/dfrac.v` for further information.
**Changes in `proofmode`:**
diff --git a/_CoqProject b/_CoqProject
index 7b786138c..3d82b5d8b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -23,6 +23,7 @@ theories/algebra/agree.v
theories/algebra/excl.v
theories/algebra/functions.v
theories/algebra/frac.v
+theories/algebra/dfrac.v
theories/algebra/csum.v
theories/algebra/list.v
theories/algebra/vector.v
diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
new file mode 100644
index 000000000..0a17ebb72
--- /dev/null
+++ b/theories/algebra/dfrac.v
@@ -0,0 +1,197 @@
+(** Camera of discardable fractions.
+
+ This is a generalisation of the fractional camera where elements can
+ represent both ownership of a fraction (as in the fractional camera) and the
+ knowledge that a fraction has been discarded.
+
+ Ownership of a fraction is denoted [DfracOwn q] and behaves identically to
+ [q] of the fractional camera.
+
+ Knowledge that a fraction has been discarded is denoted [DfracDiscarded p].
+ Elements of this form are their own core, making ownership of them
+ persistent. Resource composition combines knowledge that [p] and [p'] have been
+ discarded into the knowledge that [p max p'] has been discarded.
+
+ One can make a frame preserving update from _owning_ a fraction to _knowing_
+ that the fraction has been discarded.
+
+ Crucially, ownership over 1 is an exclusive element just as it is in the
+ fractional camera. Hence owning 1 implies that no fraction has been
+ discarded. Conversely, knowing that a fraction has been discarded implies
+ that no one can own 1. And, since discarding is an irreversible operation, it
+ also implies that no one can own 1 in the future *)
+
+From Coq.QArith Require Import Qcanon.
+From iris.algebra Require Export cmra proofmode_classes updates.
+From iris Require Import options.
+Set Default Proof Using "Type".
+
+(** An element of dfrac denotes ownership of a fraction, knowledge that a
+ fraction has been discarded, or both. Note that all elements can be written
+ on the form [DfracOwn q â‹… DfracDiscarded p]. This should be used instead
+ of [DfracBoth] which is for internal use only. *)
+Inductive dfrac :=
+ | DfracOwn : Qp → dfrac
+ | DfracDiscarded : Qp → dfrac
+ | DfracBoth : Qp → Qp → dfrac.
+
+Global Instance DfracOwn_inj : Inj (=) (=) DfracOwn.
+Proof. by injection 1. Qed.
+
+Global Instance DfracDiscarded_inj : Inj (=) (=) DfracDiscarded.
+Proof. by injection 1. Qed.
+
+Global Instance DfracBoth_inj : Inj2 (=) (=) (=) DfracBoth.
+Proof. by injection 1. Qed.
+
+Section dfrac.
+
+ Canonical Structure dfracO := leibnizO dfrac.
+
+ Implicit Types p q : Qp.
+
+ Implicit Types x y : dfrac.
+
+ (** An element is valid as long as the sum of its content is less than one. *)
+ Instance dfrac_valid : Valid dfrac := λ x,
+ match x with
+ | DfracOwn q => q ≤ 1%Qp
+ | DfracDiscarded p => p ≤ 1%Qp
+ | DfracBoth q p => (q + p)%Qp ≤ 1%Qp
+ end%Qc.
+
+ (** As in the fractional camera the core is undefined for elements denoting
+ ownership of a fraction. For elements denoting the knowledge that a fraction has
+ been discarded the core is the identity function. *)
+ Instance dfrac_pcore : PCore dfrac := λ x,
+ match x with
+ | DfracOwn q => None
+ | DfracDiscarded p => Some (DfracDiscarded p)
+ | DfracBoth q p => Some (DfracDiscarded p)
+ end.
+
+ (** When elements are combined, ownership is added together and knowledge of
+ discarded fractions is combined with the max operation. *)
+ Instance dfrac_op : Op dfrac := λ x y,
+ match x, y with
+ | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
+ | DfracOwn q, DfracDiscarded p' => DfracBoth q p'
+ | DfracOwn q, DfracBoth q' p' => DfracBoth (q + q') p'
+ | DfracDiscarded p, DfracOwn q' => DfracBoth q' p
+ | DfracDiscarded p, DfracDiscarded p' => DfracDiscarded (p `max` p')
+ | DfracDiscarded p, DfracBoth q' p' => DfracBoth q' (p `max` p')
+ | DfracBoth q p, DfracOwn q' => DfracBoth (q + q') p
+ | DfracBoth q p, DfracDiscarded p' => DfracBoth q (p `max` p')
+ | DfracBoth q p, DfracBoth q' p' => DfracBoth (q + q') (p `max` p')
+ end.
+
+ Lemma dfrac_op_own q p : DfracOwn p â‹… DfracOwn q = DfracOwn (p + q).
+ Proof. done. Qed.
+
+ Lemma dfrac_op_discarded q p :
+ DfracDiscarded p â‹… DfracDiscarded q = DfracDiscarded (p `max` q).
+ Proof. done. Qed.
+
+ Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qc.
+ Proof.
+ rewrite Qp_lt_sum. split.
+ - rewrite /included /op /dfrac_op. intros [[o|?|?] [= ->]]. by exists o.
+ - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
+ Qed.
+
+ Lemma dfrac_discarded_included q p :
+ DfracDiscarded q ≼ DfracDiscarded p ↔ (q ≤ p)%Qc.
+ Proof.
+ split.
+ - rewrite /included /op /dfrac_op. intros [[?|?|?] [= ->]]. apply Qp_le_max_l.
+ - intros ?. exists (DfracDiscarded p).
+ by rewrite dfrac_op_discarded /Qp_max decide_True.
+ Qed.
+
+ Definition dfrac_ra_mixin : RAMixin dfrac.
+ Proof.
+ split; try apply _.
+ - intros [?|?|??] y cx <-; intros [= <-]; eexists _; done.
+ - intros [?|?|??] [?|?|??] [?|?|??];
+ rewrite /op /dfrac_op 1?assoc 1?assoc; done.
+ - intros [?|?|??] [?|?|??];
+ rewrite /op /dfrac_op 1?(comm Qp_plus) 1?(comm Qp_max); done.
+ - intros [?|?|??] cx; rewrite /pcore /dfrac_pcore; intros [= <-];
+ rewrite /op /dfrac_op Qp_max_id; done.
+ - intros [?|?|??] ? [= <-]; done.
+ - intros [?|?|??] [?|?|??] ? [[?|?|??] [=]] [= <-]; eexists _; split; try done;
+ apply dfrac_discarded_included; subst; auto; apply Qp_le_max_l.
+ - intros [q|p|q p] [q'|p'|q' p']; rewrite /op /dfrac_op /valid /dfrac_valid.
+ * apply (Qp_plus_weak_r _ _ 1).
+ * apply (Qp_plus_weak_r _ _ 1).
+ * apply Qcle_trans. etrans; last apply Qp_le_plus_l. apply Qp_le_plus_l.
+ * apply (Qp_plus_weak_l _ _ 1).
+ * apply (Qp_max_lub_l _ _ 1).
+ * by intros ?%(Qp_plus_weak_l _ _ 1)%(Qp_max_lub_l _ _ 1).
+ * rewrite (comm _ _ q') -assoc. apply (Qp_plus_weak_l _ _ 1).
+ * intros H. etrans; last apply H.
+ apply Qcplus_le_mono_l. apply Qp_le_max_l.
+ * intros H. etrans; last apply H.
+ rewrite -assoc. apply Qcplus_le_mono_l, Qp_plus_weak_2_r, Qp_le_max_l.
+ Qed.
+ Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
+
+ Global Instance dfrac_cmra_discrete : CmraDiscrete dfracR.
+ Proof. apply discrete_cmra_discrete. Qed.
+
+ Global Instance dfrac_full_exclusive : Exclusive (DfracOwn 1).
+ Proof.
+ intros [q|p|q p];
+ rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid /=.
+ - apply (Qp_not_plus_ge 1 q).
+ - apply (Qp_not_plus_ge 1 p).
+ - rewrite -Qcplus_assoc. apply (Qp_not_plus_ge 1 (q + p)).
+ Qed.
+
+ Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
+ Proof.
+ apply: discrete_cancelable.
+ intros [q1|p1|q1 p1][q2|p2|q2 p2] _; rewrite /op /cmra_op; simpl;
+ try by intros [= ->].
+ - by intros ->%(inj _)%(inj _).
+ - by intros [?%symmetry%Qp_plus_id_free _]%(inj2 _).
+ - by intros [?%Qp_plus_id_free ?]%(inj2 _).
+ - by intros [->%(inj _) ->]%(inj2 _).
+ Qed.
+
+ Global Instance frac_id_free q : IdFree (DfracOwn q).
+ Proof.
+ intros [q'|p'|q' p'] _; rewrite /op /cmra_op; simpl; try by intros [=].
+ by intros [= ?%Qp_plus_id_free].
+ Qed.
+
+ Global Instance dfrac_discarded_core_id p : CoreId (DfracDiscarded p).
+ Proof. by constructor. Qed.
+
+ Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1%Qp)%Qc.
+ Proof. done. Qed.
+
+ Lemma dfrac_valid_discarded p : ✓ DfracDiscarded p ↔ (p ≤ 1%Qp)%Qc.
+ Proof. done. Qed.
+
+ Lemma dfrac_valid_own_discarded q p :
+ ✓ (DfracOwn q ⋅ DfracDiscarded p) ↔ (q + p ≤ 1%Qp)%Qc.
+ Proof. done. Qed.
+
+ Global Instance is_op_frac q : IsOp' (DfracOwn q) (DfracOwn (q/2)) (DfracOwn (q/2)).
+ Proof. by rewrite /IsOp' /IsOp dfrac_op_own Qp_div_2. Qed.
+
+ (** Discarding a fraction is a frame preserving update. *)
+ Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded q.
+ Proof.
+ intros n [[q'|p'|q' p']|];
+ rewrite /op /cmra_op -!cmra_discrete_valid_iff /valid /cmra_valid /=.
+ - by rewrite Qcplus_comm.
+ - intro. etrans. apply Qp_max_plus. done.
+ - intro. etrans; last done.
+ rewrite -Qcplus_assoc. rewrite (Qcplus_comm q _). rewrite -Qcplus_assoc.
+ apply Qcplus_le_mono_l. rewrite Qcplus_comm. apply Qp_max_plus.
+ - done.
+ Qed.
+
+End dfrac.
\ No newline at end of file
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 121c54296..85543266d 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -47,10 +47,7 @@ Global Instance frac_cancelable (q : frac) : Cancelable q.
Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
Global Instance frac_id_free (q : frac) : IdFree q.
-Proof.
- intros [q0 Hq0] ? EQ%Qp_eq. rewrite -{1}(Qcplus_0_r q) in EQ.
- eapply Qclt_not_eq; first done. by apply (inj (Qcplus q)).
-Qed.
+Proof. intros p _. apply Qp_plus_id_free. Qed.
Lemma frac_op' (q p : Qp) : (p â‹… q) = (p + q)%Qp.
Proof. done. Qed.
--
GitLab