...
 
Commits (2)
  • Robbert Krebbers's avatar
    The unbounded fractional camera. · a94a87cc
    Robbert Krebbers authored
    a94a87cc
  • Robbert Krebbers's avatar
    The unbounded fractional authoritative camera. · 1d67a47f
    Robbert Krebbers authored
    The unbounded fractional authoritative camera is a version of the fractional
    authoritative camera that can be used with fractions `> 1`.
    
    Most of the reasoning principles for this version of the fractional
    authoritative cameras are the same as for the original version. There are two
    difference:
    
    - We get the additional rule that can be used to allocate a "surplus", i.e.
      if we have the authoritative element we can always increase its fraction
      and allocate a new fragment.
    
          ✓ (a ⋅ b) → ●?{p} a ~~> ●?{p + q} (a ⋅ b) ⋅ ◯?{q} b
    
    - At the cost of that, we no longer have the `◯?{1} a` is an exclusive
      fragmental element (cf. `frac_auth_frag_validN_op_1_l`).
    1d67a47f
......@@ -26,6 +26,8 @@ theories/algebra/gmultiset.v
theories/algebra/coPset.v
theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/algebra/ufrac.v
theories/algebra/ufrac_auth.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
......
(** This file provides a version of the fractional camera whose elements are
in the internal (0,1] of the rational numbers.
Notice that this camera could in principled be obtained by restricting the
validity of the unbounded fractional camera [ufrac]. *)
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
(** Since the standard (0,1] fractional camera is used more often, we define
[frac] through a [Notation] instead of a [Definition]. That way, Coq infers the
[frac] camera by default. *)
Notation frac := Qp (only parsing).
Section frac.
......
(** This file provides a "bounded" version of the fractional camera whose
elements are in the interval (0,..) instead of (0,1]. *)
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
(** Since the standard (0,1] fractional camera [frac] is used more often, we
define [ufrac] through a [Definition] instead of a [Notation]. That way, Coq
infers the [frac] camera by default. *)
Definition ufrac := Qp.
Section ufrac.
Canonical Structure ufracC := leibnizC ufrac.
Instance ufrac_valid : Valid ufrac := λ x, True.
Instance ufrac_pcore : PCore ufrac := λ _, None.
Instance ufrac_op : Op ufrac := λ x y, (x + y)%Qp.
Lemma ufrac_included (x y : ufrac) : x y (x < y)%Qc.
Proof. by rewrite Qp_lt_sum. Qed.
Corollary ufrac_included_weak (x y : ufrac) : x y (x y)%Qc.
Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed.
Definition ufrac_ra_mixin : RAMixin ufrac.
Proof. split; try apply _; try done. Qed.
Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
Proof. apply discrete_cmra_discrete. Qed.
End ufrac.
Global Instance ufrac_cancelable (q : ufrac) : Cancelable q.
Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
Global Instance ufrac_id_free (q : ufrac) : 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.
Lemma ufrac_op' (q p : ufrac) : (p q) = (p + q)%Qp.
Proof. done. Qed.
Global Instance is_op_ufrac (q : ufrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
(** This file provides the unbounded fractional authoritative camera: a version
of the fractional authoritative camera that can be used with fractions [> 1].
Most of the reasoning principles for this version of the fractional
authoritative cameras are the same as for the original version. There are two
difference:
- We get the additional rule that can be used to allocate a "surplus", i.e.
if we have the authoritative element we can always increase its fraction
and allocate a new fragment.
<<<
✓ (a ⋅ b) → ●?{p} a ~~> ●?{p + q} (a ⋅ b) ⋅ ◯?{q} b
>>>
- We no longer have the [◯?{1} a] is the exclusive fragmental element (cf.
[frac_auth_frag_validN_op_1_l]).
*)
From iris.algebra Require Export auth frac.
From iris.algebra Require Import ufrac.
From iris.algebra Require Export updates local_updates.
From iris.algebra Require Import proofmode_classes.
From Coq Require Import QArith Qcanon.
Definition ufrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR ufracR A)).
Definition ufrac_authUR (A : cmraT) : ucmraT :=
authUR (optionUR (prodR ufracR A)).
Definition ufrac_auth_auth {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
(Some (q,x)).
Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A :=
(Some (q,x)).
Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
Instance: Params (@ufrac_auth_auth) 2.
Instance: Params (@ufrac_auth_frag) 2.
Notation "●?{ q } a" := (ufrac_auth_auth q a) (at level 10, format "●?{ q } a").
Notation "◯?{ q } a" := (ufrac_auth_frag q a) (at level 10, format "◯?{ q } a").
Section ufrac_auth.
Context {A : cmraT}.
Implicit Types a b : A.
Global Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_auth_proper q : Proper (() ==> ()) (@ufrac_auth_auth A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_frag_ne q : NonExpansive (@ufrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_frag_proper q : Proper (() ==> ()) (@ufrac_auth_frag A q).
Proof. solve_proper. Qed.
Global Instance ufrac_auth_auth_discrete a : Discrete a Discrete (?{q} a).
Proof. intros; apply Auth_discrete; apply _. Qed.
Global Instance ufrac_auth_frag_discrete a : Discrete a Discrete (?{q} a).
Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed.
Lemma ufrac_auth_validN n a p : {n} a {n} (?{p} a ?{p} a).
Proof. done. Qed.
Lemma ufrac_auth_valid p a : a (?{p} a ?{p} a).
Proof. done. Qed.
Lemma ufrac_auth_agreeN n p a b : {n} (?{p} a ?{p} b) a {n} b.
Proof.
rewrite auth_validN_eq /= => -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]].
move=> /discrete_iff /leibniz_equiv_iff; rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Qed.
Lemma ufrac_auth_agree p a b : (?{p} a ?{p} b) a b.
Proof.
intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
Qed.
Lemma ufrac_auth_agreeL `{!LeibnizEquiv A} p a b : (?{p} a ?{p} b) a = b.
Proof. intros. by eapply leibniz_equiv, ufrac_auth_agree. Qed.
Lemma ufrac_auth_includedN n p q a b : {n} (?{p} a ?{q} b) Some b {n} Some a.
Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed.
Lemma ufrac_auth_included `{CmraDiscrete A} q p a b :
(?{p} a ?{q} b) Some b Some a.
Proof. rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _] //. Qed.
Lemma ufrac_auth_includedN_total `{CmraTotal A} n q p a b :
{n} (?{p} a ?{q} b) b {n} a.
Proof. intros. by eapply Some_includedN_total, ufrac_auth_includedN. Qed.
Lemma ufrac_auth_included_total `{CmraDiscrete A, CmraTotal A} q p a b :
(?{p} a ?{q} b) b a.
Proof. intros. by eapply Some_included_total, ufrac_auth_included. Qed.
Lemma ufrac_auth_auth_validN n q a : {n} (?{q} a) {n} a.
Proof.
split; [by intros [_ [??]]|].
repeat split; simpl; by try apply: ucmra_unit_leastN.
Qed.
Lemma ufrac_auth_auth_valid q a : (?{q} a) a.
Proof. rewrite !cmra_valid_validN. by setoid_rewrite ufrac_auth_auth_validN. Qed.
Lemma ufrac_auth_frag_validN n q a : {n} (?{q} a) {n} a.
Proof. split. by intros [??]. by split. Qed.
Lemma ufrac_auth_frag_valid q a : (?{q} a) a.
Proof. split. by intros [??]. by split. Qed.
Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ?{q1+q2} (a1 a2) ?{q1} a1 ?{q2} a2.
Proof. done. Qed.
Global Instance is_op_ufrac_auth q q1 q2 a a1 a2 :
IsOp q q1 q2 IsOp a a1 a2 IsOp' (?{q} a) (?{q1} a1) (?{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance is_op_ufrac_auth_core_id q q1 q2 a :
CoreId a IsOp q q1 q2 IsOp' (?{q} a) (?{q1} a) (?{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
by rewrite -ufrac_auth_frag_op -core_id_dup.
Qed.
Lemma ufrac_auth_update p q a b a' b' :
(a,b) ~l~> (a',b') ?{p} a ?{q} b ~~> ?{p} a' ?{q} b'.
Proof.
intros. apply: auth_update.
apply: option_local_update. by apply: prod_local_update_2.
Qed.
Lemma ufrac_auth_update_surplus p q a b :
(a b) ?{p} a ~~> ?{p + q} (a b) ?{q} b.
Proof.
intros Hconsistent. apply: auth_update_alloc.
intros n m; simpl; intros [Hvalid1 Hvalid2] Heq.
split.
- split; by apply cmra_valid_validN.
- rewrite -pair_op Some_op Heq comm.
destruct m; simpl; [rewrite left_id | rewrite right_id]; done.
Qed.
End ufrac_auth.