### The unbounded fractional authoritative camera.

```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`).```
parent a94a87cc
 ... ... @@ -27,6 +27,7 @@ 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 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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!