ra.v 3.97 KB
Newer Older
1
Require Export prelude.collections prelude.relations.
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

Class Valid (A : Type) := valid : A  Prop.
Instance: Params (@valid) 2.

Class Unit (A : Type) := unit : A  A.
Instance: Params (@unit) 2.

Class Op (A : Type) := op : A  A  A.
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.

Class Included (A : Type) := included : relation A.
Instance: Params (@included) 2.
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
Hint Extern 0 (?x  ?x) => reflexivity.

Class Minus (A : Type) := minus : A  A  A.
Instance: Params (@minus) 2.
Infix "⩪" := minus (at level 40) : C_scope.

Class RA A `{Equiv A, Valid A, Unit A, Op A, Included A, Minus A} : Prop := {
  (* setoids *)
  ra_equivalence :> Equivalence (() : relation A);
  ra_op_proper x :> Proper (() ==> ()) (op x);
  ra_unit_proper :> Proper (() ==> ()) unit;
  ra_valid_proper :> Proper (() ==> impl) valid;
  ra_minus_proper :> Proper (() ==> () ==> ()) minus;
  ra_included_proper x :> Proper (() ==> impl) (included x);
  (* monoid *)
  ra_associative :> Associative () ();
  ra_commutative :> Commutative () ();
  ra_unit_l x : unit x  x  x;
  ra_unit_idempotent x : unit (unit x)  unit x;
  ra_unit_weaken x y : unit x  unit (x  y);
  ra_valid_op_l x y : valid (x  y)  valid x;
  ra_included_l x y : x  x  y;
  ra_op_difference x y : x  y  x  y  x  y
}.

(** Updates *)
Definition ra_update_set `{Op A, Valid A} (x : A) (P : A  Prop) :=
   z, valid (x  z)   y, P y  valid (y  z).
Instance: Params (@ra_update_set) 3.
Infix "⇝:" := ra_update_set (at level 70).
Definition ra_update `{Op A, Valid A} (x y : A) :=  z,
  valid (x  z)  valid (y  z).
Infix "⇝" := ra_update (at level 70).
Instance: Params (@ra_update) 3.

(** Properties **)
Section ra.
Context `{RA A}.
Implicit Types x y z : A.

Global Instance ra_valid_proper' : Proper (() ==> iff) valid.
Proof. by intros ???; split; apply ra_valid_proper. Qed.
Global Instance ra_op_proper' : Proper (() ==> () ==> ()) ().
Proof.
  intros x1 x2 Hx y1 y2 Hy.
  by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2).
Qed.
Lemma ra_valid_op_r x y : valid (x  y)  valid y.
Proof. rewrite (commutative _ x); apply ra_valid_op_l. Qed.

(** ** Units *)
Lemma ra_unit_r x : x  unit x  x.
Proof. by rewrite (commutative _ x), ra_unit_l. Qed.

(** ** Order *)
Lemma ra_included_spec x y : x  y   z, y  x  z.
Proof.
  split; [by exists (y  x); rewrite ra_op_difference|].
  intros [z Hz]; rewrite Hz; apply ra_included_l.
Qed.
Global Instance ra_included_proper' : Proper (() ==> () ==> iff) ().
Proof.
  intros x1 x2 Hx y1 y2 Hy; rewrite !ra_included_spec.
  by setoid_rewrite Hx; setoid_rewrite Hy.
Qed.
Global Instance: PreOrder included.
Proof.
  split.
  * by intros x; rewrite ra_included_spec; exists (unit x); rewrite ra_unit_r.
  * intros x y z; rewrite ?ra_included_spec; intros [z1 Hy] [z2 Hz].
    exists (z1  z2). by rewrite (associative _), <-Hy, <-Hz.
Qed.
Lemma ra_included_unit x : unit x  x.
Proof. by rewrite ra_included_spec; exists x; rewrite ra_unit_l. Qed.
Lemma ra_included_r x y : y  x  y.
Proof. rewrite (commutative _); apply ra_included_l. Qed.
Lemma ra_preserving_l x y z : x  y  z  x  z  y.
Proof.
  rewrite !ra_included_spec.
  by intros (z1&Hz1); exists z1; rewrite Hz1, (associative ()).
Qed.
Lemma ra_preserving_r x y z : x  y  x  z  y  z.
Proof. by intros; rewrite <-!(commutative _ z); apply ra_preserving_l. Qed.
Lemma ra_unit_preserving x y : x  y  unit x  unit y.
Proof.
  rewrite ra_included_spec; intros [z Hy]; rewrite Hy; apply ra_unit_weaken.
Qed.

(** ** Properties of [()] relation *)
Global Instance ra_update_preorder : PreOrder ra_update.
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
End ra.