deprecated.v 2.48 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 17 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 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. Local Arguments op _ _ _ !_ /. Local Arguments pcore _ _ !_ /. (* This is isomorphic to option, but has a very different RA structure. *) Inductive dec_agree (A : Type) : Type := | 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. Global Instance dec_agree_total : CMRATotal dec_agreeR. Proof. intros x. by exists x. Qed. (* Some properties of this CMRA *) Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x. 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 77 ``End dec_agree.``