excl.v 2.51 KB
Newer Older
1
Require Export iris.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5
Local Arguments disjoint _ _ !_ !_ /.

Inductive excl (A : Type) :=
  | Excl : A  excl A
6
  | ExclUnit : Empty (excl A)
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10
  | ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclUnit {_}.
Arguments ExclBot {_}.
11
Existing Instance ExclUnit.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14

Inductive excl_equiv `{Equiv A} : Equiv (excl A) :=
  | Excl_equiv (x y : A) : x  y  Excl x  Excl y
15
  | ExclUnit_equiv :   
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17 18 19
  | 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.
20 21
Instance excl_empty {A} : Empty (excl A) := ExclUnit.
Instance excl_unit {A} : Unit (excl A) := λ _, .
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
  * intros [?| |] [?| |]; exists ; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
  * by intros [?| |] [?| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  * by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Qed.
53 54
Instance excl_empty_ra `{Equiv A, !Equivalence (@equiv A _)} : RAEmpty (excl A).
Proof. split. done. by intros []. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56 57
Lemma excl_update {A} (x : A) y : valid y  Excl x  y.
Proof. by destruct y; intros ? [?| |]. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60 61
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
62 63 64 65 66 67 68
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71
    destruct x as [a'| |], y as [b'| |];
      intros ?? [[] Hz]; inversion_clear Hz; simpl in *; try done.
    by setoid_subst; transitivity b.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  Qed.
73
End excl_above.