upred.v 44.3 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
214
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
215
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
Infix "∨" := uPred_or : uPred_scope.
217
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
220
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
221
222
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
223
Notation "∀ x .. y , P" :=
224
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Notation "∃ x .. y , P" :=
226
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
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
229
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
Notation "✓" := uPred_valid (at level 1) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
231

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma sep_and_l P Q R : (P  (Q  R))  ((P  Q)  (P  R)).
651
Proof. auto. Qed.
652
653
654
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.
655
656
657
658
659
660
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.
661
662
663
664
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.
665
666
667
668
  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.
669
670
671
672
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).
673
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
674
Lemma sep_forall_r {A} (P : A  uPred M) Q : (( a, P a)  Q)  ( a, P a  Q).
675
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.