excl.v 2.54 KB
Newer Older
1
Require Export iris.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
6
7
8
9
10
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 disjoint _ _ !_ !_ /.
Local Arguments included _ _ !_ !_ /.

Inductive excl (A : Type) :=
  | Excl : A  excl A
  | ExclUnit : excl A
  | ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclUnit {_}.
Arguments ExclBot {_}.

Inductive excl_equiv `{Equiv A} : Equiv (excl A) :=
  | Excl_equiv (x y : A) : x  y  Excl x  Excl y
  | ExclUnit_equiv : ExclUnit  ExclUnit
  | 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_unit {A} : Unit (excl A) := λ _, ExclUnit.
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_included `{Equiv A} : Included (excl A) := λ x y,
  match x, y with
  | Excl x, Excl y => x  y
  | ExclUnit, _ => True
  | _, ExclBot => True
  | _, _ => False
  end.
Definition excl_above `{Included A} (x : A) (y : excl A) : Prop :=
  match y with Excl y' => x  y' | ExclUnit => True | ExclBot => False 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 []; destruct 1; simpl; try (intros Hx; rewrite Hx).
  * by intros [?| |] [?| |] [?| |]; constructor.
  * by intros [?| |] [?| |]; constructor.
  * by intros [?| |]; constructor.
  * constructor.
  * by intros [?| |] [?| |].
  * by intros [?| |] [?| |].
  * by intros [?| |] [?| |]; simpl; try constructor.
  * by intros [?| |] [?| |] ?; try constructor.
Qed.
Lemma excl_update {A} (x : A) y : valid y  Excl x  y.
Proof. by destruct y; intros ? [?| |]. Qed.

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'| |]; simpl; intros ??; try done.
    by intros Hab; rewrite Hab; transitivity b.
  Qed.
End excl_above.