logic.v 22.9 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

Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
Class TimelessP {M} (P : uPred M) := timelessP x n : validN 1 x  P 1 x  P n x.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
209
Global Instance uPred_preorder : PreOrder (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
210
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
211
Lemma uPred_equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
214
215
216
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
217
218
219
220
221
222
223
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
224
225

(** Non-expansiveness *)
Robbert Krebbers's avatar
Robbert Krebbers committed
226
Global Instance uPred_const_proper : Proper (iff ==> ()) (@uPred_const M).
227
Proof. by intros P Q HPQ ? [|n] ?; try apply HPQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
Global Instance uPred_and_ne n :
  Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
230
231
232
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
233
234
235
236
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
237
238
239
240
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
241
242
243
244
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
245
246
247
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
248
249
250
251
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
252
253
Proof.
  intros P P' HP Q Q' HQ x n' ? Hx'; split; intros (x1&x2&Hx&?&?);
254
    exists x1, x2; rewrite  Hx in Hx'; split_ands; try apply HP; try apply HQ;
Robbert Krebbers's avatar
Robbert Krebbers committed
255
256
    eauto using cmra_valid_op_l, cmra_valid_op_r.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
259
260
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
261
262
263
264
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
265
266
267
268
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
269
270
271
272
273
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
274
275
276
277
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
278
Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
280
Global Instance uPred_forall_proper {A : cofeT} :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
281
Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
283
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
284
Proof.
285
  by intros n P1 P2 HP x [|n']; [|split; intros [a ?]; exists a; apply HP].
Robbert Krebbers's avatar
Robbert Krebbers committed
286
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
Global Instance uPred_exist_proper {A : cofeT} :
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
289
Proof.
290
  by intros P1 P2 HP x [|n']; [|split; intros [a ?]; exists a; apply HP].
291
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
292
Global Instance uPred_later_contractive : Contractive (@uPred_later M).
Robbert Krebbers's avatar
Robbert Krebbers committed
293
294
295
296
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
297
298
299
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
300
Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_valid. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
303
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
304
305
306
307
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
308
309
Global Instance uPred_own_proper :
  Proper (() ==> ()) (@uPred_own M) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
311

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

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

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

(* Always *)
Robbert Krebbers's avatar
Robbert Krebbers committed
440
Lemma uPred_always_necessity P : ( P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
442
  intros x n ??; apply uPred_weaken with (unit x) n;auto using ra_included_unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
Lemma uPred_always_intro P Q : ( P)%I  Q  ( P)%I  ( Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
445
446
447
448
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
449
Lemma uPred_always_impl P Q : ( (P  Q))%I  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
450
451
452
453
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
454
Lemma uPred_always_and 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_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
458
Lemma uPred_always_forall `(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_exist `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
461
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
Lemma uPred_always_and_always_box P Q : ( P  Q)%I  ( P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
Proof.
464
  intros x n ? [??]; exists (unit x), x; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
465
466
467
  by rewrite ra_unit_l, ra_unit_idempotent.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
468
(* Own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
469
470
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
471
472
473
474
475
476
477
478
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
479
Lemma uPred_own_valid (a : M) : uPred_own a  uPred_valid a.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
481
482
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
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530

(* Timeless *)
Global Instance uPred_const_timeless (P : Prop) : TimelessP (@uPred_const M P).
Proof. by intros x [|n]. Qed.
Global Instance uPred_and_timeless P Q :
  TimelessP P  TimelessP Q  TimelessP (P  Q).
Proof. intros ?? x n ? [??]; split; auto. Qed.
Global Instance uPred_or_timeless P Q :
  TimelessP P  TimelessP Q  TimelessP (P  Q).
Proof. intros ?? x n ? [?|?]; [left|right]; auto. Qed.
Global Instance uPred_impl_timeless P Q : TimelessP Q  TimelessP (P  Q).
Proof.
  intros ? x [|n] ? HPQ x' [|n'] ????; auto.
  apply timelessP, HPQ, uPred_weaken with x' (S n'); eauto using cmra_valid_le.
Qed.
Global Instance uPred_sep_timeless P Q :
  TimelessP P  TimelessP Q  TimelessP (P  Q).
Proof.
  intros ?? x [|n] Hvalid (x1&x2&Hx12&?&?); [done|].
  destruct (cmra_extend_op x x1 x2 1) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *.
  rewrite Hx12 in Hvalid; exists y1, y2; split_ands; [by rewrite Hx| |].
  * apply timelessP; rewrite Hy1; eauto using cmra_valid_op_l.
  * apply timelessP; rewrite Hy2; eauto using cmra_valid_op_r.
Qed.
Global Instance uPred_wand_timeless P Q : TimelessP Q  TimelessP (P - Q).
Proof.
  intros ? x [|n] ? HPQ x' [|n'] ???; auto.
  apply timelessP, HPQ, uPred_weaken with x' (S n');
    eauto 3 using cmra_valid_le, cmra_valid_op_r.
Qed.
Global Instance uPred_forall_timeless {A} (P : A  uPred M) :
  ( x, TimelessP (P x))  TimelessP ( x, P x).
Proof. by intros ? x n ? HP a; apply timelessP. Qed.
Global Instance uPred_exist_timeless {A} (P : A  uPred M) :
  ( x, TimelessP (P x))  TimelessP ( x, P x).
Proof. by intros ? x [|n] ?; [|intros [a ?]; exists a; apply timelessP]. Qed.
Global Instance uPred_always_timeless P : TimelessP P  TimelessP ( P).
Proof. intros ? x n ??; simpl; apply timelessP; auto using cmra_unit_valid. Qed.
Global Instance uPred_eq_timeless {A : cofeT} (a b : A) :
  Timeless a  TimelessP (a  b : uPred M).
Proof. by intros ? x n ??; apply equiv_dist, timeless. Qed.
Global Instance uPred_own_timeless (a : M) :
  Timeless a  TimelessP (uPred_own a).
Proof.
  intros ? x n ? [a' ?].
  destruct (cmra_extend_op x a a' 1) as ([b b']&Hx&Hb&Hb'); auto; simpl in *.
  by exists b'; rewrite Hx, (timeless a b) by done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
End logic.