logic.v 32.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
  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
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.
47
Canonical Structure 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, !CMRAMonotone 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, !CMRAMonotone 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
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
67
    `{!CMRAMonotone f, !CMRAMonotone g} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
71
  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
  assert ( x2', y ={n2}= x1  x2'  x2  x2') as (x2'&Hy&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using ra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
    apply dist_le with n1; auto. by rewrite (associative op), <-Hx, Hy. }
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
132
  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
133
134
Qed.

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
185
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
Infix "∨" := uPred_or : uPred_scope.
187
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
190
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Infix "-★" := uPred_wand (at level 90) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
Notation "∀ x .. y , P" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
193
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
Notation "∃ x .. y , P" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196
197
  (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
198
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
199

200
201
202
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

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.
208
Implicit Types A : Type.
Robbert Krebbers's avatar
Robbert Krebbers committed
209

Robbert Krebbers's avatar
Robbert Krebbers committed
210
Global Instance uPred_preorder : PreOrder (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
211
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
212
213
Global Instance uPred_antisym : AntiSymmetric () (() : relation (uPred M)).
Proof. intros P Q HPQ HQP; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
Lemma uPred_equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Proof.
216
217
  split; [|by intros [??]; apply (anti_symmetric ())].
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
221
222
223
224
225
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
226

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

(** Introduction and elimination rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
319
Lemma uPred_const_intro P (Q : Prop) : Q  P  uPred_const Q.
320
Proof. by intros ?? [|?]. Qed.
321
322
Lemma uPred_const_elim (P : Prop) Q R : (P  Q  R)  (Q  uPred_const P)%I  R.
Proof. intros HR x [|n] ? [??]; [|apply HR]; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
Lemma uPred_True_intro P : P  True%I.
324
Proof. by apply uPred_const_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
325
Lemma uPred_False_elim P : False%I  P.
326
Proof. by intros x [|n] ?. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Lemma uPred_and_elim_l P Q : (P  Q)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Proof. by intros x n ? [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
Lemma uPred_and_elim_r P Q : (P  Q)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
330
Proof. by intros x n ? [??]. Qed.
331
332
333
334
335
336
Lemma uPred_and_intro P Q R : P  Q  P  R  P  (Q  R)%I.
Proof. intros HQ HR x n ??; split; auto. Qed.
Lemma uPred_or_intro_l P Q R : P  Q  P  (Q  R)%I.
Proof. intros HQ x n ??; left; auto. Qed.
Lemma uPred_or_intro_r P Q R : P  R  P  (Q  R)%I.
Proof. intros HR x n ??; right; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
Lemma uPred_or_elim R P Q : P  R  Q  R  (P  Q)%I  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
Lemma uPred_impl_intro P Q R : (R  P)%I  Q  R  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
Qed.
343
344
Lemma uPred_impl_elim P Q R : P  (Q  R)%I  P  Q  P  R.
Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
Lemma uPred_forall_intro P `(Q: A  uPred M): ( a, P  Q a)  P  ( a, Q a)%I.
346
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
347
Lemma uPred_forall_elim `(P : A  uPred M) a : ( a, P a)%I  P a.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Proof. intros x n ? HP; apply HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Lemma uPred_exist_intro `(P : A  uPred M) a : P a  ( a, P a)%I.
350
Proof. by intros x [|n] ??; [done|exists a]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
Lemma uPred_exist_elim `(P : A  uPred M) Q : ( a, P a  Q)  ( a, P a)%I  Q.
352
Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
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
379
380
381
382
383
384
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
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
Lemma uPred_eq_refl {A : cofeT} (a : A) P : P  (a  a)%I.
Proof. by intros x n ??; simpl. Qed.
Lemma uPred_eq_rewrite {A : cofeT} P (Q : A  uPred M)
    `{HQ : ! n, Proper (dist n ==> dist n) Q} a b :
  P  (a  b)%I  P  Q a  P  Q b.
Proof.
  intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
Lemma uPred_eq_equiv `{Empty M, !RAEmpty M} {A : cofeT} (a b : A) :
  True%I  (a  b : uPred M)%I  a  b.
Proof.
  intros Hab; apply equiv_dist; intros n; apply Hab with .
  * apply cmra_valid_validN, ra_empty_valid.
  * by destruct n.
Qed.
Lemma uPred_iff_equiv P Q : True%I  (P  Q)%I  P  Q.
Proof. by intros HPQ x [|n] ?; [|split; intros; apply HPQ with x (S n)]. Qed.

(* Derived logical stuff *)
Lemma uPred_and_elim_l' P Q R : P  R  (P  Q)%I  R.
Proof. by rewrite uPred_and_elim_l. Qed.
Lemma uPred_and_elim_r' P Q R : Q  R  (P  Q)%I  R.
Proof. by rewrite uPred_and_elim_r. Qed.

Hint Resolve uPred_or_elim uPred_or_intro_l uPred_or_intro_r.
Hint Resolve uPred_and_intro uPred_and_elim_l' uPred_and_elim_r'.
Hint Immediate uPred_True_intro uPred_False_elim.

Global Instance uPred_and_idem : Idempotent () (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_or_idem : Idempotent () (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_and_comm : Commutative () (@uPred_and M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_True_and : LeftId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_and_True : RightId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_False_and : LeftAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_and_False : RightAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_True_or : LeftAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_or_True : RightAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_False_or : LeftId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_or_False : RightId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_and_assoc : Associative () (@uPred_and M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_or_comm : Commutative () (@uPred_or M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance uPred_or_assoc : Associative () (@uPred_or M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.

Lemma uPred_const_mono (P Q: Prop) : (P  Q)  uPred_const P  @uPred_const M Q.
Proof.
  intros; rewrite <-(left_id True%I _ (uPred_const P)).
  eauto using uPred_const_elim, uPred_const_intro.
Qed.
Lemma uPred_and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
Proof. auto. Qed.
Lemma uPred_or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
Proof. auto. Qed.
Lemma uPred_impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')%I  (Q  Q')%I.
Proof.
  intros HP HQ'; apply uPred_impl_intro; rewrite <-HQ'.
  transitivity ((P  P')  P)%I; eauto using uPred_impl_elim.
Qed.
Lemma uPred_forall_mono {A} (P Q : A  uPred M) :
  ( a, P a  Q a)  ( a, P a)%I  ( a, Q a)%I.
Proof.
  intros HPQ. apply uPred_forall_intro; intros a; rewrite <-(HPQ a).
  apply uPred_forall_elim.
Qed.
Lemma uPred_exist_mono {A} (P Q : A  uPred M) :
  ( a, P a  Q a)  ( a, P a)%I  ( a, Q a)%I.
Proof.
  intros HPQ. apply uPred_exist_elim; intros a; rewrite (HPQ a).
  apply uPred_exist_intro.
Qed.

Global Instance uPred_const_mono' : Proper (impl ==> ()) (@uPred_const M).
Proof. intros P Q; apply uPred_const_mono. Qed.
Global Instance uPred_and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply uPred_and_mono. Qed.
Global Instance uPred_or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply uPred_or_mono. Qed.
Global Instance uPred_impl_mono' :
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply uPred_impl_mono. Qed.
Global Instance uPred_forall_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Proof. intros P1 P2; apply uPred_forall_mono. Qed.
Global Instance uPred_exist_mono' A :
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Proof. intros P1 P2; apply uPred_exist_mono. Qed.

Lemma uPred_equiv_eq {A : cofeT} P (a b : A) : a  b  P  (a  b)%I.
Proof. intros ->; apply uPred_eq_refl. Qed.
Lemma uPred_eq_sym {A : cofeT} (a b : A) : (a  b)%I  (b  a : uPred M)%I.
Proof.
  refine (uPred_eq_rewrite _ (λ b, b  a)%I a b _ _); auto using uPred_eq_refl.
  intros n; solve_proper.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
460
461

(* BI connectives *)
462
Lemma uPred_sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
463
Proof.
464
465
  intros HQ HQ' x n' Hx' (x1&x2&Hx&?&?); exists x1, x2;
    rewrite Hx in Hx'; eauto 7 using cmra_valid_op_l, cmra_valid_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
466
Qed.
467
Global Instance uPred_True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
468
469
470
Proof.
  intros P x n Hvalid; split.
  * intros (x1&x2&Hx&_&?); rewrite Hx in Hvalid |- *.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
    eauto using uPred_weaken, ra_included_r.
472
  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Robbert Krebbers's avatar
Robbert Krebbers committed
473
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
474
Global Instance uPred_sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
475
476
Proof.
  by intros P Q x n ?; split;
477
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
478
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
479
Global Instance uPred_sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
480
481
Proof.
  intros P Q R x n ?; split.
482
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
    + by rewrite <-(associative op), <-Hy, <-Hx.
484
485
    + 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
486
    + by rewrite (associative op), <-Hy, <-Hx.
487
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
488
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
Lemma uPred_wand_intro P Q R : (R  P)%I  Q  R  (P - Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
490
491
Proof.
  intros HPQ x n ?? x' n' ???; apply HPQ; auto.
492
  exists x, x'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
493
  eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
494
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
495
Lemma uPred_wand_elim P Q : ((P - Q)  P)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
496
497
498
Proof.
  by intros x n Hvalid (x1&x2&Hx&HPQ&?); rewrite Hx in Hvalid |- *; apply HPQ.
Qed.
499
Lemma uPred_or_sep_distr P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
Proof.
501
502
  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
503
504
    first [by left | by right | done].
Qed.
505
Lemma uPred_exist_sep_distr `(P : A  uPred M) Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
506
507
  (( b, P b)  Q)%I  ( b, P b  Q)%I.
Proof.
508
  intros x [|n]; [done|split; [by intros (x1&x2&Hx&[a ?]&?); exists a,x1,x2|]].
509
  intros [a (x1&x2&Hx&?&?)]; exists x1, x2; split_ands; by try exists a.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
Qed.
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541

(* Derived BI Stuff *)
Hint Resolve uPred_sep_mono.
Global Instance uPred_sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply uPred_sep_mono. Qed.
Lemma uPred_wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')%I  (Q - Q')%I.
Proof.
  intros HP HQ; apply uPred_wand_intro; rewrite HP, <-HQ; apply uPred_wand_elim.
Qed.
Global Instance uPred_wand_mono' :
  Proper (flip () ==> () ==> ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply uPred_wand_mono. Qed.

Global Instance uPred_sep_True : RightId () True%I (@uPred_sep M).
Proof. by intros P; rewrite (commutative _), (left_id _ _). Qed.
Lemma uPred_sep_elim_l P Q R : P  R  (P  Q)%I  R.
Proof. by intros HR; rewrite <-(right_id _ () R)%I, HR, (uPred_True_intro Q). Qed.
Lemma uPred_sep_elim_r P Q : (P  Q)%I  Q.
Proof. by rewrite (commutative ())%I; apply uPred_sep_elim_l. Qed.
Hint Resolve uPred_sep_elim_l uPred_sep_elim_r.
Lemma uPred_sep_and P Q : (P  Q)%I  (P  Q)%I.
Proof. auto. Qed.
Global Instance uPred_sep_False : LeftAbsorb () False%I (@uPred_sep M).
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Global Instance uPred_False_sep : RightAbsorb () False%I (@uPred_sep M).
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Lemma uPred_impl_wand P Q : (P  Q)%I  (P - Q)%I.
Proof. apply uPred_wand_intro, uPred_impl_elim with P; auto. Qed.
Lemma uPred_and_sep_distr P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
Proof. auto. Qed.
Lemma uPred_forall_sep_distr `(P : A  uPred M) Q :
542
  (( a, P a)  Q)%I  ( a, P a  Q)%I.
543
Proof. by apply uPred_forall_intro; intros a; rewrite uPred_forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
545

(* Later *)
546
547
548
Lemma uPred_later_mono P Q : P  Q  ( P)%I  ( Q)%I.
Proof. intros HP x [|n] ??; [done|apply HP; auto using cmra_valid_S]. Qed.
Lemma uPred_later_intro P : P  ( P)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
549
550
Proof.
  intros x [|n] ??; simpl in *; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
551
  apply uPred_weaken with x (S n); auto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
552
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
Lemma uPred_lub P : ( P  P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
Proof.
  intros x n ? HP; induction n as [|n IH]; [by apply HP|].
Robbert Krebbers's avatar
Robbert Krebbers committed
556
  apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
558
Lemma uPred_later_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Proof. by intros x [|n]; split. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
560
Lemma uPred_later_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
Proof. intros x [|n]; simpl; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
Lemma uPred_later_forall `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Proof. by intros x [|n]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
564
Lemma uPred_later_exist `(P : A  uPred M) : ( a,  P a)%I  (  a, P a)%I.
565
Proof. by intros x [|[|n]]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
566
Lemma uPred_later_exist' `{Inhabited A} (P : A  uPred M) :
567
  (  a, P a)%I  ( a,  P a)%I.
568
Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
569
Lemma uPred_later_sep P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
570
571
Proof.
  intros x n ?; split.
572
  * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
Robbert Krebbers's avatar
Robbert Krebbers committed
573
    destruct (cmra_extend_op n x x1 x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
574
      as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
575
    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
Robbert Krebbers's avatar
Robbert Krebbers committed
576
  * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
577
    exists x1, x2; eauto using (dist_S (A:=M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
578
579
Qed.

580
581
582
583
584
585
586
587
588
589
590
591
592
593
(* Later derived *)
Global Instance uPred_later_mono' : Proper (() ==> ()) (@uPred_later M).
Proof. intros P Q; apply uPred_later_mono. Qed.
Lemma uPred_later_impl P Q : ( (P  Q))%I  ( P   Q)%I.
Proof.
  apply uPred_impl_intro; rewrite <-uPred_later_and.
  apply uPred_later_mono, uPred_impl_elim with P; auto.
Qed.
Lemma uPred_later_wand P Q : ( (P - Q))%I  ( P -  Q)%I.
Proof.
  apply uPred_wand_intro; rewrite <-uPred_later_sep.
  apply uPred_later_mono, uPred_wand_elim.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
594
(* Always *)
595
596
597
598
Lemma uPred_always_const (P : Prop) :
  ( uPred_const P : uPred M)%I  uPred_const P.
Proof. done. Qed.
Lemma uPred_always_elim P : ( P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
600
  intros x n ??; apply uPred_weaken with (unit x) n;auto using ra_included_unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
602
Lemma uPred_always_intro P Q : ( P)%I  Q  ( P)%I  ( Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
603
604
605
606
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
607
Lemma uPred_always_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
608
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
609
Lemma uPred_always_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
610
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
611
Lemma uPred_always_forall `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
Lemma uPred_always_exist `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Proof. done. Qed.
615
616
617
618
619
Lemma uPred_always_and_sep' P Q : ( (P  Q))%I  ( (P  Q))%I.
Proof.
  intros x n ? [??]; exists (unit x), (unit x); rewrite ra_unit_unit; auto.
Qed.
Lemma uPred_always_and_sep_l P Q : ( P  Q)%I  ( P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
Proof.
621
  intros x n ? [??]; exists (unit x), x; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
623
  by rewrite ra_unit_l, ra_unit_idempotent.
Qed.
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
Lemma uPred_always_later P : (  P)%I  (  P)%I.
Proof. done. Qed.

(* Always derived *)
Lemma uPred_always_always P : (  P)%I  ( P)%I.
Proof.
  apply (anti_symmetric ()); auto using uPred_always_elim, uPred_always_intro.
Qed.
Lemma uPred_always_mono P Q : P  Q  ( P)%I  ( Q)%I.
Proof. intros. apply uPred_always_intro. by rewrite uPred_always_elim. Qed.
Hint Resolve uPred_always_mono.
Global Instance uPred_always_mono' : Proper (() ==> ()) (@uPred_always M).
Proof. intros P Q; apply uPred_always_mono. Qed.
Lemma uPred_always_impl P Q : ( (P  Q))%I  ( P   Q)%I.
Proof.
  apply uPred_impl_intro; rewrite <-uPred_always_and.
  apply uPred_always_mono, uPred_impl_elim with P; auto.
Qed.
Lemma uPred_always_eq {A:cofeT} (a b : A) : ( (a  b))%I  (a  b : uPred M)%I.
Proof.
  apply (anti_symmetric ()); auto using uPred_always_elim.
  refine (uPred_eq_rewrite _ (λ b,  (a  b))%I a b _ _); auto.
  { intros n; solve_proper. }
  rewrite <-(uPred_eq_refl _ True), uPred_always_const; auto.
Qed.
Lemma uPred_always_sep P Q : ( (P  Q))%I  ( P   Q)%I.
Proof.
  apply (anti_symmetric ()).
  * rewrite <-uPred_always_and_sep_l; auto.
  * rewrite <-uPred_always_and_sep', uPred_always_and; auto.
Qed.
Lemma uPred_always_wand P Q : ( (P - Q))%I  ( P -  Q)%I.
Proof.
  by apply uPred_wand_intro; rewrite <-uPred_always_sep, uPred_wand_elim.
Qed.

Lemma uPred_always_sep_and P Q : ( (P  Q))%I  ( (P  Q))%I.
Proof. apply (anti_symmetric ()); auto using uPred_always_and_sep'. Qed.
Lemma uPred_always_sep_dup P : ( P)%I  ( P   P)%I.
Proof. by rewrite <-uPred_always_sep, uPred_always_sep_and, (idempotent _). Qed.
Lemma uPred_always_wand_impl P Q : ( (P - Q))%I  ( (P  Q))%I.
Proof.
  apply (anti_symmetric ()); [|by rewrite <-uPred_impl_wand].
  apply uPred_always_intro, uPred_impl_intro.
  by rewrite uPred_always_and_sep_l, uPred_always_elim, uPred_wand_elim.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
670

Robbert Krebbers's avatar
Robbert Krebbers committed
671
(* Own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
672
673
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
674
675
676
677
678
679
680
681
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
682
683
Lemma uPred_own_unit (a : M) : uPred_own (unit a)  ( uPred_own (unit a))%I.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
684
685
686
  intros x n; split; [intros [a' Hx]|by apply uPred_always_elim]. simpl.
  rewrite <-(ra_unit_idempotent a), Hx.
  apply cmra_unit_preserving, cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
687
688
689
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
690
Lemma uPred_own_valid (a : M) : uPred_own a  uPred_valid a.
Robbert Krebbers's avatar
Robbert Krebbers committed
691
692
693
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
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712

(* 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|].
Robbert Krebbers's avatar
Robbert Krebbers committed
713
  destruct (cmra_extend_op 1 x x1 x2) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
  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' ?].
Robbert Krebbers's avatar
Robbert Krebbers committed
739
  destruct (cmra_extend_op 1 x a a') as ([b b']&Hx&Hb&Hb'); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
740
741
  by exists b'; rewrite Hx, (timeless a b) by done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
742
End logic.