deprecated.v 2.59 KB
Newer Older
 Ralf Jung committed Dec 09, 2016 1 ``````From iris.algebra Require Import ofe cmra. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Ralf Jung committed Nov 22, 2016 3 4 5 6 `````` (* Old notation for backwards compatibility. *) (* Deprecated 2016-11-22. Use ofeT instead. *) `````` Ralf Jung committed Nov 22, 2016 7 ``````Notation cofeT := ofeT (only parsing). `````` Ralf Jung committed Dec 09, 2016 8 9 `````` (* Deprecated 2016-12-09. Use agree instead. *) `````` Ralf Jung committed Dec 13, 2016 10 ``````Module dec_agree. `````` Ralf Jung committed Dec 09, 2016 11 12 13 14 15 16 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. Local Arguments op _ _ _ !_ /. Local Arguments pcore _ _ !_ /. (* This is isomorphic to option, but has a very different RA structure. *) `````` Jacques-Henri Jourdan committed Dec 23, 2017 17 ``````Inductive dec_agree (A : Type) : Type := `````` Ralf Jung committed Dec 09, 2016 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 `````` | DecAgree : A → dec_agree A | DecAgreeBot : dec_agree A. Arguments DecAgree {_} _. Arguments DecAgreeBot {_}. Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x, match x with DecAgree a => Some a | _ => None end. Section dec_agree. Context `{EqDecision A}. Implicit Types a b : A. Implicit Types x y : dec_agree A. Instance dec_agree_valid : Valid (dec_agree A) := λ x, if x is DecAgree _ then True else False. Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A). Instance dec_agree_op : Op (dec_agree A) := λ x y, match x, y with | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot | _, _ => DecAgreeBot end. Instance dec_agree_pcore : PCore (dec_agree A) := Some. Definition dec_agree_ra_mixin : RAMixin (dec_agree A). Proof. apply ra_total_mixin; apply _ || eauto. - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match). - intros [?|] [?|]; by repeat (simplify_eq/= || case_match). - intros [?|]; by repeat (simplify_eq/= || case_match). - by intros [?|] [?|] ?. Qed. Canonical Structure dec_agreeR : cmraT := discreteR (dec_agree A) dec_agree_ra_mixin. `````` Robbert Krebbers committed Oct 25, 2017 53 ``````Global Instance dec_agree_cmra_discrete : CmraDiscrete dec_agreeR. `````` Robbert Krebbers committed Feb 22, 2017 54 ``````Proof. apply discrete_cmra_discrete. Qed. `````` Robbert Krebbers committed Oct 25, 2017 55 ``````Global Instance dec_agree_cmra_total : CmraTotal dec_agreeR. `````` Ralf Jung committed Dec 09, 2016 56 57 58 ``````Proof. intros x. by exists x. Qed. (* Some properties of this CMRA *) `````` Robbert Krebbers committed Oct 25, 2017 59 ``````Global Instance dec_agree_core_id (x : dec_agreeR) : CoreId x. `````` Ralf Jung committed Dec 09, 2016 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 ``````Proof. by constructor. Qed. Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot. Proof. intros. by rewrite /= decide_False. Qed. Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x = x. Proof. destruct x; by rewrite /= ?decide_True. Qed. Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2. Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed. Lemma DecAgree_included a b : DecAgree a ≼ DecAgree b ↔ a = b. Proof. split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->. Qed. End dec_agree. Arguments dec_agreeC : clear implicits. Arguments dec_agreeR _ {_}. `````` Ralf Jung committed Dec 13, 2016 79 ``End dec_agree.``