upred.v 43.5 KB
Newer Older
1
Require Export algebra.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
Record uPred (M : cmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
8
  uPred_ne x1 x2 n : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  uPred_weaken x1 x2 n1 n2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
10
    uPred_holds n1 x1  x1  x2  n2  n1  {n2} x2  uPred_holds n2 x2
Robbert Krebbers's avatar
Robbert Krebbers committed
11
}.
12
Arguments uPred_holds {_} _ _ _ : simpl never.
13
14
Global Opaque uPred_holds.
Local Transparent uPred_holds.
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

18
19
20
21
22
23
24
Section cofe.
  Context {M : cmraT}.
  Instance uPred_equiv : Equiv (uPred M) := λ P Q,  x n,
    {n} x  P n x  Q n x.
  Instance uPred_dist : Dist (uPred M) := λ n P Q,  x n',
    n'  n  {n'} x  P n' x  Q n' x.
  Program Instance uPred_compl : Compl (uPred M) := λ c,
25
    {| uPred_holds n x := c (S n) n x |}.
26
27
28
  Next Obligation. by intros c x y n ??; simpl in *; apply uPred_ne with x. Qed.
  Next Obligation.
    intros c x1 x2 n1 n2 ????; simpl in *.
29
    apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
30
31
32
33
34
35
36
37
38
  Qed.
  Definition uPred_cofe_mixin : CofeMixin (uPred M).
  Proof.
    split.
    * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
      intros HPQ x n ?; apply HPQ with n; auto.
    * intros n; split.
      + by intros P x i.
      + by intros P Q HPQ x i ??; symmetry; apply HPQ.
39
      + by intros P Q Q' HP HQ x i ??; transitivity (Q i x);[apply HP|apply HQ].
40
    * intros n P Q HPQ x i ??; apply HPQ; auto.
41
    * intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
42
43
44
45
46
  Qed.
  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.

47
Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
49
50
51
52
Instance uPred_proper {M} (P : uPred M) n : Proper (() ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.

Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
53
  P1 {n} P2  {n} x  P1 n x  P2 n x.
54
Proof. intros HP ?; apply HP; auto. Qed.
55
56
Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
  x1  x2  n2  n1  {n2} x2  P n1 x1  P n2 x2.
57
Proof. eauto using uPred_weaken. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59

(** functor *)
60
61
62
63
Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
  `{!CMRAMonotone f} (P : uPred M1) :
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Qed.
67
68
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
  `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  Proper (dist n ==> dist n) (uPred_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Qed.
73
74
75
76
77
78
79
80
81
82
83
Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P  P.
Proof. by intros x n ?. Qed.
Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
      `{!CMRAMonotone f} `{!CMRAMonotone g}
      (P : uPred M3):
  uPred_map (g  f) P  uPred_map f (uPred_map g P).
Proof. by intros x n Hx. Qed.
Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
      `{!CMRAMonotone f} `{!CMRAMonotone g}:
  ( x, f x  g x) ->  x, uPred_map f x  uPred_map g x.
Proof. move=> H x P n Hx /=. by rewrite /uPred_holds /= H. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
87
    `{!CMRAMonotone f, !CMRAMonotone g} n :
88
  f {n} g  uPredC_map f {n} uPredC_map g.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Proof.
90
91
  by intros Hfg P y n' ??;
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94

(** logical entailement *)
95
96
Definition uPred_entails {M} (P Q : uPred M) :=  x n, {n} x  P n x  Q n x.
Hint Extern 0 (uPred_entails ?P ?P) => reflexivity.
97
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99

(** logical connectives *)
100
Program Definition uPred_const {M} (φ : Prop) : uPred M :=
101
  {| uPred_holds n x := φ |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Solve Obligations with done.
103
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
104

Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
108
109
110
111
112
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
113
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Next Obligation.
115
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto.
117
  assert (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
118
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Qed.
121
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
122

Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
125
126
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 :=
127
128
  {| uPred_holds n x :=  a, P a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
129

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

Robbert Krebbers's avatar
Robbert Krebbers committed
134
Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
135
  {| uPred_holds n x :=  x1 x2, x {n} x1  x2  P n x1  Q n x2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
Next Obligation.
137
  by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
141
  assert ( x2', y {n2} x1  x2'  x2  x2') as (x2'&Hy&?).
142
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
    apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
144
  clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
145
146
  * apply uPred_weaken with x1 n1; eauto using cmra_validN_op_l.
  * apply uPred_weaken with x2 n1; eauto using cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
148
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
151
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Next Obligation.
153
  intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
  by rewrite (dist_le _ _ _ n2 Hx).
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
  intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
  apply uPred_weaken with (x1  x3) n3;
160
    eauto using cmra_validN_included, cmra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Next Obligation.
167
  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken,cmra_validN_S; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (unit x) |}.
171
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
174
    eauto using cmra_unit_preserving, cmra_unit_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
176
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
177
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
  intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  exists (a'  x2). by rewrite (associative op) -(dist_le _ _ _ _ Hx1) // Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
185
  {| uPred_holds n x := {n} a |}.
186
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
187

Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
190
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
191
192
193
Arguments uPred_entails _ _%I _%I.
Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope.
195
Notation "x = y" := (uPred_const (x%type = y%type)) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
199
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
Infix "∨" := uPred_or : uPred_scope.
201
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
204
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
205
Notation "P -★ Q" := (uPred_wand P Q)
206
  (at level 199, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Notation "∀ x .. y , P" :=
208
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
Notation "∃ x .. y , P" :=
210
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
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
213
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
Notation "✓" := uPred_valid (at level 1) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
215

216
217
218
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

219
220
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
221
222
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
223
224
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_sep Ps end%I.
225
226
Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
227

228
229
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
Arguments timelessP {_} _ {_} _ _ _ _.
230
231
Class AlwaysStable {M} (P : uPred M) := always_stable : P   P.
Arguments always_stable {_} _ {_} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
232

Robbert Krebbers's avatar
Robbert Krebbers committed
233
Module uPred. Section uPred_logic.
234
Context {M : cmraT}.
235
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
Implicit Types P Q : uPred M.
237
Implicit Types Ps Qs : list (uPred M).
238
Implicit Types A : Type.
239
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
240
Arguments uPred_holds {_} !_ _ _ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
241

242
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
243
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
244
Global Instance: AntiSymmetric () (@uPred_entails M).
245
Proof. intros P Q HPQ HQP; split; auto. Qed.
246
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Proof.
248
  split; [|by intros [??]; apply (anti_symmetric ())].
249
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
250
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
Global Instance entails_proper :
252
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
253
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
255
256
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
  * by transitivity P1; [|transitivity Q1].
  * by transitivity P2; [|transitivity Q2].
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258

259
(** Non-expansiveness and setoid morphisms *)
Robbert Krebbers's avatar
Robbert Krebbers committed
260
Global Instance const_proper : Proper (iff ==> ()) (@uPred_const M).
261
Proof. by intros φ1 φ2 Hφ ? [|n] ?; try apply Hφ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
263
264
265
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
266
Global Instance and_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
267
  Proper (() ==> () ==> ()) (@uPred_and M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
272
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
273
Global Instance or_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
274
  Proper (() ==> () ==> ()) (@uPred_or M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
275
Global Instance impl_ne n :
Robbert Krebbers's avatar
Robbert Krebbers committed
276
  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
277
278
279
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
280
Global Instance impl_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
281
  Proper (() ==> () ==> ()) (@uPred_impl M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
285
  intros P P' HP Q Q' HQ x n' ??; split; intros (x1&x2&?&?&?); cofe_subst x;
    exists x1, x2; split_ands; try (apply HP || apply HQ);
286
    eauto using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
288
Global Instance sep_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
289
  Proper (() ==> () ==> ()) (@uPred_sep M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
Global Instance wand_ne n :
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
292
293
Proof.
  intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
294
    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Global Instance wand_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  Proper (() ==> () ==> ()) (@uPred_wand M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Global Instance eq_ne (A : cofeT) n :
Robbert Krebbers's avatar
Robbert Krebbers committed
299
  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
300
301
Proof.
  intros x x' Hx y y' Hy z n'; split; intros; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
  * by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
  * by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
Global Instance eq_proper (A : cofeT) :
Robbert Krebbers's avatar
Robbert Krebbers committed
306
  Proper (() ==> () ==> ()) (@uPred_eq M A) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
Global Instance forall_ne A :
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
Global Instance forall_proper A :
Robbert Krebbers's avatar
Robbert Krebbers committed
311
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
312
Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
Global Instance exists_ne A :
Robbert Krebbers's avatar
Robbert Krebbers committed
314
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
315
Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
Global Instance exist_proper A :
Robbert Krebbers's avatar
Robbert Krebbers committed
317
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
318
Proof. by intros P1 P2 HP x n'; split; intros [a ?]; exists a; apply HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
319
Global Instance later_contractive : Contractive (@uPred_later M).
Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
Proof.
  intros n P Q HPQ x [|n'] ??; simpl; [done|].
322
  apply (HPQ n'); eauto using cmra_validN_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
Global Instance later_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
325
  Proper (() ==> ()) (@uPred_later M) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
327
Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_validN. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Global Instance always_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
329
  Proper (() ==> ()) (@uPred_always M) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
330
Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_own M).
Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
Proof.
  by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first
Robbert Krebbers's avatar
Robbert Krebbers committed
333
334
    [rewrite -(dist_le _ _ _ _ Ha); last lia
    |rewrite (dist_le _ _ _ _ Ha); last lia].
Robbert Krebbers's avatar
Robbert Krebbers committed
335
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
337
Global Instance own_proper : Proper (() ==> ()) (@uPred_own M) := ne_proper _.
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
338
Proof. unfold uPred_iff; solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
Global Instance iff_proper :
340
  Proper (() ==> () ==> ()) (@uPred_iff M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
342

(** Introduction and elimination rules *)
343
Lemma const_intro φ P : φ  P   φ.
344
Proof. by intros ???. Qed.
345
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
346
Proof. intros HQP HQR x n ??; apply HQR; first eapply (HQP _ n); eauto. Qed.
347
Lemma True_intro P : P  True.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Proof. by apply const_intro. Qed.
349
Lemma False_elim P : False  P.
350
Proof. by intros x n ?. Qed.
351
Lemma and_elim_l P Q : (P  Q)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
Proof. by intros x n ? [??]. Qed.
353
Lemma and_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
354
Proof. by intros x n ? [??]. Qed.
355
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
356
Proof. intros HQ HR x n ??; split; auto. Qed.
357
Lemma or_intro_l P Q : P  (P  Q).
358
Proof. intros x n ??; left; auto. Qed.
359
Lemma or_intro_r P Q : Q  (P  Q).
360
Proof. intros x n ??; right; auto. Qed.
361
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
363
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
365
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
Qed.
367
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
368
Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
369
Lemma forall_intro {A} P (Q : A  uPred M): ( a, P  Q a)  P  ( a, Q a).
370
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
371
Lemma forall_elim {A} {P : A  uPred M} a : ( a, P a)  P a.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
Proof. intros x n ? HP; apply HP. Qed.
373
Lemma exist_intro {A} {P : A  uPred M} a : P a  ( a, P a).
374
Proof. by intros x n ??; exists a. Qed.
375
Lemma exist_elim {A} (P : A  uPred M) Q : ( a, P a  Q)  ( a, P a)  Q.
376
Proof. by intros HPQ x n ? [a ?]; apply HPQ with a. Qed.
377
Lemma eq_refl {A : cofeT} (a : A) P : P  (a  a).
378
Proof. by intros x n ??; simpl. Qed.
Ralf Jung's avatar
Ralf Jung committed
379
380
Lemma eq_rewrite {A : cofeT} a b (Q : A  uPred M) P
  `{HQ: n, Proper (dist n ==> dist n) Q} : P  (a  b)  P  Q a  P  Q b.
381
382
383
Proof.
  intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
384
Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
385
  True  (a  b)  a  b.
386
Proof.
387
388
  intros Hab; apply equiv_dist; intros n; apply Hab with ; last done.
  apply cmra_valid_validN, cmra_empty_valid.
389
Qed.
390
Lemma iff_equiv P Q : True  (P  Q)  P  Q.
391
Proof. by intros HPQ x n ?; split; intros; apply HPQ with x n. Qed.
392
393

(* Derived logical stuff *)
394
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
395
Proof. by rewrite and_elim_l. Qed.
396
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
397
Proof. by rewrite and_elim_r. Qed.
398
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
399
Proof. intros ->; apply or_intro_l. Qed.
400
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
401
Proof. intros ->; apply or_intro_r. Qed.
402
Lemma exist_intro' {A} P (Q : A  uPred M) a : P  Q a  P  ( a, Q a).
403
Proof. intros ->; apply exist_intro. Qed.
404

405
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
407
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
408

409
410
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
411
412
413
414
415
416
417
418
Lemma impl_elim_l P Q : ((P  Q)  P)  Q.
Proof. apply impl_elim with P; auto. Qed.
Lemma impl_elim_r P Q : (P  (P  Q))  Q.
Proof. apply impl_elim with P; auto. Qed.
Lemma impl_elim_l' P Q R : P  (Q  R)  (P  Q)  R.
Proof. intros; apply impl_elim with Q; auto. Qed.
Lemma impl_elim_r' P Q R : Q  (P  R)  (P  Q)  R.
Proof. intros; apply impl_elim with P; auto. Qed.
419
Lemma impl_entails P Q : True  (P  Q)  P  Q.
420
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
421
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
422
Proof. auto using impl_intro_l. Qed.
423

424
425
Lemma const_intro_l φ Q R : φ  (■φ  Q)  R  Q  R.
Proof. intros ? <-; auto using const_intro. Qed.
426
Lemma const_intro_r φ Q R : φ  (Q  ■φ)  R  Q  R.
427
Proof. intros ? <-; auto using const_intro. Qed.
428
429
430
431
Lemma const_elim_l φ Q R : (φ  Q  R)  ( φ  Q)  R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_elim_r φ Q R : (φ  Q  R)  (Q   φ)  R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
432
433
Lemma const_equiv (φ : Prop) : φ  ( φ : uPred M)%I  True%I.
Proof. intros; apply (anti_symmetric _); auto using const_intro. Qed.
434
435
436
Lemma equiv_eq {A : cofeT} P (a b : A) : a  b  P  (a  b).
Proof. intros ->; apply eq_refl. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : (a  b)  (b  a).
437
Proof.
Ralf Jung's avatar
Ralf Jung committed
438
  apply (eq_rewrite a b (λ b, b  a)%I); auto using eq_refl.
439
  intros n; solve_proper.
440
Qed.
441

442
443
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
444
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
445
Proof. auto. Qed.
446
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
447
Proof. auto. Qed.
448
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
449
Proof.
450
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
451
  apply impl_elim with P; eauto.
452
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
453
Lemma forall_mono {A} (P Q : A  uPred M) :
454
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
455
Proof.
456
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
457
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
458
Lemma exist_mono {A} (P Q : A  uPred M) :
459
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
460
Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
461
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
462
Proof. intros φ1 φ2; apply const_mono. Qed.
463
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
464
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
465
466
467
Global Instance and_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
468
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
469
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
470
471
472
Global Instance or_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
473
Global Instance impl_mono' :
474
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
475
476
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
477
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
478
479
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
480
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
481
Proof. intros P1 P2; apply exist_mono. Qed.
482

483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
Global Instance and_idem : Idempotent () (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_idem : Idempotent () (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_comm : Commutative () (@uPred_and M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance True_and : LeftId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_True : RightId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_or : LeftId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_False : RightId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_assoc : Associative () (@uPred_and M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Global Instance or_comm : Commutative () (@uPred_or M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance or_assoc : Associative () (@uPred_or M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
511
512
513
514
515
516
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.
  intros P; apply (anti_symmetric ()).
  * by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  * by apply impl_intro_l; rewrite left_id.
Qed.
517
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
518
Proof.
519
  apply (anti_symmetric ()); first auto.
520
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
521
Qed.
522
523
524
525
526
Lemma or_and_r P Q R : (P  Q  R)%I  ((P  R)  (Q  R))%I.
Proof. by rewrite -!(commutative _ R) or_and_l. Qed.
Lemma and_or_l P Q R : (P  (Q  R))%I  (P  Q  P  R)%I.
Proof.
  apply (anti_symmetric ()); last auto.
527
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
528
529
530
Qed.
Lemma and_or_r P Q R : ((P  Q)  R)%I  (P  R  Q  R)%I.
Proof. by rewrite -!(commutative _ R) and_or_l. Qed.
531
532
533
534
535
536
537
538
Lemma and_exist_l {A} P (Q : A  uPred M) : (P   a, Q a)%I  ( a, P  Q a)%I.
Proof.
  apply (anti_symmetric ()).
  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
    by rewrite -(exist_intro a) and_elim_r.
Qed.
Ralf Jung's avatar
Ralf Jung committed
539
540
541
542
543
Lemma and_exist_r {A} P (Q : A  uPred M) : (( a, Q a)  P)%I  ( a, Q a  P)%I.
Proof.
  rewrite -(commutative _ P) and_exist_l.
  apply exist_proper=>a. by rewrite commutative.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
545

(* BI connectives *)
546
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
547
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
548
  intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
549
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
551
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
552
553
Proof.
  intros P x n Hvalid; split.
554
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
555
  * by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
556
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Global Instance sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
558
559
Proof.
  by intros P Q x n ?; split;
560
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
561
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
Global Instance sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
563
564
Proof.
  intros P Q R x n ?; split.
565
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
566
    + by rewrite -(associative op) -Hy -Hx.
567
568
    + 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
569
    + by rewrite (associative op) -Hy -Hx.
570
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
571
Qed.
572
Lemma wand_intro_r P Q R : (P  Q)  R  P  (Q - R).
Robbert Krebbers's avatar
Robbert Krebbers committed
573
Proof.
574
  intros HPQR x n ?? x' n' ???; apply HPQR; auto.
575
  exists x, x'; split_ands; auto.
576
  eapply uPred_weaken with x n; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
Qed.
578
Lemma wand_elim_l P Q : ((P - Q)  P)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
579
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
580
581

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
582
Hint Resolve sep_mono.
583
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
584
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
585
586
587
Global Instance sep_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
588
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')  (Q - Q').
589
Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
590
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
591
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
592

Robbert Krebbers's avatar
Robbert Krebbers committed
593
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
594
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
595
Lemma sep_elim_l P Q : (P  Q)  P.
596
Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
597
Lemma sep_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
598
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
599
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
600
Proof. intros ->; apply sep_elim_l. Qed.
601
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
602
603
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
604
Lemma sep_intro_True_l P Q R : True  P  R  Q  R  (P  Q).
605
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
606
Lemma sep_intro_True_r P Q R : R  P  True  Q  R  (P  Q).
607
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
608
609
Lemma wand_intro_l P Q R : (Q  P)  R  P  (Q - R).
Proof. rewrite (commutative _); apply wand_intro_r. Qed.
610
611
612
613
614
615
Lemma wand_elim_r P Q : (P  (P - Q))  Q.
Proof. rewrite (commutative _ P); apply wand_elim_l. Qed.
Lemma wand_elim_l' P Q R : P  (Q - R)  (P  Q)  R.
Proof. intros ->; apply wand_elim_l. Qed.
Lemma wand_elim_r' P Q R : Q  (P - R)  (P  Q)  R.
Proof. intros ->; apply wand_elim_r. Qed.
616
Lemma sep_and P Q : (P  Q)  (P  Q).
617
Proof. auto. Qed.
618
Lemma impl_wand P Q : (P  Q)  (P - Q).
619
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
620

Robbert Krebbers's avatar
Robbert Krebbers committed
621
Global Instance sep_False : LeftAbsorb () False%I (@uPred_sep M).
622
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Global Instance False_sep : RightAbsorb () False%I (@uPred_sep M).
624
Proof. intros P; apply (anti_symmetric _); auto. Qed.
625
626

Lemma sep_and_l P Q R : (P  (Q  R))  ((P  Q)  (P  R)).
627
Proof. auto. Qed.
628
629
630
Lemma sep_and_r P Q R : ((P  Q)  R)  ((P  R)  (Q  R)).
Proof. auto. Qed.
Lemma sep_or_l P Q R : (P  (Q  R))%I  ((P  Q)  (P  R))%I.
631
632
633
634
635
636
Proof.
  apply (anti_symmetric ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l.
  - by apply or_intro_l.
  - by apply or_intro_r.
Qed.
637
638
639
640
Lemma sep_or_r P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
Proof. by rewrite -!(commutative _ R) sep_or_l. Qed.
Lemma sep_exist_l {A} P (Q : A  uPred M) : (P   a, Q a)%I  ( a, P  Q a)%I.
Proof.
641
642
643
644
  intros; apply (anti_symmetric ()).
  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
645
646
647
648
Qed.
Lemma sep_exist_r {A} (P: A  uPred M) Q: (( a, P a)  Q)%I  ( a, P a  Q)%I.
Proof. setoid_rewrite (commutative _ _ Q); apply sep_exist_l. Qed.
Lemma sep_forall_l {A} P (Q : A  uPred M) : (P   a, Q a)  ( a, P  Q a).
649
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
650
Lemma sep_forall_r {A} (P : A  uPred M) Q : (( a, P a)  Q)  ( a, P a  Q).
651
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
652
653

(* Later *)
654
Lemma later_mono P Q : P  Q   P   Q.
655
Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
656
Lemma later_intro P : P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
657
658
Proof.
  intros x [|n] ??; simpl in *; [done|].
659
  apply uPred_weaken with x (S n); eauto using cmra_validN_S.