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

Robbert Krebbers's avatar
Robbert Krebbers committed
6
Record uPred (M : cmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  uPred_ne x1 x2 n : uPred_holds n x1  x1 ={n}= x2  uPred_holds n x2;
9
  uPred_0 x : uPred_holds 0 x;
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  uPred_weaken x1 x2 n1 n2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
11
    uPred_holds n1 x1  x1  x2  n2  n1  {n2} x2  uPred_holds n2 x2
Robbert Krebbers's avatar
Robbert Krebbers committed
12
}.
13
14
Arguments uPred_holds {_} _ _ _.
Hint Resolve uPred_0.
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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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.
      + by intros P Q Q' HP HQ x i ??; transitivity (Q i x); [apply HP|apply HQ].
    * intros n P Q HPQ x i ??; apply HPQ; auto.
    * intros P Q x i; rewrite Nat.le_0_r; intros ->; split; intros; apply uPred_0.
    * by intros c n x i ??; apply (chain_cauchy c i n).
  Qed.
  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.

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

(** functor *)
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Program Definition uPred_map {M1 M2 : cmraT} (f : M2  M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  `{! n, Proper (dist n ==> dist n) f, !CMRAMonotone f}
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}.
58
Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
59
Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2  M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  `{! n, Proper (dist n ==> dist n) f, !CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  Proper (dist n ==> dist n) (uPred_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
  by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
70
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
72
    `{!CMRAMonotone f, !CMRAMonotone g} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
73
74
  f ={n}= g  uPredC_map f ={n}= uPredC_map g.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  by intros Hfg P y n' ??; rewrite /= (dist_le _ _ _ _(Hfg y)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78

(** logical entailement *)
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q,  x n,
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  {n} x  P n x  Q n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
82

(** logical connectives *)
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Program Definition uPred_const {M} (P : Prop) : uPred M :=
84
  {| uPred_holds n x := match n return _ with 0 => True | _ => P end |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Solve Obligations with done.
86
Next Obligation. intros M P x1 x2 [|n1] [|n2]; auto with lia. Qed.
87
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
88

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

Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
110
111
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 :=
112
113
114
115
116
117
118
  {| 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
119

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
183
184
185
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
186

Robbert Krebbers's avatar
Robbert Krebbers committed
187
188
189
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
190
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Infix "∨" := uPred_or : uPred_scope.
192
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
195
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
196
197
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
198
Notation "∀ x .. y , P" :=
199
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
Notation "∃ x .. y , P" :=
201
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
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
204
Infix "≡" := uPred_eq : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Notation "✓" := uPred_valid (at level 1) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
206

207
208
209
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

210
211
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
212
213
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
214
215
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_sep Ps end%I.
216
217
Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
218

Robbert Krebbers's avatar
Robbert Krebbers committed
219
Class TimelessP {M} (P : uPred M) := timelessP x n : {1} x  P 1 x  P n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
220

Robbert Krebbers's avatar
Robbert Krebbers committed
221
Module uPred. Section uPred_logic.
222
Context {M : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
Implicit Types P Q : uPred M.
224
Implicit Types Ps Qs : list (uPred M).
225
Implicit Types A : Type.
Robbert Krebbers's avatar
Robbert Krebbers committed
226

Robbert Krebbers's avatar
Robbert Krebbers committed
227
Global Instance: PreOrder (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
228
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Global Instance: AntiSymmetric () (() : relation (uPred M)).
230
Proof. intros P Q HPQ HQP; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
Proof.
233
234
  split; [|by intros [??]; apply (anti_symmetric ())].
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
Global Instance entails_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
241
  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
242
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
243

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

(** Introduction and elimination rules *)
Robbert Krebbers's avatar
Robbert Krebbers committed
332
Lemma const_intro P (Q : Prop) : Q  P  uPred_const Q.
333
Proof. by intros ?? [|?]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Lemma const_elim (P : Prop) Q R : (P  Q  R)  (Q  uPred_const P)%I  R.
335
Proof. intros HR x [|n] ? [??]; [|apply HR]; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
337
338
Lemma True_intro P : P  True%I.
Proof. by apply const_intro. Qed.
Lemma False_elim P : False%I  P.
339
Proof. by intros x [|n] ?. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Lemma and_elim_l P Q : (P  Q)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
Proof. by intros x n ? [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
Lemma and_elim_r P Q : (P  Q)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
Proof. by intros x n ? [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R)%I.
345
Proof. intros HQ HR x n ??; split; auto. Qed.
346
347
348
349
Lemma or_intro_l P Q : P  (P  Q)%I.
Proof. intros x n ??; left; auto. Qed.
Lemma or_intro_r P Q : Q  (P  Q)%I.
Proof. intros x n ??; right; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
350
Lemma or_elim R P Q : P  R  Q  R  (P  Q)%I  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
Lemma impl_intro P Q R : (R  P)%I  Q  R  (P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
354
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Lemma impl_elim P Q R : P  (Q  R)%I  P  Q  P  R.
357
Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
Lemma forall_intro P `(Q: A  uPred M): ( a, P  Q a)  P  ( a, Q a)%I.
359
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
360
Lemma forall_elim `(P : A  uPred M) a : ( a, P a)%I  P a.
Robbert Krebbers's avatar
Robbert Krebbers committed
361
Proof. intros x n ? HP; apply HP. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Lemma exist_intro `(P : A  uPred M) a : P a  ( a, P a)%I.
363
Proof. by intros x [|n] ??; [done|exists a]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Lemma exist_elim `(P : A  uPred M) Q : ( a, P a  Q)  ( a, P a)%I  Q.
365
Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
Lemma eq_refl {A : cofeT} (a : A) P : P  (a  a)%I.
367
Proof. by intros x n ??; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
368
Lemma eq_rewrite {A : cofeT} P (Q : A  uPred M)
369
370
371
372
373
    `{HQ : ! n, Proper (dist n ==> dist n) Q} a b :
  P  (a  b)%I  P  Q a  P  Q b.
Proof.
  intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
374
Lemma eq_equiv `{Empty M, !RAIdentity M} {A : cofeT} (a b : A) :
375
376
377
378
379
380
  True%I  (a  b : uPred M)%I  a  b.
Proof.
  intros Hab; apply equiv_dist; intros n; apply Hab with .
  * apply cmra_valid_validN, ra_empty_valid.
  * by destruct n.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
381
Lemma iff_equiv P Q : True%I  (P  Q)%I  P  Q.
382
383
384
Proof. by intros HPQ x [|n] ?; [|split; intros; apply HPQ with x (S n)]. Qed.

(* Derived logical stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
385
Lemma and_elim_l' P Q R : P  R  (P  Q)%I  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
Proof. by rewrite ->and_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
Lemma and_elim_r' P Q R : Q  R  (P  Q)%I  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
388
Proof. by rewrite ->and_elim_r. Qed.
389
390
391
392
393
394
Lemma or_intro_l' P Q R : P  Q  P  (Q  R)%I.
Proof. intros ->; apply or_intro_l. Qed.
Lemma or_intro_r' P Q R : P  R  P  (Q  R)%I.
Proof. intros ->; apply or_intro_r. Qed.
Lemma exist_intro' P `(Q : A  uPred M) a : P  Q a  P  ( a, Q a)%I.
Proof. intros ->; apply exist_intro. Qed.
395

396
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
398
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
399

Robbert Krebbers's avatar
Robbert Krebbers committed
400
Global Instance and_idem : Idempotent () (@uPred_and M).
401
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
402
Global Instance or_idem : Idempotent () (@uPred_or M).
403
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Global Instance and_comm : Commutative () (@uPred_and M).
405
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
406
Global Instance True_and : LeftId () True%I (@uPred_and M).
407
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
408
Global Instance and_True : RightId () True%I (@uPred_and M).
409
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
411
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
413
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
415
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
416
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
417
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
418
Global Instance False_or : LeftId () False%I (@uPred_or M).
419
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
Global Instance or_False : RightId () False%I (@uPred_or M).
421
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
422
Global Instance and_assoc : Associative () (@uPred_and M).
423
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
424
Global Instance or_comm : Commutative () (@uPred_or M).
425
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
Global Instance or_assoc : Associative () (@uPred_or M).
427
428
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
429
Lemma const_mono (P Q: Prop) : (P  Q)  uPred_const P  @uPred_const M Q.
430
431
Proof.
  intros; rewrite <-(left_id True%I _ (uPred_const P)).
Robbert Krebbers's avatar
Robbert Krebbers committed
432
  eauto using const_elim, const_intro.
433
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
434
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
435
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
436
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
437
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
438
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')%I  (Q  Q')%I.
439
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
441
  intros HP HQ'; apply impl_intro; rewrite <-HQ'.
  transitivity ((P  P')  P)%I; eauto using impl_elim.
442
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Lemma forall_mono {A} (P Q : A  uPred M) :
444
445
  ( a, P a  Q a)  ( a, P a)%I  ( a, Q a)%I.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
446
447
  intros HPQ. apply forall_intro; intros a; rewrite <-(HPQ a).
  apply forall_elim.
448
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
Lemma exist_mono {A} (P Q : A  uPred M) :
450
451
  ( a, P a  Q a)  ( a, P a)%I  ( a, Q a)%I.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
  intros HPQ. apply exist_elim; intros a; rewrite ->(HPQ a); apply exist_intro.
453
454
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
455
456
457
458
459
460
461
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
Proof. intros P Q; apply const_mono. Qed.
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
462
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
465
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
466
467
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
468
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
469
Proof. intros P1 P2; apply exist_mono. Qed.
470

Robbert Krebbers's avatar
Robbert Krebbers committed
471
472
473
Lemma equiv_eq {A : cofeT} P (a b : A) : a  b  P  (a  b)%I.
Proof. intros ->; apply eq_refl. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : (a  b)%I  (b  a : uPred M)%I.
474
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
  refine (eq_rewrite _ (λ b, b  a)%I a b _ _); auto using eq_refl.
476
477
  intros n; solve_proper.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
478
479

(* BI connectives *)
Robbert Krebbers's avatar
Robbert Krebbers committed
480
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
481
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
482
483
  intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
    eauto 7 using cmra_valid_op_l, cmra_valid_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
484
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
485
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
486
487
Proof.
  intros P x n Hvalid; split.
488
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, @ra_included_r.
489
  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Robbert Krebbers's avatar
Robbert Krebbers committed
490
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
491
Global Instance sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
492
493
Proof.
  by intros P Q x n ?; split;
494
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
495
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
496
Global Instance sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
497
498
Proof.
  intros P Q R x n ?; split.
499
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
    + by rewrite -(associative op) -Hy -Hx.
501
502
    + 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
503
    + by rewrite (associative op) -Hy -Hx.
504
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
505
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
506
Lemma wand_intro P Q R : (R  P)%I  Q  R  (P - Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
507
508
Proof.
  intros HPQ x n ?? x' n' ???; apply HPQ; auto.
509
  exists x, x'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
  eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
511
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
Lemma wand_elim P Q : ((P - Q)  P)%I  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
513
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
514
Lemma or_sep_distr P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
Proof.
516
517
  split; [by intros (x1&x2&Hx&[?|?]&?); [left|right]; exists x1, x2|].
  intros [(x1&x2&Hx&?&?)|(x1&x2&Hx&?&?)]; exists x1, x2; split_ands;
Robbert Krebbers's avatar
Robbert Krebbers committed
518
519
    first [by left | by right | done].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
Lemma exist_sep_distr `(P : A  uPred M) Q :
Robbert Krebbers's avatar
Robbert Krebbers committed
521
522
  (( b, P b)  Q)%I  ( b, P b  Q)%I.
Proof.
523
  intros x [|n]; [done|split; [by intros (x1&x2&Hx&[a ?]&?); exists a,x1,x2|]].
524
  intros [a (x1&x2&Hx&?&?)]; exists x1, x2; split_ands; by try exists a.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
Qed.
526
527

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
528
529
530
531
Hint Resolve sep_mono.
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')%I  (Q - Q')%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
Proof. intros HP HQ; apply wand_intro; rewrite ->HP, <-HQ; apply wand_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
533
534
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
535

Robbert Krebbers's avatar
Robbert Krebbers committed
536
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
538
Lemma sep_elim_l P Q : (P  Q)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
539
Proof. by rewrite ->(True_intro Q), (right_id _ _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
Lemma sep_elim_r P Q : (P  Q)%I  Q.
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
542
543
544
545
546
Lemma sep_elim_l' P Q R : P  R  (P  Q)%I  R.
Proof. intros ->; apply sep_elim_l. Qed.
Lemma sep_elim_r' P Q R : Q  R  (P  Q)%I  R.
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
547
Lemma sep_and P Q : (P  Q)%I  (P  Q)%I.
548
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
549
Global Instance sep_False : LeftAbsorb () False%I (@uPred_sep M).
550
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
551
Global Instance False_sep : RightAbsorb () False%I (@uPred_sep M).
552
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
554
555
Lemma impl_wand P Q : (P  Q)%I  (P - Q)%I.
Proof. apply wand_intro, impl_elim with P; auto. Qed.
Lemma and_sep_distr P Q R : ((P  Q)  R)%I  ((P  R)  (Q  R))%I.
556
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
557
Lemma forall_sep_distr `(P : A  uPred M) Q :
558
  (( a, P a)  Q)%I  ( a, P a  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Proof. by apply forall_intro; intros a; rewrite ->forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
560
561

(* Later *)
Robbert Krebbers's avatar
Robbert Krebbers committed
562
Lemma later_mono P Q : P  Q  ( P)%I  ( Q)%I.
563
Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_valid_S]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
564
Lemma later_intro P : P  ( P)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
565
566
Proof.
  intros x [|n] ??; simpl in *; [done|].
567
  apply uPred_weaken with x (S n); eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
568
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
569
Lemma lub P : ( P  P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
570
571
Proof.
  intros x n ? HP; induction n as [|n IH]; [by apply HP|].
Robbert Krebbers's avatar
Robbert Krebbers committed
572
  apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
574
Lemma later_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
Proof. by intros x [|n]; split. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
576
Lemma later_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
Proof. intros x [|n]; simpl; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed