logic.v 20.6 KB
Newer Older
1
Require Import iris.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
Local Hint Extern 1 (_  _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_  _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_  _) => omega.

Robbert Krebbers's avatar
Robbert Krebbers committed
6
Structure uPred (M : cmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  uPred_ne x1 x2 n : uPred_holds n x1  x1 ={n}= x2  uPred_holds n x2;
9
  uPred_0 x : uPred_holds 0 x;
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
  uPred_weaken x1 x2 n1 n2 :
    x1  x2  n2  n1  validN n2 x2  uPred_holds n1 x1  uPred_holds n2 x2
Robbert Krebbers's avatar
Robbert Krebbers committed
12
}.
13
14
Arguments uPred_holds {_} _ _ _.
Hint Resolve uPred_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

Robbert Krebbers's avatar
Robbert Krebbers committed
18
Instance uPred_equiv (M : cmraT) : Equiv (uPred M) := λ P Q,  x n,
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  validN n x  P n x  Q n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Instance uPred_dist (M : cmraT) : Dist (uPred M) := λ n P Q,  x n',
21
  n'  n  validN n' x  P n' x  Q n' x.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Program Instance uPred_compl (M : cmraT) : Compl (uPred M) := λ c,
23
  {| uPred_holds n x := c n n x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
Next Obligation. by intros M c x y n ??; simpl in *; apply uPred_ne with x. Qed.
25
Next Obligation. by intros M c x; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Next Obligation.
27
  intros M c x1 x2 n1 n2 ????; simpl in *.
28
  apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Instance uPred_cofe (M : cmraT) : Cofe (uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
Proof.
  split.
  * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
34
    intros HPQ x n ?; apply HPQ with n; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
39
  * intros n; split.
    + by intros P x i.
    + by intros P Q HPQ x i ??; symmetry; apply HPQ.
    + by intros P Q Q' HP HQ x i ??; transitivity (Q i x); [apply HP|apply HQ].
  * intros n P Q HPQ x i ??; apply HPQ; auto.
40
41
  * intros P Q x i; rewrite Nat.le_0_r; intros ->; split; intros; apply uPred_0.
  * by intros c n x i ??; apply (chain_cauchy c i n).
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
47
Instance uPred_holds_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
Instance uPred_holds_proper {M} (P : uPred M) n : Proper (() ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_holds_ne, equiv_dist. Qed.
Definition uPredC (M : cmraT) : cofeT := CofeT (uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49

(** functor *)
Robbert Krebbers's avatar
Robbert Krebbers committed
50
Program Definition uPred_map {M1 M2 : cmraT} (f : M2  M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  `{! n, Proper (dist n ==> dist n) f, !CMRAPreserving f}
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
53
Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
54
Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  by intros M1 M2 f ?? P y1 y2 n i ???; simpl; apply uPred_weaken; auto;
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
    apply validN_preserving || apply included_preserving.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2  M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  `{! n, Proper (dist n ==> dist n) f, !CMRAPreserving f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  Proper (dist n ==> dist n) (uPred_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
Proof.
  by intros n x1 x2 Hx y n'; split; apply Hx; try apply validN_preserving.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAPreserving f} :
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
70
71
72
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
    `{!CMRAPreserving f, !CMRAPreserving g} n :
  f ={n}= g  uPredC_map f ={n}= uPredC_map g.
Proof.
  by intros Hfg P y n' ??; simpl; rewrite (dist_le _ _ _ _(Hfg y)) by lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74

(** logical entailement *)
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q,  x n,
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
78
  validN n x  P n x  Q n x.

(** logical connectives *)
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Program Definition uPred_const {M} (P : Prop) : uPred M :=
80
  {| uPred_holds n x := match n return _ with 0 => True | _ => P end |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Solve Obligations with done.
82
Next Obligation. intros M P x1 x2 [|n1] [|n2]; auto with lia. Qed.
83
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
84

Robbert Krebbers's avatar
Robbert Krebbers committed
85
86
87
88
89
90
91
92
Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_or {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_impl {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
       x  x'  n'  n  validN n' x'  P n' x'  Q n' x' |}.
Next Obligation.
95
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
98
  destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto.
  assert (x2' ={n2}= x2) as Hx2' by (by apply dist_le with n1).
  assert (validN n2 x2') by (by rewrite Hx2'); rewrite <-Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  by apply HPQ, uPred_weaken with x2' n2, uPred_ne with x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Qed.
101
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
Next Obligation. naive_solver eauto 2 with lia. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
Program Definition uPred_forall {M A} (P : A  uPred M) : uPred M :=
  {| uPred_holds n x :=  a, P a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_exist {M A} (P : A  uPred M) : uPred M :=
108
109
110
111
112
113
114
  {| uPred_holds n x :=
       match n return _ with 0 => True | _ =>  a, P a n x end |}.
Next Obligation. intros M A P x y [|n]; naive_solver eauto using uPred_ne. Qed.
Next Obligation. done. Qed.
Next Obligation.
  intros M A P x y [|n] [|n']; naive_solver eauto 2 using uPred_weaken with lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
115

Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
  {| uPred_holds n x := a1 ={n}= a2 |}.
118
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
119

Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x1 x2, x ={n}= x1  x2  P n x1  Q n x2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Next Obligation.
123
  by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite <-Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Qed.
125
Next Obligation. by intros M P Q x; exists x, x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Next Obligation.
127
  intros M P Q x y n1 n2 Hxy ?? (x1&x2&Hx&?&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
131
  assert ( x2', y ={n2}= x1  x2'  x2  x2') as (x2'&Hy&?).
  { rewrite ra_included_spec in Hxy; destruct Hxy as [z Hy].
    exists (x2  z); split; eauto using ra_included_l.
    apply dist_le with n1; auto. by rewrite (associative op), <-Hx, Hy. }
132
  exists x1, x2'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  * apply uPred_weaken with x1 n1; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
    by apply cmra_valid_op_l with x2'; rewrite <-Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  * apply uPred_weaken with x2 n1; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
    by apply cmra_valid_op_r with x1; rewrite <-Hy.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
       n'  n  validN n' (x  x')  P n' x'  Q n' (x  x') |}.
Next Obligation.
143
  intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
146
  rewrite <-(dist_le _ _ _ _ Hx) by done; apply HPQ; auto.
  by rewrite (dist_le _ _ _ n2 Hx).
Qed.
147
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Next Obligation.
149
  intros M P Q x1 x2 n1 n2 ??? HPQ x3 n3 ???; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
  apply uPred_weaken with (x1  x3) n3; auto using ra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
153
154
  apply HPQ; auto.
  apply cmra_valid_included with (x2  x3); auto using ra_preserving_r.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
Program Definition uPred_later {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Next Obligation. intros M P ?? [|n]; eauto using uPred_ne,(dist_le (A:=M)). Qed.
158
Next Obligation. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
159
Next Obligation.
160
  intros M P x1 x2 [|n1] [|n2] ????; auto with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  apply uPred_weaken with x1 n1; eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (unit x) |}.
165
Next Obligation. by intros M P x1 x2 n ? Hx; simpl in *; rewrite <-Hx. Qed.
166
Next Obligation. by intros; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
    auto using ra_unit_preserving, cmra_unit_valid.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
  {| uPred_holds n x :=  a', x ={n}= a  a' |}.
174
Next Obligation. by intros M a x1 x2 n [a' Hx] ?; exists a'; rewrite <-Hx. Qed.
175
Next Obligation. by intros M a x; exists x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Next Obligation.
177
  intros M a x1 x n1 n2; rewrite ra_included_spec; intros [x2 Hx] ?? [a' Hx1].
Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
  exists (a'  x2). by rewrite (associative op), <-(dist_le _ _ _ _ Hx1), Hx.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
Program Definition uPred_valid {M : cmraT} (a : M) : uPred M :=
  {| uPred_holds n x := validN n a |}.
182
Solve Obligations with naive_solver eauto 2 using cmra_valid_le, cmra_valid_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
183

Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
186
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
187

Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
190
191
192
193
194
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
Infix "∨" := uPred_or : uPred_scope.
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
Infix "-★" := uPred_wand (at level 90) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
Notation "∀ x .. y , P" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
196
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Notation "∃ x .. y , P" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : uPred_scope.
Notation "▷ P" := (uPred_later P) (at level 20) : uPred_scope.
Notation "□ P" := (uPred_always P) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203

Section logic.
204
Context {M : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Implicit Types P Q : uPred M.
Robbert Krebbers's avatar
Robbert Krebbers committed
206

Robbert Krebbers's avatar
Robbert Krebbers committed
207
Global Instance uPred_preorder : PreOrder (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
208
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
Lemma uPred_equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
212
213
214
Proof.
  split.
  * intros HPQ; split; intros x i; apply HPQ.
  * by intros [HPQ HQP]; intros x i ?; split; [apply HPQ|apply HQP].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
216
217
218
219
220
221
Global Instance uPred_entails_proper :
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Proof.
  intros P1 P2 HP Q1 Q2 HQ; rewrite uPred_equiv_spec in HP, HQ; split; intros.
  * by rewrite (proj2 HP), <-(proj1 HQ).
  * by rewrite (proj1 HP), <-(proj2 HQ).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223

(** Non-expansiveness *)
Robbert Krebbers's avatar
Robbert Krebbers committed
224
Global Instance uPred_const_proper : Proper (iff ==> ()) (@uPred_const M).
225
Proof. by intros P Q HPQ ? [|n] ?; try apply HPQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
Global Instance uPred_and_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
230
Proof.
  intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
232
233
234
Global Instance uPred_and_proper :
  Proper (() ==> () ==> ()) (@uPred_and M) := ne_proper_2 _.
Global Instance uPred_or_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
237
238
Proof.
  intros P P' HP Q Q' HQ; split; intros [?|?];
    first [by left; apply HP | by right; apply HQ].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
241
242
Global Instance uPred_or_proper :
  Proper (() ==> () ==> ()) (@uPred_or M) := ne_proper_2 _.
Global Instance uPred_impl_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
243
244
245
Proof.
  intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
247
248
249
Global Instance uPred_impl_proper :
  Proper (() ==> () ==> ()) (@uPred_impl M) := ne_proper_2 _.
Global Instance uPred_sep_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
250
251
Proof.
  intros P P' HP Q Q' HQ x n' ? Hx'; split; intros (x1&x2&Hx&?&?);
252
    exists x1, x2; rewrite  Hx in Hx'; split_ands; try apply HP; try apply HQ;
Robbert Krebbers's avatar
Robbert Krebbers committed
253
254
    eauto using cmra_valid_op_l, cmra_valid_op_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
256
257
258
Global Instance uPred_sep_proper :
  Proper (() ==> () ==> ()) (@uPred_sep M) := ne_proper_2 _.
Global Instance uPred_wand_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
261
262
Proof.
  intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
    apply HQ, HPQ, HP; eauto using cmra_valid_op_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
264
265
266
Global Instance uPred_wand_proper :
  Proper (() ==> () ==> ()) (@uPred_wand M) := ne_proper_2 _.
Global Instance uPred_eq_ne {A : cofeT} n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
267
268
269
270
271
Proof.
  intros x x' Hx y y' Hy z n'; split; intros; simpl in *.
  * by rewrite <-(dist_le _ _ _ _ Hx), <-(dist_le _ _ _ _ Hy) by auto.
  * by rewrite (dist_le _ _ _ _ Hx), (dist_le _ _ _ _ Hy) by auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
273
274
275
Global Instance uPred_eq_proper {A : cofeT} :
  Proper (() ==> () ==> ()) (@uPred_eq M A) := ne_proper_2 _.
Global Instance uPred_forall_ne {A : cofeT} :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
276
Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
278
Global Instance uPred_forall_proper {A : cofeT} :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
279
Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
281
Global Instance uPred_exists_ne {A : cofeT} :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
282
Proof.
283
  by intros n P1 P2 HP x [|n']; [|split; intros [a ?]; exists a; apply HP].
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
286
Global Instance uPred_exist_proper {A : cofeT} :
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
287
Proof.
288
  by intros P1 P2 HP x [|n']; [|split; intros [a ?]; exists a; apply HP].
289
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
Global Instance uPred_later_contractive : Contractive (@uPred_later M).
Robbert Krebbers's avatar
Robbert Krebbers committed
291
292
293
294
Proof.
  intros n P Q HPQ x [|n'] ??; simpl; [done|].
  apply HPQ; eauto using cmra_valid_S.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
296
297
Global Instance uPred_later_proper :
  Proper (() ==> ()) (@uPred_later M) := ne_proper _.
Global Instance uPred_always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
300
301
Global Instance uPred_always_proper :
  Proper (() ==> ()) (@uPred_always M) := ne_proper _.
Global Instance uPred_own_ne n : Proper (dist n ==> dist n) (@uPred_own M).
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
304
305
Proof.
  by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first
    [rewrite <-(dist_le _ _ _ _ Ha) by lia|rewrite (dist_le _ _ _ _ Ha) by lia].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
Global Instance uPred_own_proper :
  Proper (() ==> ()) (@uPred_own M) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
309

(** Introduction and elimination rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
310
Lemma uPred_const_intro P (Q : Prop) : Q  P  uPred_const Q.
311
Proof. by intros ?? [|?]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
312
Lemma uPred_True_intro P : P  True%I.
313
Proof. by apply uPred_const_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
314
Lemma uPred_False_elim P : False%I  P.
315
Proof. by intros x [|n] ?. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
Lemma uPred_and_elim_l P Q : (P  Q)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
Proof. by intros x n ? [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
Lemma uPred_and_elim_r P Q : (P  Q)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
Proof. by intros x n ? [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
Lemma uPred_and_intro R P Q : R  P  R  Q  R  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
Proof. intros HP HQ x n ??; split. by apply HP. by apply HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
322
Lemma uPred_or_intro_l P Q : P  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
Proof. by left. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
Lemma uPred_or_intro_r P Q : Q  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
325
Proof. by right. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
Lemma uPred_or_elim R P Q : P  R  Q  R  (P  Q)%I  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Lemma uPred_impl_intro P Q R : (R  P)%I  Q  R  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
330
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
332
Lemma uPred_impl_elim P Q : ((P  Q)  P)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
333
Proof. by intros x n ? [HQ HP]; apply HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Lemma uPred_forall_intro P `(Q: A  uPred M): ( a, P  Q a)  P  ( a, Q a)%I.
335
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
Lemma uPred_forall_elim `(P : A  uPred M) a : ( a, P a)%I  P a.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
Proof. intros x n ? HP; apply HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Lemma uPred_exist_intro `(P : A  uPred M) a : P a  ( a, P a)%I.
339
Proof. by intros x [|n] ??; [done|exists a]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Lemma uPred_exist_elim `(P : A  uPred M) Q : ( a, P a  Q)  ( a, P a)%I  Q.
341
Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
343

(* BI connectives *)
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Lemma uPred_sep_elim_l P Q : (P  Q)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
346
Proof.
  intros x n Hvalid (x1&x2&Hx&?&?); rewrite Hx in Hvalid |- *.
Robbert Krebbers's avatar
Robbert Krebbers committed
347
  by apply uPred_weaken with x1 n; auto using ra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Global Instance uPred_sep_left_id : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
350
351
352
Proof.
  intros P x n Hvalid; split.
  * intros (x1&x2&Hx&_&?); rewrite Hx in Hvalid |- *.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
    apply uPred_weaken with x2 n; auto using ra_included_r.
354
  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Robbert Krebbers's avatar
Robbert Krebbers committed
355
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Global Instance uPred_sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
357
358
Proof.
  by intros P Q x n ?; split;
359
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
360
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
361
Global Instance uPred_sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
362
363
Proof.
  intros P Q R x n ?; split.
364
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
365
    + by rewrite <-(associative op), <-Hy, <-Hx.
366
367
    + by exists x1, y1.
  * intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2  x2); split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
368
    + by rewrite (associative op), <-Hy, <-Hx.
369
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
371
Lemma uPred_wand_intro P Q R : (R  P)%I  Q  R  (P - Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
373
Proof.
  intros HPQ x n ?? x' n' ???; apply HPQ; auto.
374
  exists x, x'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
375
  eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
377
Lemma uPred_wand_elim P Q : ((P - Q)  P)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
378
379
380
Proof.
  by intros x n Hvalid (x1&x2&Hx&HPQ&?); rewrite Hx in Hvalid |- *; apply HPQ.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
381
Lemma uPred_sep_or P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
Proof.
383
384
  split; [by intros (x1&x2&Hx&[?|?]&?); [left|right]; exists x1, x2|].
  intros [(x1&x2&Hx&?&?)|(x1&x2&Hx&?&?)]; exists x1, x2; split_ands;
Robbert Krebbers's avatar
Robbert Krebbers committed
385
386
    first [by left | by right | done].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
Lemma uPred_sep_and P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
388
Proof. by intros x n ? (x1&x2&Hx&[??]&?); split; exists x1, x2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
389
Lemma uPred_sep_exist `(P : A  uPred M) Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
390
391
  (( b, P b)  Q)%I  ( b, P b  Q)%I.
Proof.
392
  intros x [|n]; [done|split; [by intros (x1&x2&Hx&[a ?]&?); exists a,x1,x2|]].
393
  intros [a (x1&x2&Hx&?&?)]; exists x1, x2; split_ands; by try exists a.
Robbert Krebbers's avatar
Robbert Krebbers committed
394
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
Lemma uPred_sep_forall `(P : A  uPred M) Q :
396
397
  (( a, P a)  Q)%I  ( a, P a  Q)%I.
Proof. by intros x n ? (x1&x2&Hx&?&?); intros a; exists x1, x2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
398
399

(* Later *)
Robbert Krebbers's avatar
Robbert Krebbers committed
400
Lemma uPred_later_weaken P : P  ( P)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
402
Proof.
  intros x [|n] ??; simpl in *; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
403
  apply uPred_weaken with x (S n); auto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
Lemma uPred_lub P : ( P  P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
407
Proof.
  intros x n ? HP; induction n as [|n IH]; [by apply HP|].
Robbert Krebbers's avatar
Robbert Krebbers committed
408
  apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
409
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
Lemma uPred_later_impl P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
412
413
414
Proof.
  intros x [|n] ? HPQ x' [|n'] ???; auto with lia.
  apply HPQ; auto using cmra_valid_S.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
Lemma uPred_later_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
416
Proof. by intros x [|n]; split. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
417
Lemma uPred_later_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
Proof. intros x [|n]; simpl; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
419
Lemma uPred_later_forall `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
Proof. by intros x [|n]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Lemma uPred_later_exist `(P : A  uPred M) : ( a,  P a)%I  (  a, P a)%I.
422
Proof. by intros x [|[|n]]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
Lemma uPred_later_exist' `{Inhabited A} (P : A  uPred M) :
424
  (  a, P a)%I  ( a,  P a)%I.
425
Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
Lemma uPred_later_sep P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
428
Proof.
  intros x n ?; split.
429
  * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
Robbert Krebbers's avatar
Robbert Krebbers committed
430
431
    destruct (cmra_extend_op x x1 x2 n)
      as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
432
    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
Robbert Krebbers's avatar
Robbert Krebbers committed
433
  * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
434
    exists x1, x2; eauto using (dist_S (A:=M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
435
436
437
Qed.

(* Always *)
Robbert Krebbers's avatar
Robbert Krebbers committed
438
Lemma uPred_always_necessity P : ( P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
439
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
  intros x n ??; apply uPred_weaken with (unit x) n;auto using ra_included_unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
442
Lemma uPred_always_intro P Q : ( P)%I  Q  ( P)%I  ( Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
444
445
446
Proof.
  intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_valid.
  by rewrite ra_unit_idempotent.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
447
Lemma uPred_always_impl P Q : ( (P  Q))%I  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
449
450
451
Proof.
  intros x n ? HPQ x' n' ???.
  apply HPQ; auto using ra_unit_preserving, cmra_unit_valid.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
Lemma uPred_always_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
453
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
Lemma uPred_always_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
455
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
456
Lemma uPred_always_forall `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
458
Lemma uPred_always_exist `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
459
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
460
Lemma uPred_always_and_always_box P Q : ( P  Q)%I  ( P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
461
Proof.
462
  intros x n ? [??]; exists (unit x), x; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
465
  by rewrite ra_unit_l, ra_unit_idempotent.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
466
(* Own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
Lemma uPred_own_op (a1 a2 : M) :
  uPred_own (a1  a2)  (uPred_own a1  uPred_own a2)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
470
471
472
473
474
475
476
Proof.
  intros x n ?; split.
  * intros [z ?]; exists a1, (a2  z); split; [by rewrite (associative op)|].
    split. by exists (unit a1); rewrite ra_unit_r. by exists z.
  * intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1  z2).
    rewrite (associative op), <-(commutative op z1), <-!(associative op), <-Hy2.
    by rewrite (associative op), (commutative op z1), <-Hy1.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
Lemma uPred_own_valid (a : M) : uPred_own a  uPred_valid a.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
479
480
Proof.
  intros x n Hv [a' Hx]; simpl; rewrite Hx in Hv; eauto using cmra_valid_op_l.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
481
End logic.