Require Export iris.cmra. Local Arguments disjoint _ _ !_ !_ /. Inductive excl (A : Type) := | Excl : A → excl A | ExclUnit : Empty (excl A) | ExclBot : excl A. Arguments Excl {_} _. Arguments ExclUnit {_}. Arguments ExclBot {_}. Existing Instance ExclUnit. Inductive excl_equiv `{Equiv A} : Equiv (excl A) := | Excl_equiv (x y : A) : x ≡ y → Excl x ≡ Excl y | ExclUnit_equiv : ∅ ≡ ∅ | ExclBot_equiv : ExclBot ≡ ExclBot. Existing Instance excl_equiv. Instance excl_valid {A} : Valid (excl A) := λ x, match x with Excl _ | ExclUnit => True | ExclBot => False end. Instance excl_empty {A} : Empty (excl A) := ExclUnit. Instance excl_unit {A} : Unit (excl A) := λ _, ∅. Instance excl_op {A} : Op (excl A) := λ x y, match x, y with | Excl x, ExclUnit | ExclUnit, Excl x => Excl x | ExclUnit, ExclUnit => ExclUnit | _, _=> ExclBot end. Instance excl_minus {A} : Minus (excl A) := λ x y, match x, y with | _, ExclUnit => x | Excl _, Excl _ => ExclUnit | _, _ => ExclBot end. Instance excl_ra `{Equiv A, !Equivalence (@equiv A _)} : RA (excl A). Proof. split. * split. + by intros []; constructor. + by destruct 1; constructor. + destruct 1; inversion 1; constructor; etransitivity; eauto. * by intros []; destruct 1; constructor. * constructor. * by destruct 1. * by do 2 destruct 1; constructor. * by intros [?| |] [?| |] [?| |]; constructor. * by intros [?| |] [?| |]; constructor. * by intros [?| |]; constructor. * constructor. * intros [?| |] [?| |]; exists ∅; constructor. * by intros [?| |] [?| |]. * by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor. Qed. Instance excl_empty_ra `{Equiv A, !Equivalence (@equiv A _)} : RAEmpty (excl A). Proof. split. done. by intros []. Qed. Lemma excl_update {A} (x : A) y : valid y → Excl x ⇝ y. Proof. by destruct y; intros ? [?| |]. Qed. Definition excl_above `{Equiv A, Op A} (x : A) (y : excl A) : Prop := match y with Excl y' => x ≼ y' | ExclUnit => True | ExclBot => False end. Instance: Params (@excl_above) 3. Section excl_above. Context `{RA A}. Global Instance excl_above_proper : Proper ((≡) ==> (≡) ==> iff) excl_above. Proof. by intros ?? Hx; destruct 1 as [?? Hy| |]; simpl; rewrite ?Hx,?Hy. Qed. Lemma excl_above_weaken (a b : A) x y : excl_above b y → a ≼ b → x ≼ y → excl_above a x. Proof. destruct x as [a'| |], y as [b'| |]; intros ?? [[] Hz]; inversion_clear Hz; simpl in *; try done. by setoid_subst; transitivity b. Qed. End excl_above.