frac_auth.v 5.25 KB
 Jacques-Henri Jourdan committed Sep 13, 2019 1 ``````From iris.algebra Require Export frac auth updates local_updates. `````` Robbert Krebbers committed Oct 31, 2017 2 ``````From iris.algebra Require Import proofmode_classes. `````` Robbert Krebbers committed Jun 08, 2017 3 `````` `````` Hai Dang committed May 23, 2019 4 5 6 7 8 9 10 ``````(** Authoritative CMRA where the NON-authoritative parts can be fractional. This CMRA allows the original non-authoritative element `◯ a` to be split into fractional parts `◯!{q} a`. Using `◯! a ≡ ◯!{1} a` is in effect the same as using the original `◯ a`. Currently, however, this CMRA hides the ability to split the authoritative part into fractions. *) `````` Robbert Krebbers committed Jun 08, 2017 11 12 13 14 15 16 17 18 19 20 21 22 ``````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. `````` Maxime Dénès committed Jan 24, 2019 23 24 ``````Instance: Params (@frac_auth_auth) 1 := {}. Instance: Params (@frac_auth_frag) 2 := {}. `````` Robbert Krebbers committed Jun 08, 2017 25 `````` `````` Ralf Jung committed Jun 11, 2019 26 27 28 ``````Notation "●F a" := (frac_auth_auth a) (at level 10). Notation "◯F{ q } a" := (frac_auth_frag q a) (at level 10, format "◯F{ q } a"). Notation "◯F a" := (frac_auth_frag 1 a) (at level 10). `````` Robbert Krebbers committed Jun 08, 2017 29 30 31 32 33 34 35 36 37 38 39 40 41 42 `````` 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. `````` Ralf Jung committed Jun 11, 2019 43 `````` Global Instance frac_auth_auth_discrete a : Discrete a → Discrete (●F a). `````` Hai Dang committed May 23, 2019 44 `````` Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed. `````` Ralf Jung committed Jun 11, 2019 45 `````` Global Instance frac_auth_frag_discrete q a : Discrete a → Discrete (◯F{q} a). `````` Hai Dang committed May 23, 2019 46 `````` Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed. `````` Robbert Krebbers committed Jun 08, 2017 47 `````` `````` Ralf Jung committed Jun 11, 2019 48 `````` Lemma frac_auth_validN n a : ✓{n} a → ✓{n} (●F a ⋅ ◯F a). `````` Hai Dang committed May 23, 2019 49 `````` Proof. by rewrite auth_both_validN. Qed. `````` Ralf Jung committed Jun 11, 2019 50 `````` Lemma frac_auth_valid a : ✓ a → ✓ (●F a ⋅ ◯F a). `````` Robbert Krebbers committed May 24, 2019 51 `````` Proof. intros. by apply auth_both_valid_2. Qed. `````` Robbert Krebbers committed Jun 08, 2017 52 `````` `````` Ralf Jung committed Jun 11, 2019 53 `````` Lemma frac_auth_agreeN n a b : ✓{n} (●F a ⋅ ◯F b) → a ≡{n}≡ b. `````` Robbert Krebbers committed Jun 08, 2017 54 `````` Proof. `````` Hai Dang committed May 23, 2019 55 `````` rewrite auth_both_validN /= => -[Hincl Hvalid]. `````` Robbert Krebbers committed Jun 08, 2017 56 57 `````` by move: Hincl=> /Some_includedN_exclusive /(_ Hvalid ) [??]. Qed. `````` Ralf Jung committed Jun 11, 2019 58 `````` Lemma frac_auth_agree a b : ✓ (●F a ⋅ ◯F b) → a ≡ b. `````` Robbert Krebbers committed Jun 08, 2017 59 60 61 `````` Proof. intros. apply equiv_dist=> n. by apply frac_auth_agreeN, cmra_valid_validN. Qed. `````` Ralf Jung committed Jun 11, 2019 62 `````` Lemma frac_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●F a ⋅ ◯F b) → a = b. `````` Robbert Krebbers committed Jun 08, 2017 63 64 `````` Proof. intros. by apply leibniz_equiv, frac_auth_agree. Qed. `````` Ralf Jung committed Jun 11, 2019 65 `````` Lemma frac_auth_includedN n q a b : ✓{n} (●F a ⋅ ◯F{q} b) → Some b ≼{n} Some a. `````` Hai Dang committed May 23, 2019 66 `````` Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed. `````` Robbert Krebbers committed Oct 25, 2017 67 `````` Lemma frac_auth_included `{CmraDiscrete A} q a b : `````` Ralf Jung committed Jun 11, 2019 68 `````` ✓ (●F a ⋅ ◯F{q} b) → Some b ≼ Some a. `````` Robbert Krebbers committed May 24, 2019 69 `````` Proof. by rewrite auth_both_valid /= => -[/Some_pair_included [_ ?] _]. Qed. `````` Robbert Krebbers committed Oct 25, 2017 70 `````` Lemma frac_auth_includedN_total `{CmraTotal A} n q a b : `````` Ralf Jung committed Jun 11, 2019 71 `````` ✓{n} (●F a ⋅ ◯F{q} b) → b ≼{n} a. `````` Robbert Krebbers committed Jun 08, 2017 72 `````` Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed. `````` Robbert Krebbers committed Oct 25, 2017 73 `````` Lemma frac_auth_included_total `{CmraDiscrete A, CmraTotal A} q a b : `````` Ralf Jung committed Jun 11, 2019 74 `````` ✓ (●F a ⋅ ◯F{q} b) → b ≼ a. `````` Robbert Krebbers committed Jun 08, 2017 75 76 `````` Proof. intros. by eapply Some_included_total, frac_auth_included. Qed. `````` Ralf Jung committed Jun 11, 2019 77 `````` Lemma frac_auth_auth_validN n a : ✓{n} (●F a) ↔ ✓{n} a. `````` Robbert Krebbers committed Jun 08, 2017 78 `````` Proof. `````` Hai Dang committed May 23, 2019 79 80 `````` rewrite auth_auth_frac_validN Some_validN. split. by intros [?[]]. intros. by split. `````` Robbert Krebbers committed Jun 08, 2017 81 `````` Qed. `````` Ralf Jung committed Jun 11, 2019 82 `````` Lemma frac_auth_auth_valid a : ✓ (●F a) ↔ ✓ a. `````` Robbert Krebbers committed Jun 08, 2017 83 84 `````` Proof. rewrite !cmra_valid_validN. by setoid_rewrite frac_auth_auth_validN. Qed. `````` Ralf Jung committed Jun 11, 2019 85 `````` Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ ✓{n} q ∧ ✓{n} a. `````` Robbert Krebbers committed Jun 08, 2017 86 `````` Proof. done. Qed. `````` Ralf Jung committed Jun 11, 2019 87 `````` Lemma frac_auth_frag_valid q a : ✓ (◯F{q} a) ↔ ✓ q ∧ ✓ a. `````` Robbert Krebbers committed Jun 08, 2017 88 89 `````` Proof. done. Qed. `````` Ralf Jung committed Jun 11, 2019 90 `````` Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2. `````` Robbert Krebbers committed Jun 08, 2017 91 92 `````` Proof. done. Qed. `````` Ralf Jung committed Jun 11, 2019 93 `````` Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) → False. `````` 94 `````` Proof. rewrite -frac_auth_frag_op frac_auth_frag_validN=> -[/exclusiveN_l []]. Qed. `````` Ralf Jung committed Jun 11, 2019 95 `````` Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) → False. `````` 96 `````` Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed. `````` Robbert Krebbers committed Jun 08, 2017 97 `````` `````` Robbert Krebbers committed Jun 08, 2017 98 `````` Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) : `````` Ralf Jung committed Jun 11, 2019 99 `````` IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2). `````` Robbert Krebbers committed Jun 08, 2017 100 101 `````` Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed. `````` Robbert Krebbers committed Nov 27, 2017 102 `````` Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a : A) : `````` Ralf Jung committed Jun 11, 2019 103 `````` CoreId a → IsOp q q1 q2 → IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a). `````` Robbert Krebbers committed Jun 08, 2017 104 `````` Proof. `````` Robbert Krebbers committed Jun 08, 2017 105 `````` rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->. `````` 106 `````` by rewrite -frac_auth_frag_op -core_id_dup. `````` Robbert Krebbers committed Jun 08, 2017 107 108 109 `````` Qed. Lemma frac_auth_update q a b a' b' : `````` Ralf Jung committed Jun 11, 2019 110 `````` (a,b) ~l~> (a',b') → ●F a ⋅ ◯F{q} b ~~> ●F a' ⋅ ◯F{q} b'. `````` Robbert Krebbers committed Jun 08, 2017 111 112 113 `````` Proof. intros. by apply auth_update, option_local_update, prod_local_update_2. Qed. `````` Robbert Krebbers committed Aug 02, 2018 114 `````` `````` Ralf Jung committed Jun 11, 2019 115 `````` Lemma frac_auth_update_1 a b a' : ✓ a' → ●F a ⋅ ◯F b ~~> ●F a' ⋅ ◯F a'. `````` Robbert Krebbers committed Aug 02, 2018 116 117 118 `````` Proof. intros. by apply auth_update, option_local_update, exclusive_local_update. Qed. `````` Robbert Krebbers committed Jun 08, 2017 119 ``End frac_auth.``