logic.v 23.1 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
  uPred_weaken x1 x2 n1 n2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
11
    uPred_holds n1 x1  x1  x2  n2  n1  validN n2 x2  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
  naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2  M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  `{! n, Proper (dist n ==> dist n) f, !CMRAPreserving f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  Proper (dist n ==> dist n) (uPred_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
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
66
67
68
69
70
71
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
72
73

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
87
88
89
90
91
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
92
93
       x  x'  n'  n  validN n' x'  P n' x'  Q n' x' |}.
Next Obligation.
94
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
97
  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
98
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Qed.
100
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
Next Obligation. naive_solver eauto 2 with lia. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
106
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 :=
107
108
109
110
111
112
113
  {| 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
114

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

Robbert Krebbers's avatar
Robbert Krebbers committed
119
120
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
121
Next Obligation.
122
  by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite <-Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Qed.
124
Next Obligation. by intros M P Q x; exists x, x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
  intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ? Hvalid.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
130
  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. }
Robbert Krebbers's avatar
Robbert Krebbers committed
131
132
133
  rewrite Hy in Hvalid; exists x1, x2'; split_ands; auto.
  * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
  * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
135
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
153
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.
154
Next Obligation. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (unit x) |}.
160
Next Obligation. by intros M P x1 x2 n ? Hx; simpl in *; rewrite <-Hx. Qed.
161
Next Obligation. by intros; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
166
    auto using ra_unit_preserving, cmra_unit_valid.
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
181
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
182

Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
185
186
187
188
189
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
190
Notation "∀ x .. y , P" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
Notation "∃ x .. y , P" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
  (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
196
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
197

Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
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
200
Section logic.
201
Context {M : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
Implicit Types P Q : uPred M.
Robbert Krebbers's avatar
Robbert Krebbers committed
203

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
463
(* Own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
464
465
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
466
467
468
469
470
471
472
473
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
474
475
476
477
478
479
480
481
482
Lemma uPred_own_unit (a : M) : uPred_own (unit a)  ( uPred_own (unit a))%I.
Proof.
  intros x n; split; [intros [a' Hx]|by apply uPred_always_necessity].
  assert ( a'', unit (unit a  a')  unit (unit a)  a'') as [a'' Ha]
    by (rewrite <-ra_included_spec; auto using ra_unit_weaken).
  by exists a''; rewrite Hx, Ha, ra_unit_idempotent.
Qed.
Lemma uPred_own_empty `{Empty M, !RAEmpty M} : True%I  uPred_own .
Proof. intros x [|n] ??; [done|]. by  exists x; rewrite (left_id _ _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
Lemma uPred_own_valid (a : M) : uPred_own a  uPred_valid a.
Robbert Krebbers's avatar
Robbert Krebbers committed
484
485
486
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
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
531
532
533
534

(* 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
535
End logic.