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.