upred.v 44.4 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;
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
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.
58
Proof. intros HP ?; apply HP; auto. Qed.
59
60
Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
  x1  x2  n2  n1  {n2} x2  P n1 x1  P n2 x2.
61
Proof. eauto using uPred_weaken. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
63

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

(** logical entailement *)
100
101
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.
102
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
132
133
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 :=
134
135
136
137
138
139
140
  {| 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
141

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

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

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

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

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

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

233
234
235
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

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

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

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

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

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

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

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

430
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
431
432
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
433

434
435
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
436
437
438
439
440
441
442
443
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.
444
Lemma impl_entails P Q : True  (P  Q)  P  Q.
445
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
446
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
447
Proof. auto using impl_intro_l. Qed.
448

449
450
Lemma const_intro_l φ Q R : φ  (■φ  Q)  R  Q  R.
Proof. intros ? <-; auto using const_intro. Qed.
451
Lemma const_intro_r φ Q R : φ  (Q  ■φ)  R  Q  R.
452
Proof. intros ? <-; auto using const_intro. Qed.
453
454
455
456
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
457
458
Lemma const_equiv (φ : Prop) : φ  ( φ : uPred M)%I  True%I.
Proof. intros; apply (anti_symmetric _); auto using const_intro. Qed.
459
460
461
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).
462
Proof.
463
464
  refine (eq_rewrite _ (λ b, b  a)%I a b _ _); auto using eq_refl.
  intros n; solve_proper.
465
Qed.
466

467
468
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
469
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
470
Proof. auto. Qed.
471
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
472
Proof. auto. Qed.
473
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
474
Proof.
475
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
476
  apply impl_elim with P; eauto.
477
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
Lemma forall_mono {A} (P Q : A  uPred M) :
479
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
480
Proof.
481
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
482
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
Lemma exist_mono {A} (P Q : A  uPred M) :
484
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
485
Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
486
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
487
Proof. intros φ1 φ2; apply const_mono. Qed.
488
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
489
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
490
491
492
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.
493
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
494
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
495
496
497
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
498
Global Instance impl_mono' :
499
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
500
501
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
502
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
503
504
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
505
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
506
Proof. intros P1 P2; apply exist_mono. Qed.
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
533
534
535
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
536
537
538
539
540
541
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.
542
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
543
Proof.
544
  apply (anti_symmetric ()); first auto.
545
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
546
Qed.
547
548
549
550
551
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.
552
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
553
554
555
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.
556
557
558
559
560
561
562
563
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
564
565
566
567
568
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
569
570

(* BI connectives *)
571
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
572
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
  intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
574
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
576
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
577
578
Proof.
  intros P x n Hvalid; split.
579
580
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite cmra_unit_l].
Robbert Krebbers's avatar
Robbert Krebbers committed
581
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
582
Global Instance sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
583
584
Proof.
  by intros P Q x n ?; split;
585
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
586
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
587
Global Instance sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
588
589
Proof.
  intros P Q R x n ?; split.
590
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
    + by rewrite -(associative op) -Hy -Hx.
592
593
    + 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
594
    + by rewrite (associative op) -Hy -Hx.
595
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
596
Qed.
597
Lemma wand_intro_r P Q R : (P  Q)  R  P  (Q - R).
Robbert Krebbers's avatar
Robbert Krebbers committed
598
Proof.
599
  intros HPQR x n ?? x' n' ???; apply HPQR; auto.
600
  exists x, x'; split_ands; auto.
601
  eapply uPred_weaken with x n; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
602
Qed.
603
Lemma wand_elim_l P Q : ((P - Q)  P)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
605
606

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
607
Hint Resolve sep_mono.
608
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
609
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
610
611
612
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.
613
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')  (Q - Q').
614
Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
615
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
616
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
617

Robbert Krebbers's avatar
Robbert Krebbers committed
618
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
620
Lemma sep_elim_l P Q : (P  Q)  P.
621
Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
622
Lemma sep_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
624
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
625
Proof. intros ->; apply sep_elim_l. Qed.
626
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
627
628
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
629
Lemma sep_intro_True_l P Q R : True  P  R  Q  R  (P  Q).
630
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
631
Lemma sep_intro_True_r P Q R : R  P  True  Q  R  (P  Q).
632
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
633
634
Lemma wand_intro_l P Q R : (Q  P)  R  P  (Q - R).
Proof. rewrite (commutative _); apply wand_intro_r. Qed.
635
636
637
638
639
640
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.
641
Lemma sep_and P Q : (P  Q)  (P  Q).
642
Proof. auto. Qed.
643
Lemma impl_wand P Q : (P  Q)  (P - Q).
644
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
645

Robbert Krebbers's avatar
Robbert Krebbers committed
646
Global Instance sep_False : LeftAbsorb () False%I (@uPred_sep M).
647
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
648
Global Instance False_sep : RightAbsorb () False%I (@uPred_sep M).
649
Proof. intros P; apply (anti_symmetric _); auto. Qed.
650
651

Lemma sep_and_l P Q R : (P  (Q  R))  ((P  Q)  (P  R)).
652
Proof. auto. Qed.
653
654
655
Lemma sep_and_r P Q R : ((P  Q)  R)  ((P  R)  (Q  R)).
Proof. auto. Qed.
Lemma sep_or_l P Q R : (P  (Q  R))%I  ((P  Q)  (P  R))%I.
656
657
658
659
660
661
Proof.
  apply (anti_symmetric ()); last by eauto 8.
  apply wand_elim_r', or_elim; apply wand_intro_l.
  - by apply or_intro_l.
  - by apply or_intro_r.
Qed.
662
663
664
665
Lemma sep_or_r P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
Proof. by rewrite -!(commutative _ R) sep_or_l. Qed.
Lemma sep_exist_l {A} P (Q : A  uPred M) : (P   a, Q a)%I  ( a, P  Q a)%I.
Proof.
666
667
668
669
  intros; apply (anti_symmetric ()).
  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
670
671
672
673
Qed.
Lemma sep_exist_r {A} (P: A  uPred M) Q: (( a, P a)  Q)%I  ( a, P a  Q)%I.
Proof. setoid_rewrite (commutative _ _ Q); apply sep_exist_l. Qed.
Lemma sep_forall_l {A} P (Q : A  uPred M) : (P   a, Q a)  ( a, P  Q a).
674
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
675
Lemma sep_forall_r {A} (P : A  uPred M) Q : (( a, P a)  Q)  ( a, P a  Q).