upred.v 44.3 KB
Newer Older
1
From algebra Require Export 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
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.

22
23
24
25
26
27
28
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,
29
    {| uPred_holds n x := c (S n) n x |}.
30
31
32
  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 *.
33
    apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
34
35
36
37
38
39
40
41
42
  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.
43
      + by intros P Q Q' HP HQ x i ??; transitivity (Q i x);[apply HP|apply HQ].
44
    * intros n P Q HPQ x i ??; apply HPQ; auto.
45
    * intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
46
47
48
49
50
  Qed.
  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.

51
Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
53
54
55
56
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 :
57
  P1 {n} P2  {n} x  P1 n x  P2 n x.
58
Proof. intros HP ?; apply HP; auto. Qed.
59
60
Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
  x1  x2  n2  n1  {n2} x2  P n1 x1  P n2 x2.
61
Proof. eauto using uPred_weaken. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63

(** functor *)
64
65
66
67
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
68
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Qed.
71
72
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
  `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  Proper (dist n ==> dist n) (uPred_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
77
78
79
80
81
82
83
84
85
86
87
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
88
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
89
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    `{!CMRAMonotone f, !CMRAMonotone g} n :
92
  f {n} g  uPredC_map f {n} uPredC_map g.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Proof.
94
95
  by intros Hfg P y n' ??;
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98

(** logical entailement *)
99
Definition uPred_entails {M} (P Q : uPred M) :=  x n, {n} x  P n x  Q n x.
100
Hint Extern 0 (uPred_entails _ _) => reflexivity.
101
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
130
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 :=
131
132
  {| 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
133

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

Robbert Krebbers's avatar
Robbert Krebbers committed
138
Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
139
  {| uPred_holds n x :=  x1 x2, x {n} x1  x2  P n x1  Q n x2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Next Obligation.
141
  by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
145
  assert ( x2', y {n2} x1  x2'  x2  x2') as (x2'&Hy&?).
146
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using cmra_included_l.
147
    apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
148
  clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
149
150
  * 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
151
152
Qed.

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

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

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

192
193
Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
194
195
Notation "■ φ" := (uPred_const φ%C%type)
  (at level 20, right associativity) : uPred_scope.
Ralf Jung's avatar
Ralf Jung committed
196
Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
198
199
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
200
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
Infix "∨" := uPred_or : uPred_scope.
202
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
205
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
206
Notation "P -★ Q" := (uPred_wand P Q)
207
  (at level 199, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
Notation "∀ x .. y , P" :=
209
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Notation "∃ x .. y , P" :=
211
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
212
213
214
215
Notation "▷ P" := (uPred_later P)
  (at level 20, right associativity) : uPred_scope.
Notation "□ P" := (uPred_always P)
  (at level 20, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
Infix "≡" := uPred_eq : uPred_scope.
217
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
218

219
220
221
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
239
Class AlwaysStableL {M} (Ps : list (uPred M)) :=
  always_stableL : Forall AlwaysStable Ps.
Arguments always_stableL {_} _ {_}.

Robbert Krebbers's avatar
Robbert Krebbers committed
240
Module uPred. Section uPred_logic.
241
Context {M : cmraT}.
242
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
Implicit Types P Q : uPred M.
244
Implicit Types Ps Qs : list (uPred M).
245
Implicit Types A : Type.
246
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
247
Arguments uPred_holds {_} !_ _ _ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
248

249
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
250
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
251
Global Instance: AntiSymm () (@uPred_entails M).
252
Proof. intros P Q HPQ HQP; split; auto. Qed.
253
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
Proof.
255
  split; [|by intros [??]; apply (anti_symm ())].
256
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Global Instance entails_proper :
259
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
260
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
262
263
  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
264
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
265

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

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

(* Derived logical stuff *)
401
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
402
Proof. by rewrite and_elim_l. Qed.
403
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
404
Proof. by rewrite and_elim_r. Qed.
405
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
406
Proof. intros ->; apply or_intro_l. Qed.
407
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
408
Proof. intros ->; apply or_intro_r. Qed.
409
Lemma exist_intro' {A} P (Q : A  uPred M) a : P  Q a  P  ( a, Q a).
410
Proof. intros ->; apply exist_intro. Qed.
411

412
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
414
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
415

416
417
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
418
419
420
421
422
423
424
425
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.
426
Lemma impl_entails P Q : True  (P  Q)  P  Q.
427
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
428
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
429
Proof. auto using impl_intro_l. Qed.
430

431
432
Lemma const_intro_l φ Q R : φ  (■φ  Q)  R  Q  R.
Proof. intros ? <-; auto using const_intro. Qed.
433
Lemma const_intro_r φ Q R : φ  (Q  ■φ)  R  Q  R.
434
Proof. intros ? <-; auto using const_intro. Qed.
435
436
437
438
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
439
Lemma const_equiv (φ : Prop) : φ  ( φ : uPred M)%I  True%I.
440
Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
441
442
443
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).
444
Proof.
Ralf Jung's avatar
Ralf Jung committed
445
  apply (eq_rewrite a b (λ b, b  a)%I); auto using eq_refl.
446
  intros n; solve_proper.
447
Qed.
448

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

490
491
492
493
494
495
Global Instance and_idem : IdemP () (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_idem : IdemP () (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_comm : Comm () (@uPred_and M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
496
Global Instance True_and : LeftId () True%I (@uPred_and M).
497
Proof. intros P; apply (anti_symm ()); auto. Qed.
498
Global Instance and_True : RightId () True%I (@uPred_and M).
499
Proof. intros P; apply (anti_symm ()); auto. Qed.
500
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
501
Proof. intros P; apply (anti_symm ()); auto. Qed.
502
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
503
Proof. intros P; apply (anti_symm ()); auto. Qed.
504
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
505
Proof. intros P; apply (anti_symm ()); auto. Qed.
506
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
507
Proof. intros P; apply (anti_symm ()); auto. Qed.
508
Global Instance False_or : LeftId () False%I (@uPred_or M).
509
Proof. intros P; apply (anti_symm ()); auto. Qed.
510
Global Instance or_False : RightId () False%I (@uPred_or M).
511
512
513
514
515
516
517
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_assoc : Assoc () (@uPred_and M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance or_comm : Comm () (@uPred_or M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance or_assoc : Assoc () (@uPred_or M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
518
519
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.
520
  intros P; apply (anti_symm ()).
Robbert Krebbers's avatar
Robbert Krebbers committed
521
522
523
  * by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  * by apply impl_intro_l; rewrite left_id.
Qed.
524
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
525
Proof.
526
  apply (anti_symm ()); first auto.
527
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
528
Qed.
529
Lemma or_and_r P Q R : (P  Q  R)%I  ((P  R)  (Q  R))%I.
530
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
531
532
Lemma and_or_l P Q R : (P  (Q  R))%I  (P  Q  P  R)%I.
Proof.
533
  apply (anti_symm ()); last auto.
534
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
535
536
Qed.
Lemma and_or_r P Q R : ((P  Q)  R)%I  (P  R  Q  R)%I.
537
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
538
539
Lemma and_exist_l {A} P (Q : A  uPred M) : (P   a, Q a)%I  ( a, P  Q a)%I.
Proof.
540
  apply (anti_symm ()).
541
542
543
544
545
  - 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
546
547
Lemma and_exist_r {A} P (Q : A  uPred M) : (( a, Q a)  P)%I  ( a, Q a  P)%I.
Proof.
548
549
  rewrite -(comm _ P) and_exist_l.
  apply exist_proper=>a. by rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
550
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
551
552

(* BI connectives *)
553
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
555
  intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
556
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
558
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
559
560
Proof.
  intros P x n Hvalid; split.
561
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
562
  * by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Qed. 
564
Global Instance sep_comm : Comm () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
565
566
Proof.
  by intros P Q x n ?; split;
567
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
Robbert Krebbers's avatar
Robbert Krebbers committed
568
Qed.
569
Global Instance sep_assoc : Assoc () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
570
571
Proof.
  intros P Q R x n ?; split.
572
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
573
    + by rewrite -(assoc op) -Hy -Hx.
574
575
    + by exists x1, y1.
  * intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2  x2); split_ands; auto.
576
    + by rewrite (assoc op) -Hy -Hx.
577
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
578
Qed.
579
Lemma wand_intro_r P Q R : (P  Q)  R  P  (Q - R).
Robbert Krebbers's avatar
Robbert Krebbers committed
580
Proof.
581
  intros HPQR x n ?? x' n' ???; apply HPQR; auto.
582
  exists x, x'; split_ands; auto.
583
  eapply uPred_weaken with x n; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
Qed.
585
Lemma wand_elim_l P Q : ((P - Q)  P)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
586
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
587
588

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
589
Hint Resolve sep_mono.
590
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
591
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
592
593
594
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.
595
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')  (Q - Q').
596
Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
597
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
598
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
599

Robbert Krebbers's avatar
Robbert Krebbers committed
600
Global Instance sep_True : RightId () True%I (@uPred_sep M).
601
Proof. by intros P; rewrite comm left_id. Qed.
602
Lemma sep_elim_l P Q : (P  Q)  P.
603
Proof. by rewrite (True_intro Q) right_id. Qed.
604
Lemma sep_elim_r P Q : (P  Q)  Q.
605
Proof. by rewrite (comm ())%I; apply sep_elim_l. Qed.
606
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
607
Proof. intros ->; apply sep_elim_l. Qed.
608
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
609
610
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
611
Lemma sep_intro_True_l P Q R : True  P  R  Q  R  (P  Q).
612
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
613
Lemma sep_intro_True_r P Q R : R  P  True  Q  R  (P  Q).
614
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
615
Lemma wand_intro_l P Q R : (Q  P)  R  P  (Q - R).
616
Proof. rewrite comm; apply wand_intro_r. Qed.
617
Lemma wand_elim_r P Q : (P  (P - Q))  Q.
618
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
619
620
621
622
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.
623
Lemma sep_and P Q : (P  Q)  (P  Q).
624
Proof. auto. Qed.
625
Lemma impl_wand P Q : (P  Q)  (P - Q).
626
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Ralf Jung's avatar
Ralf Jung committed
627
628
629
630
Lemma const_elim_sep_l φ Q R : (φ  Q  R)  ( φ  Q)  R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_elim_sep_r φ Q R : (φ  Q  R)  (Q   φ)  R.
Proof. intros; apply const_elim