logic.v 41 KB
Newer Older
1
Require Export 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
Record 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
Arguments uPred_holds {_} _ _ _ : simpl never.
14
15
Global Opaque uPred_holds.
Local Transparent uPred_holds.
16
Hint Resolve uPred_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
19

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

Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
53
54
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56

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

(** logical entailement *)
93
94
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.
95
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97

(** logical connectives *)
98
99
Program Definition uPred_const {M} (φ : Prop) : uPred M :=
  {| uPred_holds n x := match n return _ with 0 => True | _ => φ end |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Solve Obligations with done.
101
Next Obligation. intros M P x1 x2 [|n1] [|n2]; auto with lia. Qed.
102
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
103

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

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
129
130
131
132
133
  {| 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
134

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
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.
173
Next Obligation. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (unit x) |}.
179
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
180
Next Obligation. by intros; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
  intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
183
    eauto using @ra_unit_preserving, cmra_unit_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
186
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed.
189
Next Obligation. by intros M a x; exists x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  exists (a'  x2). by rewrite (associative op) -(dist_le _ _ _ _ Hx1) // Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
195
  {| uPred_holds n x := {n} a |}.
196
Solve Obligations with naive_solver eauto 2 using cmra_valid_le, cmra_valid_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
197

Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
201
202
203
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.
204
Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
207
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
208
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
Infix "∨" := uPred_or : uPred_scope.
210
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
213
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
214
215
Notation "P -★ Q" := (uPred_wand P Q)
  (at level 90, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
Notation "∀ x .. y , P" :=
217
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
Notation "∃ x .. y , P" :=
219
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
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
222
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
Notation "✓" := uPred_valid (at level 1) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
224

225
226
227
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

228
229
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
230
231
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
232
233
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_sep Ps end%I.
234
235
Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
236

237
238
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
Arguments timelessP {_} _ {_} _ _ _ _.
239
240
Class AlwaysStable {M} (P : uPred M) := always_stable : P   P.
Arguments always_stable {_} _ {_} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
241

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

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

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

(** Introduction and elimination rules *)
356
Lemma const_intro φ P : φ  P   φ.
357
Proof. by intros ?? [|?]. Qed.
358
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
359
360
361
362
Proof.
  intros HQP HQR x [|n] ??; first done.
  apply HQR; first eapply (HQP _ (S n)); eauto.
Qed.
363
Lemma True_intro P : P  True.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Proof. by apply const_intro. Qed.
365
Lemma False_elim P : False  P.
366
Proof. by intros x [|n] ?. Qed.
367
Lemma and_elim_l P Q : (P  Q)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
368
Proof. by intros x n ? [??]. Qed.
369
Lemma and_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
Proof. by intros x n ? [??]. Qed.
371
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
372
Proof. intros HQ HR x n ??; split; auto. Qed.
373
Lemma or_intro_l P Q : P  (P  Q).
374
Proof. intros x n ??; left; auto. Qed.
375
Lemma or_intro_r P Q : Q  (P  Q).
376
Proof. intros x n ??; right; auto. Qed.
377
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
378
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
379
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
380
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
381
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
Qed.
383
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
384
Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
385
Lemma forall_intro {A} P (Q : A  uPred M): ( a, P  Q a)  P  ( a, Q a).
386
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
387
Lemma forall_elim {A} (P : A  uPred M) a : ( a, P a)  P a.
Robbert Krebbers's avatar
Robbert Krebbers committed
388
Proof. intros x n ? HP; apply HP. Qed.
389
Lemma exist_intro {A} (P : A  uPred M) a : P a  ( a, P a).
390
Proof. by intros x [|n] ??; [done|exists a]. Qed.
391
Lemma exist_elim {A} (P : A  uPred M) Q : ( a, P a  Q)  ( a, P a)  Q.
392
Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
393
Lemma eq_refl {A : cofeT} (a : A) P : P  (a  a).
394
Proof. by intros x n ??; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
Lemma eq_rewrite {A : cofeT} P (Q : A  uPred M)
396
  `{HQ:∀ n, Proper (dist n ==> dist n) Q} a b : P  (a  b)  P  Q a  P  Q b.
397
398
399
Proof.
  intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
400
Lemma eq_equiv `{Empty M, !RAIdentity M} {A : cofeT} (a b : A) :
401
  True  (a  b)  a  b.
402
403
404
405
406
Proof.
  intros Hab; apply equiv_dist; intros n; apply Hab with .
  * apply cmra_valid_validN, ra_empty_valid.
  * by destruct n.
Qed.
407
Lemma iff_equiv P Q : True  (P  Q)  P  Q.
408
409
410
Proof. by intros HPQ x [|n] ?; [|split; intros; apply HPQ with x (S n)]. Qed.

(* Derived logical stuff *)
411
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
412
Proof. by rewrite and_elim_l. Qed.
413
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
414
Proof. by rewrite and_elim_r. Qed.
415
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
416
Proof. intros ->; apply or_intro_l. Qed.
417
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
418
Proof. intros ->; apply or_intro_r. Qed.
419
Lemma exist_intro' {A} P (Q : A  uPred M) a : P  Q a  P  ( a, Q a).
420
Proof. intros ->; apply exist_intro. Qed.
421

422
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
423
424
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
425

426
427
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
428
429
430
431
432
433
434
435
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.
436

437
438
439
440
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.
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.
445
446
  refine (eq_rewrite _ (λ b, b  a)%I a b _ _); auto using eq_refl.
  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
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
473
474
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
475
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
476
477
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
478
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
479
480
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
481
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
482
Proof. intros P1 P2; apply exist_mono. Qed.
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
511
512
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.
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
513
Proof.
514
  apply (anti_symmetric ()); first auto.
515
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
516
Qed.
517
518
519
520
521
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.
522
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
523
524
525
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
526
527

(* BI connectives *)
528
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
529
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
531
  intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
    eauto 7 using cmra_valid_op_l, cmra_valid_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
533
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
534
535
Proof.
  intros P x n Hvalid; split.
536
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, @ra_included_r.
537
  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Robbert Krebbers's avatar
Robbert Krebbers committed
538
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
539
Global Instance sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
Proof.
  by intros P Q x n ?; split;
542
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
543
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
Global Instance sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
545
546
Proof.
  intros P Q R x n ?; split.
547
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
548
    + by rewrite -(associative op) -Hy -Hx.
549
550
    + 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
551
    + by rewrite (associative op) -Hy -Hx.
552
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
Qed.
554
Lemma wand_intro_r P Q R : (P  Q)  R  P  (Q - R).
Robbert Krebbers's avatar
Robbert Krebbers committed
555
Proof.
556
  intros HPQR x n ?? x' n' ???; apply HPQR; auto.
557
  exists x, x'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
558
  eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Qed.
560
Lemma wand_elim_l P Q : ((P - Q)  P)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
562
563
564
565
Lemma sep_or_l_1 P Q R : (P  (Q  R))  (P  Q  P  R).
Proof. by intros x n ? (x1&x2&Hx&?&[?|?]); [left|right]; exists x1, x2. Qed.
Lemma sep_exist_l_1 {A} P (Q : A  uPred M) : (P   b, Q b)  ( b, P  Q b).
Proof. by intros x [|n] ?; [done|intros (x1&x2&?&?&[a ?]); exists a,x1,x2]. Qed.
566
567

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
568
Hint Resolve sep_mono.
569
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
570
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
571
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')  (Q - Q').
572
Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
573
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
574
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
575

Robbert Krebbers's avatar
Robbert Krebbers committed
576
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
577
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
578
Lemma sep_elim_l P Q : (P  Q)  P.
579
Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
580
Lemma sep_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
581
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
582
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
583
Proof. intros ->; apply sep_elim_l. Qed.
584
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
585
586
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.