upred.v 44.7 KB
Newer Older
1
Require Export algebra.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5
Local Hint Extern 1 (_  _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_  _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_  _) => omega.

Robbert Krebbers's avatar
Robbert Krebbers committed
6
Record uPred (M : cmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
8
  uPred_ne x1 x2 n : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  uPred_weaken x1 x2 n1 n2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
10
    uPred_holds n1 x1  x1  x2  n2  n1  {n2} x2  uPred_holds n2 x2
Robbert Krebbers's avatar
Robbert Krebbers committed
11
}.
12
Arguments uPred_holds {_} _ _ _ : simpl never.
13 14
Global Opaque uPred_holds.
Local Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
105 106 107 108 109 110 111 112
Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_or {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_impl {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
113
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Next Obligation.
115
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto.
117
  assert (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
118
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Qed.
121
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
122

Robbert Krebbers's avatar
Robbert Krebbers committed
123 124 125 126
Program Definition uPred_forall {M A} (P : A  uPred M) : uPred M :=
  {| uPred_holds n x :=  a, P a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_exist {M A} (P : A  uPred M) : uPred M :=
127 128
  {| uPred_holds n x :=  a, P a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
129

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

446 447
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
448
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
449
Proof. auto. Qed.
450
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
451
Proof. auto. Qed.
452
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
453
Proof.
454
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
455
  apply impl_elim with P; eauto.
456
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
Lemma forall_mono {A} (P Q : A  uPred M) :
458
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
459
Proof.
460
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
461
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
Lemma exist_mono {A} (P Q : A  uPred M) :
463
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
464
Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
465
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
466
Proof. intros φ1 φ2; apply const_mono. Qed.
467
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
469 470 471
Global Instance and_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
472
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
473
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
474 475 476
Global Instance or_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
477
Global Instance impl_mono' :
478
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
479 480
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
481
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
484
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
485
Proof. intros P1 P2; apply exist_mono. Qed.
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 513 514
Global Instance and_idem : Idempotent () (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_idem : Idempotent () (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_comm : Commutative () (@uPred_and M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance True_and : LeftId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_True : RightId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_or : LeftId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_False : RightId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_assoc : Associative () (@uPred_and M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Global Instance or_comm : Commutative () (@uPred_or M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance or_assoc : Associative () (@uPred_or M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516 517 518 519 520
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.
  intros P; apply (anti_symmetric ()).
  * by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  * by apply impl_intro_l; rewrite left_id.
Qed.
521
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
522
Proof.
523
  apply (anti_symmetric ()); first auto.
524
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
525
Qed.
526 527 528 529 530
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.
531
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
532 533 534
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.
535 536 537 538 539 540 541 542
Lemma and_exist_l {A} P (Q : A  uPred M) : (P   a, Q a)%I  ( a, P  Q a)%I.
Proof.
  apply (anti_symmetric ()).
  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
    by rewrite -(exist_intro a) and_elim_r.
Qed.
Ralf Jung's avatar
Ralf Jung committed
543 544 545 546 547
Lemma and_exist_r {A} P (Q : A  uPred M) : (( a, Q a)  P)%I  ( a, Q a  P)%I.
Proof.
  rewrite -(commutative _ P) and_exist_l.
  apply exist_proper=>a. by rewrite commutative.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
548 549

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

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