logic.v 40.6 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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Program Definition uPred_map {M1 M2 : cmraT} (f : M2  M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  `{! n, Proper (dist n ==> dist n) f, !CMRAMonotone f}
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
60
Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
61
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2  M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  `{! n, Proper (dist n ==> dist n) f, !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.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
74
    `{!CMRAMonotone f, !CMRAMonotone g} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
75
76
  f ={n}= g  uPredC_map f ={n}= uPredC_map g.
Proof.
77
78
  by intros Hfg P y n' ??;
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81

(** logical entailement *)
82
83
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.
84
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
85
86

(** logical connectives *)
87
88
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
89
Solve Obligations with done.
90
Next Obligation. intros M P x1 x2 [|n1] [|n2]; auto with lia. Qed.
91
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
92

Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
99
100
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
101
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Next Obligation.
103
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
  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).
106
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Qed.
109
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
Next Obligation. naive_solver eauto 2 with lia. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
114
115
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 :=
116
117
118
119
120
121
122
  {| 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
123

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

Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
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
130
Next Obligation.
131
  by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Qed.
133
Next Obligation. by intros M P Q x; exists x, x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  assert ( x2', y ={n2}= x1  x2'  x2  x2') as (x2'&Hy&?).
137
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using @ra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
    apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
139
140
141
  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
142
143
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
146
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Next Obligation.
148
  intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
  by rewrite (dist_le _ _ _ n2 Hx).
Qed.
152
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
  intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
  apply uPred_weaken with (x1  x3) n3;
156
    eauto using cmra_valid_included, @ra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
158
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
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.
162
Next Obligation. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (unit x) |}.
168
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
169
Next Obligation. by intros; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
172
    eauto using @ra_unit_preserving, cmra_unit_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
174
Qed.

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

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

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

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

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

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

240
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
241
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
242
Global Instance: AntiSymmetric () (@uPred_entails M).
243
Proof. intros P Q HPQ HQP; split; auto. Qed.
244
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
Proof.
246
  split; [|by intros [??]; apply (anti_symmetric ())].
247
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
Global Instance entails_proper :
250
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
251
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
  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
255
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256

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

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

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

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

415
416
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
417
418
419
420
421
422
423
424
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.
425

426
427
428
429
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.
430
431
432
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).
433
Proof.
434
435
  refine (eq_rewrite _ (λ b, b  a)%I a b _ _); auto using eq_refl.
  intros n; solve_proper.
436
Qed.
437

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

473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
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.
502
Proof.
503
  apply (anti_symmetric ()); first auto.
504
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
505
Qed.
506
507
508
509
510
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.
511
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
512
513
514
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
515
516

(* BI connectives *)
517
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
518
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
519
520
  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
521
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
522
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
523
524
Proof.
  intros P x n Hvalid; split.
525
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, @ra_included_r.
526
  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Robbert Krebbers's avatar
Robbert Krebbers committed
527
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
528
Global Instance sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
529
530
Proof.
  by intros P Q x n ?; split;
531
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
532
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
533
Global Instance sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
534
535
Proof.
  intros P Q R x n ?; split.
536
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
    + by rewrite -(associative op) -Hy -Hx.
538
539
    + 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
540
    + by rewrite (associative op) -Hy -Hx.
541
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
542
Qed.
543
Lemma wand_intro_r P Q R : (P  Q)  R  P  (Q - R).
Robbert Krebbers's avatar
Robbert Krebbers committed
544
Proof.
545
  intros HPQR x n ?? x' n' ???; apply HPQR; auto.
546
  exists x, x'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
547
  eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
548
Qed.
549
Lemma wand_elim_l P Q : ((P - Q)  P)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
550
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
551
552
553
554
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.
555
556

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Hint Resolve sep_mono.
558
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
560
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')  (Q - Q').
561
Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
562
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
564

Robbert Krebbers's avatar
Robbert Krebbers committed
565
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
566
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
567
Lemma sep_elim_l P Q : (P  Q)  P.
568
Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
569
Lemma sep_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
570
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
571
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
572
Proof. intros ->; apply sep_elim_l. Qed.
573
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
574
575
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
576
577
Lemma wand_intro_l P Q R : (Q  P)  R  P  (Q - R).
Proof. rewrite (commutative _); apply wand_intro_r. Qed.
578
579
580
581
582
583
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.
584
Lemma sep_and P Q : (P  Q)  (P  Q).
585
Proof. auto. Qed.
586
Lemma impl_wand P Q : (P  Q)  (P - Q).
587
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
588

Robbert Krebbers's avatar
Robbert Krebbers committed
589
Global Instance sep_False : LeftAbsorb () False%I (@uPred_sep M).
590
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
Global Instance False_sep : RightAbsorb () False%I (@uPred_sep M).
592
Proof. intros P; apply (anti_symmetric _); auto. Qed.