logic.v 33.3 KB
Newer Older
1
Require Import modures.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  {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
  {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',
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  n'  n  {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
  {n} x  P n x  Q n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77

(** 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
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Next Obligation.
94
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
  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).
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  assert ({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
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
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
Program Definition uPred_valid {M : cmraT} (a : M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  {| uPred_holds n x := {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
Notation "✓" := uPred_valid (at level 1) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
200

201
202
203
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
204
Class TimelessP {M} (P : uPred M) := timelessP x n : {1} x  P 1 x  P n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
205

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

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

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

(** Introduction and elimination rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
320
Lemma uPred_const_intro P (Q : Prop) : Q  P  uPred_const Q.
321
Proof. by intros ?? [|?]. Qed.
322
323
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
324
Lemma uPred_True_intro P : P  True%I.
325
Proof. by apply uPred_const_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
Lemma uPred_False_elim P : False%I  P.
327
Proof. by intros x [|n] ?. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Lemma uPred_and_elim_l P Q : (P  Q)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
Proof. by intros x n ? [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
330
Lemma uPred_and_elim_r P Q : (P  Q)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
Proof. by intros x n ? [??]. Qed.
332
333
334
335
336
337
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
338
Lemma uPred_or_elim R P Q : P  R  Q  R  (P  Q)%I  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Lemma uPred_impl_intro P Q R : (R  P)%I  Q  R  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
Qed.
344
345
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
346
Lemma uPred_forall_intro P `(Q: A  uPred M): ( a, P  Q a)  P  ( a, Q a)%I.
347
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Lemma uPred_forall_elim `(P : A  uPred M) a : ( a, P a)%I  P a.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Proof. intros x n ? HP; apply HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
Lemma uPred_exist_intro `(P : A  uPred M) a : P a  ( a, P a)%I.
351
Proof. by intros x [|n] ??; [done|exists a]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
Lemma uPred_exist_elim `(P : A  uPred M) Q : ( a, P a  Q)  ( a, P a)%I  Q.
353
Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
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
460
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
461
462

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

(* 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 :
543
  (( a, P a)  Q)%I  ( a, P a  Q)%I.
544
Proof. by apply uPred_forall_intro; intros a; rewrite uPred_forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
546

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

581
582
583
584
585
586
587
588
589
590
591
592
593
594
(* 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
595
(* Always *)
596
597
598
599
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
600
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
  intros x n ??; apply uPred_weaken with (unit x) n;auto using ra_included_unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
602
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
603
Lemma uPred_always_intro P Q : ( P)%I  Q  ( P)%I  ( Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
605
606
607
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
608
Lemma uPred_always_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
609
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
610
Lemma uPred_always_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
611
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
Lemma uPred_always_forall `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Lemma uPred_always_exist `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
Proof. done. Qed.
616
617
618
619
620
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
621
Proof.
622
  intros x n ? [??]; exists (unit x), x; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
624
  by rewrite ra_unit_l, ra_unit_idempotent.
Qed.
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
670
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
671

Robbert Krebbers's avatar
Robbert Krebbers committed
672
(* Own *)
Robbert Krebbers's avatar
Robbert Krebbers committed
673
674
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
675
676
677
678
679
680
681
682
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
683
684
Lemma uPred_own_unit (a : M) : uPred_own (unit a)  ( uPred_own (unit a))%I.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
685
686
687
  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
688
689
690
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
691
Lemma uPred_own_valid (a : M) : uPred_own a  ( a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
692
693
694
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
695
696
697
698
699
700
701
702
Lemma uPred_valid_intro (a : M) :  a  True%I  ( a)%I.
Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
Lemma uPred_valid_elim_timess (a : M) :
  ValidTimeless a  ¬  a  ( a)%I  False%I.
Proof.
  intros ? Hvalid x [|n] ??; [done|apply Hvalid].
  apply (valid_timeless _), cmra_valid_le with (S n); auto with lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721

(* 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
722
  destruct (cmra_extend_op 1 x x1 x2) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
744
745
746

(** Timeless elements *)
Global Instance uPred_own_timeless (a: M): Timeless a  TimelessP (uPred_own a).
Robbert Krebbers's avatar
Robbert Krebbers committed
747
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
748
  by intros ? x n ??; apply cmra_included_includedN, cmra_timeless_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
749
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
750
End logic.