dra.v 9.21 KB
Newer Older
1
From iris.algebra Require Export cmra updates.
2
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
3

4
Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
5
  (* setoids *)
6
7
8
9
10
  mixin_dra_equivalence : Equivalence (() : relation A);
  mixin_dra_op_proper : Proper (() ==> () ==> ()) ();
  mixin_dra_core_proper : Proper (() ==> ()) core;
  mixin_dra_valid_proper : Proper (() ==> impl) valid;
  mixin_dra_disjoint_proper x : Proper (() ==> impl) (disjoint x);
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  (* validity *)
12
13
  mixin_dra_op_valid x y :  x   y  x  y   (x  y);
  mixin_dra_core_valid x :  x   core x;
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  (* monoid *)
15
16
17
18
19
20
21
22
23
  mixin_dra_assoc : Assoc () ();
  mixin_dra_disjoint_ll x y z :  x   y   z  x  y  x  y  z  x  z;
  mixin_dra_disjoint_move_l x y z :
     x   y   z  x  y  x  y  z  x  y  z;
  mixin_dra_symmetric : Symmetric (@disjoint A _);
  mixin_dra_comm x y :  x   y  x  y  x  y  y  x;
  mixin_dra_core_disjoint_l x :  x  core x  x;
  mixin_dra_core_l x :  x  core x  x  x;
  mixin_dra_core_idemp x :  x  core (core x)  core x;
24
  mixin_dra_core_mono x y : 
Robbert Krebbers's avatar
Robbert Krebbers committed
25
     z,  x   y  x  y  core (x  y)  core x  z   z  core x  z
Robbert Krebbers's avatar
Robbert Krebbers committed
26
}.
27
Structure draT := DraT {
28
29
30
31
32
33
  dra_car :> Type;
  dra_equiv : Equiv dra_car;
  dra_core : Core dra_car;
  dra_disjoint : Disjoint dra_car;
  dra_op : Op dra_car;
  dra_valid : Valid dra_car;
34
  dra_mixin : DraMixin dra_car
35
}.
36
Arguments DraT _ {_ _ _ _ _} _.
37
38
39
40
41
42
43
44
45
Arguments dra_car : simpl never.
Arguments dra_equiv : simpl never.
Arguments dra_core : simpl never.
Arguments dra_disjoint : simpl never.
Arguments dra_op : simpl never.
Arguments dra_valid : simpl never.
Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
(** Lifting properties from the mixin *)
Section dra_mixin.
  Context {A : draT}.
  Implicit Types x y : A.
  Global Instance dra_equivalence : Equivalence (() : relation A).
  Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
  Global Instance dra_op_proper : Proper (() ==> () ==> ()) (@op A _).
  Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
  Global Instance dra_core_proper : Proper (() ==> ()) (@core A _).
  Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
  Global Instance dra_valid_proper : Proper (() ==> impl) (@valid A _).
  Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
  Global Instance dra_disjoint_proper x : Proper (() ==> impl) (disjoint x).
  Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
  Lemma dra_op_valid x y :  x   y  x  y   (x  y).
  Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
  Lemma dra_core_valid x :  x   core x.
  Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
  Global Instance dra_assoc : Assoc () (@op A _).
  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
  Lemma dra_disjoint_ll x y z :  x   y   z  x  y  x  y  z  x  z.
  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
  Lemma dra_disjoint_move_l x y z :
     x   y   z  x  y  x  y  z  x  y  z.
  Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
  Global Instance  dra_symmetric : Symmetric (@disjoint A _).
  Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
  Lemma dra_comm x y :  x   y  x  y  x  y  y  x.
  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
  Lemma dra_core_disjoint_l x :  x  core x  x.
  Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
  Lemma dra_core_l x :  x  core x  x  x.
  Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
  Lemma dra_core_idemp x :  x  core (core x)  core x.
  Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
82
  Lemma dra_core_mono x y : 
83
     z,  x   y  x  y  core (x  y)  core x  z   z  core x  z.
84
  Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
End dra_mixin.

Record validity (A : draT) := Validity {
  validity_car : A;
  validity_is_valid : Prop;
  validity_prf : validity_is_valid  valid validity_car
}.
Add Printing Constructor validity.
Arguments Validity {_} _ _ _.
Arguments validity_car {_} _.
Arguments validity_is_valid {_} _.

Definition to_validity {A : draT} (x : A) : validity A :=
  Validity x (valid x) id.

(* The actual construction *)
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Section dra.
102
103
104
Context (A : draT).
Implicit Types a b : A.
Implicit Types x y z : validity A.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
Arguments valid _ _ !_ /.
106

107
108
Instance validity_valid : Valid (validity A) := validity_is_valid.
Instance validity_equiv : Equiv (validity A) := λ x y,
109
  (valid x  valid y)  (valid x  validity_car x  validity_car y).
110
Instance validity_equivalence : Equivalence (@equiv (validity A) _).
111
112
Proof.
  split; unfold equiv, validity_equiv.
113
114
115
  - by intros [x px ?]; simpl.
  - intros [x px ?] [y py ?]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
116
    split; [|intros; trans y]; tauto.
117
Qed.
118
Canonical Structure validityC : ofeT := discreteC (validity A).
119

Robbert Krebbers's avatar
Robbert Krebbers committed
120
Instance dra_valid_proper' : Proper (() ==> iff) (valid : A  Prop).
121
122
Proof. by split; apply: dra_valid_proper. Qed.
Global Instance to_validity_proper : Proper (() ==> ()) to_validity.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
124
Instance: Proper (() ==> () ==> iff) (disjoint : relation A).
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
  intros x1 x2 Hx y1 y2 Hy; split.
127
128
  - by rewrite Hy (symmetry_iff () x1) (symmetry_iff () x2) Hx.
  - by rewrite -Hy (symmetry_iff () x2) (symmetry_iff () x1) -Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Qed.
130
131
132
133

Lemma dra_disjoint_rl a b c :  a   b   c  b  c  a  b  c  a  b.
Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
Lemma dra_disjoint_lr a b c :  a   b   c  a  b  a  b  c  b  c.
134
Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
135
136
Lemma dra_disjoint_move_r a b c :
   a   b   c  b  c  a  b  c  a  b  c.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Proof.
138
139
  intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
  apply dra_disjoint_move_l; auto; by rewrite dra_comm.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
142

143
Lemma validity_valid_car_valid z :  z   validity_car z.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
Program Instance validity_pcore : PCore (validity A) := λ x,
  Some (Validity (core (validity_car x)) ( x) _).
148
149
Solve Obligations with naive_solver eauto using dra_core_valid.
Program Instance validity_op : Op (validity A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  Validity (validity_car x  validity_car y)
Robbert Krebbers's avatar
Robbert Krebbers committed
151
           ( x   y  validity_car x  validity_car y) _.
152
Solve Obligations with naive_solver eauto using dra_op_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
153

154
Definition validity_ra_mixin : RAMixin (validity A).
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  apply ra_total_mixin; first eauto.
157
  - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
158
    split; intros (?&?&?); split_and!;
Robbert Krebbers's avatar
Robbert Krebbers committed
159
      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
160
161
162
  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
  - intros ?? [??]; naive_solver.
  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
Robbert Krebbers's avatar
Robbert Krebbers committed
163
      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
164
      |intros; by rewrite assoc].
165
166
  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
  - intros [x px ?]; split;
Ralf Jung's avatar
Ralf Jung committed
167
168
      naive_solver eauto using dra_core_l, dra_core_disjoint_l.
  - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
170
    destruct (dra_core_mono x z) as (z'&Hz').
171
    unshelve eexists (Validity z' (px  py  pz) _).
Robbert Krebbers's avatar
Robbert Krebbers committed
172
    { intros (?&?&?); apply Hz'; tauto. }
173
174
    split; simpl; first tauto.
    intros. rewrite Hy //. tauto.
175
  - by intros [x px ?] [y py ?] (?&?&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Qed.
177
178
Canonical Structure validityR : cmraT :=
  discreteR (validity A) validity_ra_mixin.
179

180
Global Instance validity_disrete_cmra : CmraDiscrete validityR.
181
Proof. apply discrete_cmra_discrete. Qed.
182
183
Global Instance validity_cmra_total : CmraTotal validityR.
Proof. rewrite /CmraTotal; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
184

185
186
Lemma validity_update x y :
  ( c,  x   c  validity_car x  c   y  validity_car y  c)  x ~~> y.
Robbert Krebbers's avatar
Robbert Krebbers committed
187
Proof.
188
189
  intros Hxy; apply cmra_discrete_update=> z [?[??]].
  split_and!; try eapply Hxy; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Qed.
191

192
193
194
195
Lemma to_validity_op a b :
  ( (a  b)   a   b  a  b) 
  to_validity (a  b)  to_validity a  to_validity b.
Proof. split; naive_solver eauto using dra_op_valid. Qed.
196

197
(* TODO: This has to be proven again. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
198
(*
199
200
201
202
203
Lemma to_validity_included x y:
  (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
Proof.
  split.
  - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
    destruct Hvl' as [? [? ?]]; split; first done.
    exists (validity_car z); eauto.
206
  - intros (Hvl & z & EQ & ? & ?).
Robbert Krebbers's avatar
Robbert Krebbers committed
207
    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
208
    split; first done. exists (to_validity z). split; first split.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
    + intros _. simpl. by split_and!.
210
211
212
    + intros _. setoid_subst. by apply dra_op_valid. 
    + intros _. rewrite /= EQ //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
214
End dra.