frac_auth.v 5.1 KB
 Robbert Krebbers committed Jun 08, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 ``````From iris.algebra Require Export frac auth. From iris.algebra Require Export updates local_updates. From iris.proofmode Require Import classes. Definition frac_authR (A : cmraT) : cmraT := authR (optionUR (prodR fracR A)). Definition frac_authUR (A : cmraT) : ucmraT := authUR (optionUR (prodR fracR A)). Definition frac_auth_auth {A : cmraT} (x : A) : frac_authR A := ● (Some (1%Qp,x)). Definition frac_auth_frag {A : cmraT} (q : frac) (x : A) : frac_authR A := ◯ (Some (q,x)). Typeclasses Opaque frac_auth_auth frac_auth_frag. Instance: Params (@frac_auth_auth) 1. Instance: Params (@frac_auth_frag) 2. Notation "●! a" := (frac_auth_auth a) (at level 10). Notation "◯!{ q } a" := (frac_auth_frag q a) (at level 10, format "◯!{ q } a"). Notation "◯! a" := (frac_auth_frag 1 a) (at level 10). Section frac_auth. Context {A : cmraT}. Implicit Types a b : A. Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth A). Proof. solve_proper. Qed. Global Instance frac_auth_auth_proper : Proper ((≡) ==> (≡)) (@frac_auth_auth A). Proof. solve_proper. Qed. Global Instance frac_auth_frag_ne q : NonExpansive (@frac_auth_frag A q). Proof. solve_proper. Qed. Global Instance frac_auth_frag_proper q : Proper ((≡) ==> (≡)) (@frac_auth_frag A q). Proof. solve_proper. Qed. `````` Robbert Krebbers committed Oct 25, 2017 37 38 39 40 `````` Global Instance frac_auth_auth_discrete a : Discrete a → Discrete (●! a). Proof. intros; apply Auth_discrete; apply _. Qed. Global Instance frac_auth_frag_discrete a : Discrete a → Discrete (◯! a). Proof. intros; apply Auth_discrete, Some_discrete; apply _. Qed. `````` Robbert Krebbers committed Jun 08, 2017 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 `````` Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●! a ⋅ ◯! a). Proof. done. Qed. Lemma frac_auth_valid a : ✓ a → ✓ (●! a ⋅ ◯! a). Proof. done. Qed. Lemma frac_auth_agreeN n a b : ✓{n} (●! a ⋅ ◯! b) → a ≡{n}≡ b. Proof. rewrite auth_validN_eq /= => -[Hincl Hvalid]. by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??]. Qed. Lemma frac_auth_agree a b : ✓ (●! a ⋅ ◯! b) → a ≡ b. Proof. intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN. Qed. Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●! a ⋅ ◯! b) → a = b. Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed. Lemma frac_auth_includedN n q a b : ✓{n} (●! a ⋅ ◯!{q} b) → Some b ≼{n} Some a. Proof. by rewrite auth_validN_eq /= => -[/Some_pair_includedN [_ ?] _]. Qed. `````` Robbert Krebbers committed Oct 25, 2017 61 `````` Lemma frac_auth_included `{CmraDiscrete A} q a b : `````` Robbert Krebbers committed Jun 08, 2017 62 63 `````` ✓ (●! a ⋅ ◯!{q} b) → Some b ≼ Some a. Proof. by rewrite auth_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed. `````` Robbert Krebbers committed Oct 25, 2017 64 `````` Lemma frac_auth_includedN_total `{CmraTotal A} n q a b : `````` Robbert Krebbers committed Jun 08, 2017 65 66 `````` ✓{n} (●! a ⋅ ◯!{q} b) → b ≼{n} a. Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed. `````` Robbert Krebbers committed Oct 25, 2017 67 `````` Lemma frac_auth_included_total `{CmraDiscrete A, CmraTotal A} q a b : `````` Robbert Krebbers committed Jun 08, 2017 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 `````` ✓ (●! a ⋅ ◯!{q} b) → b ≼ a. Proof. intros. by eapply Some_included_total, frac_auth_included. Qed. Lemma frac_auth_auth_validN n a : ✓{n} (●! a) ↔ ✓{n} a. Proof. split; [by intros [_ [??]]|]. by repeat split; simpl; auto using ucmra_unit_leastN. Qed. Lemma frac_auth_auth_valid a : ✓ (●! a) ↔ ✓ a. Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed. Lemma frac_auth_frag_validN n q a : ✓{n} (◯!{q} a) ↔ ✓{n} q ∧ ✓{n} a. Proof. done. Qed. Lemma frac_auth_frag_valid q a : ✓ (◯!{q} a) ↔ ✓ q ∧ ✓ a. Proof. done. Qed. Lemma frag_auth_op q1 q2 a1 a2 : ◯!{q1+q2} (a1 ⋅ a2) ≡ ◯!{q1} a1 ⋅ ◯!{q2} a2. Proof. done. Qed. `````` Robbert Krebbers committed Jun 08, 2017 87 88 89 90 91 `````` Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯!{1} a ⋅ ◯!{q} b) → False. Proof. rewrite -frag_auth_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed. Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯!{1} a ⋅ ◯!{q} b) → False. Proof. rewrite -frag_auth_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed. `````` Robbert Krebbers committed Jun 08, 2017 92 93 94 95 `````` Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) : IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2). Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed. `````` Robbert Krebbers committed Nov 27, 2017 96 `````` Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a : A) : `````` Robbert Krebbers committed Oct 25, 2017 97 `````` CoreId a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a). `````` Robbert Krebbers committed Jun 08, 2017 98 `````` Proof. `````` Robbert Krebbers committed Jun 08, 2017 99 `````` rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->. `````` Robbert Krebbers committed Oct 25, 2017 100 `````` by rewrite -frag_auth_op -core_id_dup. `````` Robbert Krebbers committed Jun 08, 2017 101 102 103 104 105 106 107 `````` Qed. Lemma frac_auth_update q a b a' b' : (a,b) ~l~> (a',b') → ●! a ⋅ ◯!{q} b ~~> ●! a' ⋅ ◯!{q} b'. Proof. intros. by apply auth_update, option_local_update, prod_local_update_2. Qed. `````` Robbert Krebbers committed May 09, 2018 108 109 110 111 112 113 114 115 116 117 118 119 120 `````` Lemma frac_auth_update_alloc q a b c : (∀ n : nat, ✓{n} a → ✓{n} (c ⋅ a)) → ●! a ⋅ ◯!{q} b ~~> ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b). Proof. intros ?. by apply frac_auth_update, op_local_update. Qed. Lemma frac_auth_dealloc q a b c `{!Cancelable c} : ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b) ~~> ●! a ⋅ ◯!{q} b. Proof. apply frac_auth_update. move=> n [x|] /= Hvalid Heq; split; eauto using cmra_validN_op_r. eapply (cancelableN c); by rewrite ?assoc. Qed. `````` Robbert Krebbers committed Jun 08, 2017 121 ``End frac_auth.``