logic.v 42.8 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.

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
57
58
59
60
61
62
63
64
65
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 :
  P1 ={n}= P2  {n} x  P1 n x  P2 n x.
Proof.
  intros HP ?. apply HP; by auto.
Qed.
Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
  x1  x2  n2  n1  {n2} x2  P n1 x1  P n2 x2.
Proof.
  intros; eauto using uPred_weaken.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
67

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

(** logical entailement *)
104
105
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.
106
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108

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

Robbert Krebbers's avatar
Robbert Krebbers committed
115
116
117
118
119
120
121
122
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
123
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Next Obligation.
125
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
  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).
128
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Qed.
131
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
Next Obligation. naive_solver eauto 2 with lia. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
134
135
136
137
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 :=
138
139
140
141
142
143
144
  {| 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
145

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

Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
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
152
Next Obligation.
153
  by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Qed.
155
Next Obligation. by intros M P Q x; exists x, x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  assert ( x2', y ={n2}= x1  x2'  x2  x2') as (x2'&Hy&?).
159
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using @ra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
    apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
161
162
163
  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
164
165
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
168
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
Next Obligation.
170
  intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
  by rewrite (dist_le _ _ _ n2 Hx).
Qed.
174
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
177
  intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
  apply uPred_weaken with (x1  x3) n3;
178
    eauto using cmra_valid_included, @ra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
181
182
183
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.
184
Next Obligation. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
  intros M P x1 x2 [|n1] [|n2]; eauto using uPred_weaken, cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
187
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (unit x) |}.
190
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
191
Next Obligation. by intros; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
  intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
194
    eauto using @ra_unit_preserving, cmra_unit_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
197
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
198
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed.
200
Next Obligation. by intros M a x; exists x. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
  intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  exists (a'  x2). by rewrite (associative op) -(dist_le _ _ _ _ Hx1) // Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  {| uPred_holds n x := {n} a |}.
207
Solve Obligations with naive_solver eauto 2 using cmra_valid_le, cmra_valid_0.
Robbert Krebbers's avatar
Robbert Krebbers committed
208

Robbert Krebbers's avatar
Robbert Krebbers committed
209
210
211
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
212
213
214
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.
215
Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
218
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
219
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
Infix "∨" := uPred_or : uPred_scope.
221
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
224
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
225
226
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
227
Notation "∀ x .. y , P" :=
228
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Notation "∃ x .. y , P" :=
230
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
232
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
233
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
Notation "✓" := uPred_valid (at level 1) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
235

236
237
238
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

239
240
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
241
242
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
243
244
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_sep Ps end%I.
245
246
Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
247

248
249
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
Arguments timelessP {_} _ {_} _ _ _ _.
250
251
Class AlwaysStable {M} (P : uPred M) := always_stable : P   P.
Arguments always_stable {_} _ {_} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
252

Robbert Krebbers's avatar
Robbert Krebbers committed
253
Module uPred. Section uPred_logic.
254
Context {M : cmraT}.
255
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
Implicit Types P Q : uPred M.
257
Implicit Types Ps Qs : list (uPred M).
258
Implicit Types A : Type.
259
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
260
Arguments uPred_holds {_} !_ _ _ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
261

262
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
264
Global Instance: AntiSymmetric () (@uPred_entails M).
265
Proof. intros P Q HPQ HQP; split; auto. Qed.
266
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
Proof.
268
  split; [|by intros [??]; apply (anti_symmetric ())].
269
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Global Instance entails_proper :
272
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
273
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
274
275
276
  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
277
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
278

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

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

(* Derived logical stuff *)
422
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
423
Proof. by rewrite and_elim_l. Qed.
424
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
425
Proof. by rewrite and_elim_r. Qed.
426
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
427
Proof. intros ->; apply or_intro_l. Qed.
428
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
429
Proof. intros ->; apply or_intro_r. Qed.
430
Lemma exist_intro' {A} P (Q : A  uPred M) a : P  Q a  P  ( a, Q a).
431
Proof. intros ->; apply exist_intro. Qed.
432

433
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
434
435
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
436

437
438
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
439
440
441
442
443
444
445
446
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.
447
448
449
450
451
452
453
454
455
Lemma impl_entails P Q : True  (P  Q)  P  Q.
Proof.
  intros H; eapply impl_elim; last reflexivity. rewrite -H.
  by apply True_intro.
Qed.
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
Proof.
  intros H; apply impl_intro_l. by rewrite -H and_elim_l.
Qed.
456

457
458
459
460
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.
461
462
463
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).
464
Proof.
465
466
  refine (eq_rewrite _ (λ b, b  a)%I a b _ _); auto using eq_refl.
  intros n; solve_proper.
467
Qed.
468

469
470
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
471
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
472
Proof. auto. Qed.
473
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
474
Proof. auto. Qed.
475
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
476
Proof.
477
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
478
  apply impl_elim with P; eauto.
479
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
480
Lemma forall_mono {A} (P Q : A  uPred M) :
481
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
482
Proof.
483
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
484
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
Lemma exist_mono {A} (P Q : A  uPred M) :
486
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
487
Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
488
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
489
Proof. intros φ1 φ2; apply const_mono. Qed.
490
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
491
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
492
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
493
494
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
495
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
496
497
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
498
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
499
500
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
501
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
502
Proof. intros P1 P2; apply exist_mono. Qed.
503

504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
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.
533
Proof.
534
  apply (anti_symmetric ()); first auto.
535
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
536
Qed.
537
538
539
540
541
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.
542
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
543
544
545
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
546
547

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
596
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
597
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
598
Lemma sep_elim_l P Q : (P  Q)  P.
599
Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
600
Lemma sep_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
602
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
603
Proof. intros ->; apply sep_elim_l. Qed.
604
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
605
606
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
607
608
Lemma wand_intro_l P Q R : (Q  P)  R  P  (Q - R).
Proof. rewrite (commutative _); apply wand_intro_r. Qed.
609
610
611
612
613
614
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.
615
Lemma sep_and P Q : (P  Q)