logic.v 18.1 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
Require Import cmra cofe_instances.
Local Hint Extern 1 (_  _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_  _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_  _) => omega.

Structure iProp (A : cmraT) : Type := IProp {
  iprop_holds :> nat  A -> Prop;
  iprop_ne x1 x2 n : iprop_holds n x1  x1 ={n}= x2  iprop_holds n x2;
  iprop_weaken x1 x2 n1 n2 :
    x1  x2  n2  n1  validN n2 x2  iprop_holds n1 x1  iprop_holds n2 x2
}.
Add Printing Constructor iProp.
Instance: Params (@iprop_holds) 3.

Instance iprop_equiv (A : cmraT) : Equiv (iProp A) := λ P Q,  x n,
  validN n x  P n x  Q n x.
Instance iprop_dist (A : cmraT) : Dist (iProp A) := λ n P Q,  x n',
  n' < n  validN n' x  P n' x  Q n' x.
Program Instance iprop_compl (A : cmraT) : Compl (iProp A) := λ c,
  {| iprop_holds n x := c (S n) n x |}.
Next Obligation. by intros A c x y n ??; simpl in *; apply iprop_ne with x. Qed.
Next Obligation.
  intros A c x1 x2 n1 n2 ????; simpl in *.
  apply (chain_cauchy c (S n2) (S n1)); eauto using iprop_weaken, cmra_valid_le.
Qed.
Instance iprop_cofe (A : cmraT) : Cofe (iProp A).
Proof.
  split.
  * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
    intros HPQ x n ?; apply HPQ with (S n); auto.
  * 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.
  * intros P Q x i ??; lia.
  * intros c n x i ??; apply (chain_cauchy c (S i) n); auto.
Qed.
Instance iprop_holds_ne {A} (P : iProp A) n : Proper (dist n ==> iff) (P n).
Proof. intros x1 x2 Hx; split; eauto using iprop_ne. Qed.
Instance iprop_holds_proper {A} (P : iProp A) n : Proper (() ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply iprop_holds_ne, equiv_dist. Qed.
Definition iPropC (A : cmraT) : cofeT := CofeT (iProp A).

(** functor *)
Program Definition iProp_map {A B : cmraT} (f: B -n> A) `{!CMRAPreserving f}
  (P : iProp A) : iProp B := {| iprop_holds n x := P n (f x) |}.
Next Obligation. by intros A B f ? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
Next Obligation.
  by intros A B f ? P y1 y2 n i ???; simpl; apply iprop_weaken; auto;
    apply validN_preserving || apply included_preserving.
Qed.

(** logical entailement *)
Instance iprop_entails {A} : SubsetEq (iProp A) := λ P Q,  x n,
  validN n x  P n x  Q n x.

(** logical connectives *)
Program Definition iprop_const {A} (P : Prop) : iProp A :=
  {| iprop_holds n x := P |}.
Solve Obligations with done.

Program Definition iprop_and {A} (P Q : iProp A) : iProp A :=
  {| iprop_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
Program Definition iprop_or {A} (P Q : iProp A) : iProp A :=
  {| iprop_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
Program Definition iprop_impl {A} (P Q : iProp A) : iProp A :=
  {| iprop_holds n x :=  x' n',
       x  x'  n'  n  validN n' x'  P n' x'  Q n' x' |}.
Next Obligation.
  intros A P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
  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'.
  by apply HPQ, iprop_weaken with x2' n2, iprop_ne with x2.
Qed.
Next Obligation. naive_solver eauto 2 with lia. Qed.

Program Definition iprop_forall {A B} (P : A  iProp B) : iProp B :=
  {| iprop_holds n x :=  a, P a n x |}.
Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
Program Definition iprop_exist {A B} (P : A  iProp B) : iProp B :=
  {| iprop_holds n x :=  a, P a n x |}.
Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.

Program Definition iprop_eq {A} {B : cofeT} (b1 b2 : B) : iProp A :=
  {| iprop_holds n x := b1 ={n}= b2 |}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=B)).

Program Definition iprop_sep {A} (P Q : iProp A) : iProp A :=
  {| iprop_holds n x :=  x1 x2, x ={n}= x1  x2  P n x1  Q n x2 |}.
Next Obligation.
95
  by intros A P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite <-Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
98
99
100
101
102
Qed.
Next Obligation.
  intros A P Q x y n1 n2 Hxy ?? (x1&x2&Hx&?&?).
  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. }
103
  exists x1, x2'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
  * apply iprop_weaken with x1 n1; auto.
    by apply cmra_valid_op_l with x2'; rewrite <-Hy.
  * apply iprop_weaken with x2 n1; auto.
    by apply cmra_valid_op_r with x1; rewrite <-Hy.
Qed.

Program Definition iprop_wand {A} (P Q : iProp A) : iProp A :=
  {| iprop_holds n x :=  x' n',
       n'  n  validN n' (x  x')  P n' x'  Q n' (x  x') |}.
Next Obligation.
  intros A P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
  rewrite <-(dist_le _ _ _ _ Hx) by done; apply HPQ; auto.
  by rewrite (dist_le _ _ _ n2 Hx).
Qed.
Next Obligation.
  intros A P Q x1 x2 n1 n2 ??? HPQ x3 n3 ???; simpl in *.
  apply iprop_weaken with (x1  x3) n3; auto using ra_preserving_r.
  apply HPQ; auto.
  apply cmra_valid_included with (x2  x3); auto using ra_preserving_r.
Qed.

Program Definition iprop_later {A} (P : iProp A) : iProp A :=
  {| iprop_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Next Obligation. intros A P ?? [|n]; eauto using iprop_ne,(dist_le (A:=A)). Qed.
Next Obligation.
  intros A P x1 x2 [|n1] [|n2] ????; auto with lia.
  apply iprop_weaken with x1 n1; eauto using cmra_valid_S.
Qed.
Program Definition iprop_always {A} (P : iProp A) : iProp A :=
  {| iprop_holds n x := P n (unit x) |}.
Next Obligation. by intros A P x1 x2 n ? Hx; simpl in *; rewrite <-Hx. Qed.
Next Obligation.
  intros A P x1 x2 n1 n2 ????; eapply iprop_weaken with (unit x1) n1;
    auto using ra_unit_preserving, cmra_unit_valid.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
142
143
144
145
146
147
148
149
150
Program Definition iprop_own {A : cmraT} (a : A) : iProp A :=
  {| iprop_holds n x :=  a', x ={n}= a  a' |}.
Next Obligation. by intros A a x1 x2 n [a' Hx] ?; exists a'; rewrite <-Hx. Qed.
Next Obligation.
  intros A a x1 x n1 n2; rewrite ra_included_spec; intros [x2 Hx] ?? [a' Hx1].
  exists (a'  x2). by rewrite (associative op), <-(dist_le _ _ _ _ Hx1), Hx.
Qed.
Program Definition iprop_valid {A : cmraT} (a : A) : iProp A :=
  {| iprop_holds n x := validN n a |}.
Solve Obligations with naive_solver eauto 2 using cmra_valid_le.

Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
Definition iprop_fixpoint {A} (P : iProp A  iProp A)
  `{!Contractive P} : iProp A := fixpoint P (iprop_const True).

Delimit Scope iprop_scope with I.
Bind Scope iprop_scope with iProp.
Arguments iprop_holds {_} _%I _ _.

Notation "'False'" := (iprop_const False) : iprop_scope.
Notation "'True'" := (iprop_const True) : iprop_scope.
Infix "∧" := iprop_and : iprop_scope.
Infix "∨" := iprop_or : iprop_scope.
Infix "→" := iprop_impl : iprop_scope.
Infix "★" := iprop_sep (at level 80, right associativity) : iprop_scope.
Infix "-★" := iprop_wand (at level 90) : iprop_scope.
Notation "∀ x .. y , P" :=
  (iprop_forall (λ x, .. (iprop_forall (λ y, P)) ..)) : iprop_scope.
Notation "∃ x .. y , P" :=
  (iprop_exist (λ x, .. (iprop_exist (λ y, P)) ..)) : iprop_scope.
Notation "▷ P" := (iprop_later P) (at level 20) : iprop_scope.
Notation "□ P" := (iprop_always P) (at level 20) : iprop_scope.

Section logic.
Context {A : cmraT}.
Implicit Types P Q : iProp A.

Global Instance iprop_preorder : PreOrder (() : relation (iProp A)).
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
Lemma iprop_equiv_spec P Q : P  Q  P  Q  Q  P.
Proof.
  split.
  * intros HPQ; split; intros x i; apply HPQ.
  * by intros [HPQ HQP]; intros x i ?; split; [apply HPQ|apply HQP].
Qed.

(** Non-expansiveness *)
Global Instance iprop_const_proper : Proper (iff ==> ()) (@iprop_const A).
Proof. intros P Q HPQ ???; apply HPQ. Qed.
Global Instance iprop_and_ne n :
  Proper (dist n ==> dist n ==> dist n) (@iprop_and A).
Proof.
  intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
Qed.
193
194
Global Instance iprop_and_proper :
  Proper (() ==> () ==> ()) (@iprop_and A) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196
197
198
199
200
Global Instance iprop_or_ne n :
  Proper (dist n ==> dist n ==> dist n) (@iprop_or A).
Proof.
  intros P P' HP Q Q' HQ; split; intros [?|?];
    first [by left; apply HP | by right; apply HQ].
Qed.
201
202
Global Instance iprop_or_proper :
  Proper (() ==> () ==> ()) (@iprop_or A) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
205
206
207
Global Instance iprop_impl_ne n :
  Proper (dist n ==> dist n ==> dist n) (@iprop_impl A).
Proof.
  intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
Qed.
208
209
Global Instance iprop_impl_proper :
  Proper (() ==> () ==> ()) (@iprop_impl A) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
212
213
Global Instance iprop_sep_ne n :
  Proper (dist n ==> dist n ==> dist n) (@iprop_sep A).
Proof.
  intros P P' HP Q Q' HQ x n' ? Hx'; split; intros (x1&x2&Hx&?&?);
214
    exists x1, x2; rewrite  Hx in Hx'; split_ands; try apply HP; try apply HQ;
Robbert Krebbers's avatar
Robbert Krebbers committed
215
216
    eauto using cmra_valid_op_l, cmra_valid_op_r.
Qed.
217
218
Global Instance iprop_sep_proper :
  Proper (() ==> () ==> ()) (@iprop_sep A) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
221
222
223
224
Global Instance iprop_wand_ne n :
  Proper (dist n ==> dist n ==> dist n) (@iprop_wand A).
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.
225
226
Global Instance iprop_wand_proper :
  Proper (() ==> () ==> ()) (@iprop_wand A) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
230
231
232
233
Global Instance iprop_eq_ne {B : cofeT} n :
  Proper (dist n ==> dist n ==> dist n) (@iprop_eq A B).
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.
234
235
Global Instance iprop_eq_proper {B : cofeT} :
  Proper (() ==> () ==> ()) (@iprop_eq A B) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
Global Instance iprop_forall_ne {B : cofeT} :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_forall B A).
Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
239
240
241
Global Instance iprop_forall_proper {B : cofeT} :
  Proper (pointwise_relation _ () ==> ()) (@iprop_forall B A).
Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
243
244
245
246
Global Instance iprop_exists_ne {B : cofeT} :
  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_exist B A).
Proof.
  by intros n P1 P2 HP12 x n'; split; intros [a HP]; exists a; apply HP12.
Qed.
247
248
249
250
251
Global Instance iprop_exist_proper {B : cofeT} :
  Proper (pointwise_relation _ () ==> ()) (@iprop_exist B A).
Proof.
  by intros P1 P2 HP12 x n'; split; intros [a HP]; exists a; apply HP12.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295

(** Introduction and elimination rules *)
Lemma iprop_True_intro P : P  True%I.
Proof. done. Qed.
Lemma iprop_False_elim P : False%I  P.
Proof. by intros x n ?. Qed.
Lemma iprop_and_elim_l P Q : (P  Q)%I  P.
Proof. by intros x n ? [??]. Qed.
Lemma iprop_and_elim_r P Q : (P  Q)%I  Q.
Proof. by intros x n ? [??]. Qed.
Lemma iprop_and_intro R P Q : R  P  R  Q  R  (P  Q)%I.
Proof. intros HP HQ x n ??; split. by apply HP. by apply HQ. Qed.
Lemma iprop_or_intro_l P Q : P  (P  Q)%I.
Proof. by left. Qed.
Lemma iprop_or_intro_r P Q : Q  (P  Q)%I.
Proof. by right. Qed.
Lemma iprop_or_elim R P Q : P  R  Q  R  (P  Q)%I  R.
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
Lemma iprop_impl_intro P Q R : (R  P)%I  Q  R  (P  Q)%I.
Proof.
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using iprop_weaken.
Qed.
Lemma iprop_impl_elim P Q : ((P  Q)  P)%I  Q.
Proof. by intros x n ? [HQ HP]; apply HQ. Qed.
Lemma iprop_forall_intro P `(Q: B  iProp A): ( b, P  Q b)  P  ( b, Q b)%I.
Proof. by intros HPQ x n ?? b; apply HPQ. Qed.
Lemma iprop_forall_elim `(P : B  iProp A) b : ( b, P b)%I  P b.
Proof. intros x n ? HP; apply HP. Qed.
Lemma iprop_exist_intro `(P : B  iProp A) b : P b  ( b, P b)%I.
Proof. by intros x n ??; exists b. Qed.
Lemma iprop_exist_elim `(P : B  iProp A) Q : ( b, P b  Q)  ( b, P b)%I  Q.
Proof. by intros HPQ x n ? [b ?]; apply HPQ with b. Qed.

(* BI connectives *)
Lemma iprop_sep_elim_l P Q : (P  Q)%I  P.
Proof.
  intros x n Hvalid (x1&x2&Hx&?&?); rewrite Hx in Hvalid |- *.
  by apply iprop_weaken with x1 n; auto using ra_included_l.
Qed.
Global Instance iprop_sep_left_id : LeftId () True%I (@iprop_sep A).
Proof.
  intros P x n Hvalid; split.
  * intros (x1&x2&Hx&_&?); rewrite Hx in Hvalid |- *.
    apply iprop_weaken with x2 n; auto using ra_included_r.
296
  * by intros ?; exists (unit x), x; rewrite ra_unit_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
298
299
300
Qed. 
Global Instance iprop_sep_commutative : Commutative () (@iprop_sep A).
Proof.
  by intros P Q x n ?; split;
301
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
304
305
Qed.
Global Instance iprop_sep_associative : Associative () (@iprop_sep A).
Proof.
  intros P Q R x n ?; split.
306
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
    + by rewrite <-(associative op), <-Hy, <-Hx.
308
309
    + 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
310
    + by rewrite (associative op), <-Hy, <-Hx.
311
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
312
313
314
315
Qed.
Lemma iprop_wand_intro P Q R : (R  P)%I  Q  R  (P - Q)%I.
Proof.
  intros HPQ x n ?? x' n' ???; apply HPQ; auto.
316
  exists x, x'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
317
318
319
320
321
322
323
324
  eapply iprop_weaken with x n; eauto using cmra_valid_op_l.
Qed.
Lemma iprop_wand_elim P Q : ((P - Q)  P)%I  Q.
Proof.
  by intros x n Hvalid (x1&x2&Hx&HPQ&?); rewrite Hx in Hvalid |- *; apply HPQ.
Qed.
Lemma iprop_sep_or P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
Proof.
325
326
  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
327
328
329
    first [by left | by right | done].
Qed.
Lemma iprop_sep_and P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
330
Proof. by intros x n ? (x1&x2&Hx&[??]&?); split; exists x1, x2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
333
Lemma iprop_sep_exist {B} (P : B  iProp A) Q :
  (( b, P b)  Q)%I  ( b, P b  Q)%I.
Proof.
334
335
  split; [by intros (x1&x2&Hx&[b ?]&?); exists b, x1, x2|].
  intros [b (x1&x2&Hx&?&?)]; exists x1, x2; split_ands; by try exists b.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
337
338
Qed.
Lemma iprop_sep_forall `(P : B  iProp A) Q :
  (( b, P b)  Q)%I  ( b, P b  Q)%I.
339
Proof. by intros x n ? (x1&x2&Hx&?&?); intros b; exists x1, x2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378

(* Later *)
Global Instance iprop_later_contractive : Contractive (@iprop_later A).
Proof.
  intros n P Q HPQ x [|n'] ??; simpl; [done|].
  apply HPQ; eauto using cmra_valid_S.
Qed.
Lemma iprop_later_weaken P : P  ( P)%I.
Proof.
  intros x [|n] ??; simpl in *; [done|].
  apply iprop_weaken with x (S n); auto using cmra_valid_S.
Qed.
Lemma iprop_lub P : ( P  P)%I  P.
Proof.
  intros x n ? HP; induction n as [|n IH]; [by apply HP|].
  apply HP, IH, iprop_weaken with x (S n); eauto using cmra_valid_S.
Qed.
Lemma iprop_later_impl P Q : ( (P  Q))%I  ( P   Q)%I.
Proof.
  intros x [|n] ? HPQ x' [|n'] ???; auto with lia.
  apply HPQ; auto using cmra_valid_S.
Qed.
Lemma iprop_later_and P Q : ( (P  Q))%I  ( P   Q)%I.
Proof. by intros x [|n]; split. Qed.
Lemma iprop_later_or P Q : ( (P  Q))%I  ( P   Q)%I.
Proof. intros x [|n]; simpl; tauto. Qed.
Lemma iprop_later_forall `(P : B  iProp A) : (  b, P b)%I  ( b,  P b)%I.
Proof. by intros x [|n]. Qed.
Lemma iprop_later_exist `(P : B  iProp A) : ( b,  P b)%I  (  b, P b)%I.
Proof. by intros x [|n]. Qed.
Lemma iprop_later_exist' `{Inhabited B} (P : B  iProp A) :
  (  b, P b)%I  ( b,  P b)%I.
Proof.
  intros x [|n]; split; try done.
  by destruct (_ : Inhabited B) as [b]; exists b.
Qed.
Lemma iprop_later_sep P Q : ( (P  Q))%I  ( P   Q)%I.
Proof.
  intros x n ?; split.
379
  * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
Robbert Krebbers's avatar
Robbert Krebbers committed
380
381
    destruct (cmra_extend_op x x1 x2 n)
      as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
382
    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
Robbert Krebbers's avatar
Robbert Krebbers committed
383
  * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
384
    exists x1, x2; eauto using (dist_S (A:=A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
Qed.

(* Always *)
Lemma iprop_always_necessity P : ( P)%I  P.
Proof.
  intros x n ??; apply iprop_weaken with (unit x) n;auto using ra_included_unit.
Qed.
Lemma iprop_always_intro P Q : ( P)%I  Q  ( P)%I  ( Q)%I.
Proof.
  intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_valid.
  by rewrite ra_unit_idempotent.
Qed.
Lemma iprop_always_impl P Q : ( (P  Q))%I  (P  Q)%I.
Proof.
  intros x n ? HPQ x' n' ???.
  apply HPQ; auto using ra_unit_preserving, cmra_unit_valid.
Qed.
Lemma iprop_always_and P Q : ( (P  Q))%I  ( P   Q)%I.
Proof. done. Qed.
Lemma iprop_always_or P Q : ( (P  Q))%I  ( P   Q)%I.
Proof. done. Qed.
Lemma iprop_always_forall `(P : B  iProp A) : (  b, P b)%I  ( b,  P b)%I.
Proof. done. Qed.
Lemma iprop_always_exist `(P : B  iProp A) : (  b, P b)%I  ( b,  P b)%I.
Proof. done. Qed.
Lemma iprop_always_and_always_box P Q : ( P  Q)%I  ( P  Q)%I.
Proof.
412
  intros x n ? [??]; exists (unit x), x; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
414
415
  by rewrite ra_unit_l, ra_unit_idempotent.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
(* Own *)
Lemma iprop_own_op (a1 a2 : A) :
  iprop_own (a1  a2)  (iprop_own a1  iprop_own a2)%I.
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.
Lemma iprop_own_valid (a : A) : iprop_own a  iprop_valid a.
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
432
433
434
435
436
(* Fix *)
Lemma iprop_fixpoint_unfold (P : iProp A  iProp A) `{!Contractive P} :
  iprop_fixpoint P  P (iprop_fixpoint P).
Proof. apply fixpoint_unfold. Qed.
End logic.