logic.v 37.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
Arguments uPred_holds {_} _ _ _ : simpl never.
14
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
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.
40
      + by intros P Q Q' HP HQ x i ??; transitivity (Q i x);[apply HP|apply HQ].
41
    * intros n P Q HPQ x i ??; apply HPQ; auto.
42
    * intros P Q x i; rewrite Nat.le_0_r=> ->; split; intros; apply uPred_0.
43
44
45
46
47
48
    * 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; 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.
75
76
  by intros Hfg P y n' ??;
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
79

(** logical entailement *)
80
81
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.
82
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
83
84

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

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

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

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

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

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

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

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

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

212
213
214
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

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

224
225
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
Arguments timelessP {_} _ {_} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
226

Robbert Krebbers's avatar
Robbert Krebbers committed
227
Module uPred. Section uPred_logic.
228
Context {M : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Implicit Types P Q : uPred M.
230
Implicit Types Ps Qs : list (uPred M).
231
Implicit Types A : Type.
232
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
233
Arguments uPred_holds {_} !_ _ _ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
234

235
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
236
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
237
Global Instance: AntiSymmetric () (@uPred_entails M).
238
Proof. intros P Q HPQ HQP; split; auto. Qed.
239
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
Proof.
241
  split; [|by intros [??]; apply (anti_symmetric ())].
242
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
Global Instance entails_proper :
245
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
246
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
248
249
  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
250
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
251

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

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

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

406
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
407
408
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
409

410
411
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
412
413
414
415
416
417
418
419
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.
420

Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
423
424
Lemma const_elim_l (P : Prop) Q R : (P  Q  R)  ( P  Q)  R.
Proof. intros; apply const_elim with P; eauto. Qed.
Lemma const_elim_r (P : Prop) Q R : (P  Q  R)  (Q   P)  R.
Proof. intros; apply const_elim with P; eauto. Qed.
425
426
427
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).
428
Proof.
429
430
  refine (eq_rewrite _ (λ b, b  a)%I a b _ _); auto using eq_refl.
  intros n; solve_proper.
431
Qed.
432
433
434

Lemma const_mono (P Q: Prop) : (P  Q)   P   Q.
Proof. intros; apply const_elim with P; eauto using const_intro. Qed.
435
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
436
Proof. auto. Qed.
437
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
438
Proof. auto. Qed.
439
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
440
Proof.
441
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
442
  apply impl_elim with P; eauto.
443
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
444
Lemma forall_mono {A} (P Q : A  uPred M) :
445
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
446
Proof.
447
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
448
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
449
Lemma exist_mono {A} (P Q : A  uPred M) :
450
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
451
Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
452
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
Robbert Krebbers's avatar
Robbert Krebbers committed
453
Proof. intros P Q; apply const_mono. Qed.
454
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
455
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
456
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
459
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
460
461
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
462
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
463
464
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
465
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
466
Proof. intros P1 P2; apply exist_mono. Qed.
467

468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
Global Instance and_idem : Idempotent () (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_idem : Idempotent () (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_comm : Commutative () (@uPred_and M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance True_and : LeftId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_True : RightId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_or : LeftId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_False : RightId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_assoc : Associative () (@uPred_and M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Global Instance or_comm : Commutative () (@uPred_or M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance or_assoc : Associative () (@uPred_or M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
497
Proof.
498
  apply (anti_symmetric ()); first auto.
499
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
500
Qed.
501
502
503
504
505
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.
506
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
507
508
509
Qed.
Lemma and_or_r P Q R : ((P  Q)  R)%I  (P  R  Q  R)%I.
Proof. by rewrite -!(commutative _ R) and_or_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
511

(* BI connectives *)
512
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
513
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
514
515
  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
516
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
517
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
518
519
Proof.
  intros P x n Hvalid; split.
520
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, @ra_included_r.
521
  * by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Robbert Krebbers's avatar
Robbert Krebbers committed
522
Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
523
Global Instance sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
Proof.
  by intros P Q x n ?; split;
526
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
527
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
528
Global Instance sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
529
530
Proof.
  intros P Q R x n ?; split.
531
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
    + by rewrite -(associative op) -Hy -Hx.
533
534
    + 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
535
    + by rewrite (associative op) -Hy -Hx.
536
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Qed.
538
Lemma wand_intro P Q R : (P  Q)  R  P  (Q - R).
Robbert Krebbers's avatar
Robbert Krebbers committed
539
Proof.
540
  intros HPQR x n ?? x' n' ???; apply HPQR; auto.
541
  exists x, x'; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
542
  eapply uPred_weaken with x n; eauto using cmra_valid_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
543
Qed.
544
Lemma wand_elim_l P Q : ((P - Q)  P)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
546
547
548
549
Lemma sep_or_l_1 P Q R : (P  (Q  R))  (P  Q  P  R).
Proof. by intros x n ? (x1&x2&Hx&?&[?|?]); [left|right]; exists x1, x2. Qed.
Lemma sep_exist_l_1 {A} P (Q : A  uPred M) : (P   b, Q b)  ( b, P  Q b).
Proof. by intros x [|n] ?; [done|intros (x1&x2&?&?&[a ?]); exists a,x1,x2]. Qed.
550
551

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
552
Hint Resolve sep_mono.
553
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
555
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')  (Q - Q').
556
Proof. intros HP HQ; apply wand_intro; rewrite HP -HQ; apply wand_elim_l. Qed.
557
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
558
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
559

Robbert Krebbers's avatar
Robbert Krebbers committed
560
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
561
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
562
Lemma sep_elim_l P Q : (P  Q)  P.
563
Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
564
Lemma sep_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
565
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
566
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
567
Proof. intros ->; apply sep_elim_l. Qed.
568
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
569
570
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
571
572
573
574
575
576
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.
577
Lemma sep_and P Q : (P  Q)  (P  Q).
578
Proof. auto. Qed.
579
580
581
Lemma impl_wand P Q : (P  Q)  (P - Q).
Proof. apply wand_intro, impl_elim with P; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
582
Global Instance sep_False : LeftAbsorb () False%I (@uPred_sep M).
583
Proof. intros P; apply (anti_symmetric _); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
Global Instance False_sep : RightAbsorb () False%I (@uPred_sep M).
585
Proof. intros P; apply (anti_symmetric _); auto. Qed.
586
587

Lemma sep_and_l P Q R : (P  (Q  R))  ((P  Q)  (P  R)).
588
Proof. auto. Qed.
589
590
591
592
593
594
595
596
597
598
599
600
601
602
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.
Proof. apply (anti_symmetric ()); eauto 10 using sep_or_l_1. Qed.
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.
  intros; apply (anti_symmetric ()); eauto using sep_exist_l_1.
  apply exist_elim=> a; apply sep_mono; auto using exist_intro.
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).
603
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
604
Lemma sep_forall_r {A} (P : A  uPred M) Q : (( a, P a)  Q)  ( a, P a  Q).
605
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
606
607

(* Later *)
608
Lemma later_mono P Q : P  Q   P   Q.
609
Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_valid_S]. Qed.
610
Lemma later_intro P : P   P.
Robbert Krebbers's avatar
Robbert Krebbers committed
611
612
Proof.
  intros x [|n] ??; simpl in *; [done|].
613
  apply uPred_weaken with x (S n); eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
Qed.
615
Lemma lub P : ( P  P)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
617
Proof.
  intros x n ? HP; induction n as [|n IH]; [by apply HP|].
Robbert Krebbers's avatar
Robbert Krebbers committed
618
  apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
Lemma later_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
Proof. by intros x [|n]; split. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
Lemma later_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Proof. intros x [|n]; simpl; tauto. Qed.
624
Lemma later_forall {A} (P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
Proof. by intros x [|n]. Qed.
626
Lemma later_exist {A} (P : A  uPred M) : ( a,  P a)  (  a, P a).
627
Proof. by intros x [|[|n]]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
628
Lemma later_exist' `{Inhabited A} (P : A  uPred M) :
629
  (  a, P a)%I  ( a,  P a)%I.
630
Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
631
Lemma later_sep P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
632
633
Proof.
  intros x n ?; split.
634
  * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
Robbert Krebbers's avatar
Robbert Krebbers committed
635
    destruct (cmra_extend_op n x x1 x2)
636
      as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_valid_S; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
Robbert Krebbers's avatar
Robbert Krebbers committed
638
  * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
639
    exists x1, x2; eauto using dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
640
641
Qed.

642
(* Later derived *)
643
Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M).
Robbert Krebbers's avatar
Robbert Krebbers committed
644
Proof. intros P Q; apply later_mono. Qed.
645
Lemma later_impl P Q :  (P  Q)  ( P   Q).
646
Proof.
647
  apply impl_intro_l; rewrite -later_and.
Robbert Krebbers's avatar
Robbert Krebbers committed
648
  apply later_mono, impl_elim with P; auto.
649
Qed.
650
Lemma later_wand P Q :  (P - Q)  ( P -  Q).
651
Proof. apply wand_intro; rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
652

Robbert Krebbers's avatar
Robbert Krebbers committed
653
(* Always *)
654
Lemma always_const (P : Prop) : (  P : uPred M)%I  ( P)%I.
655
Proof. done. Qed.
656
Lemma always_elim P :  P  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
657
Proof.
658
659
  intros x n ??; apply uPred_weaken with (unit x) n;
    eauto using @ra_included_unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
660
Qed.