logic.v 34.7 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

Robbert Krebbers's avatar
Robbert Krebbers committed
18
Instance uPred_equiv (M : cmraT) : Equiv (uPred M) := λ P Q,  x n,
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  {n} x  P n x  Q n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Instance uPred_dist (M : cmraT) : Dist (uPred M) := λ n P Q,  x n',
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  n'  n  {n'} x  P n' x  Q n' x.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Program Instance uPred_compl (M : cmraT) : Compl (uPred M) := λ c,
23
  {| uPred_holds n x := c n n x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
Next Obligation. by intros M c x y n ??; simpl in *; apply uPred_ne with x. Qed.
25
Next Obligation. by intros M c x; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Next Obligation.
27
  intros M c x1 x2 n1 n2 ????; simpl in *.
28
  apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Instance uPred_cofe (M : cmraT) : Cofe (uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
Proof.
  split.
  * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
34
    intros HPQ x n ?; apply HPQ with n; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
39
  * 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.
40
41
  * 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).
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
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.
47
Canonical Structure uPredC (M : cmraT) : cofeT := CofeT (uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49

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

(** logical entailement *)
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q,  x n,
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  {n} x  P n x  Q n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
106
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 :=
107
108
109
110
111
112
113
  {| 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
114

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
178
179
180
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
181

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

202
203
204
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
216
Module uPred. Section uPred_logic.
217
Context {M : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
Implicit Types P Q : uPred M.
219
Implicit Types Ps Qs : list (uPred M).
220
Implicit Types A : Type.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

Robbert Krebbers's avatar
Robbert Krebbers committed
222
Global Instance: PreOrder (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
223
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
224
Global Instance: AntiSymmetric () (() : relation (uPred M)).
225
Proof. intros P Q HPQ HQP; split; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
Proof.
228
229
  split; [|by intros [??]; apply (anti_symmetric ())].
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
Global Instance entails_proper :
Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
  intros P1 P2 HP Q1 Q2 HQ; rewrite equiv_spec in HP, HQ; split; intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
237
  * by rewrite (proj2 HP), <-(proj1 HQ).
  * by rewrite (proj1 HP), <-(proj2 HQ).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
238

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

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

390
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
391
392
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
393

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

Robbert Krebbers's avatar
Robbert Krebbers committed
423
Lemma const_mono (P Q: Prop) : (P  Q)  uPred_const P  @uPred_const M Q.
424
425
Proof.
  intros; rewrite <-(left_id True%I _ (uPred_const P)).
Robbert Krebbers's avatar
Robbert Krebbers committed
426
  eauto using const_elim, const_intro.
427
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
428
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
429
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')%I  (Q  Q')%I.
431
Proof. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
432
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')%I  (Q  Q')%I.
433
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
434
435
  intros HP HQ'; apply impl_intro; rewrite <-HQ'.
  transitivity ((P  P')  P)%I; eauto using impl_elim.
436
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
437
Lemma forall_mono {A} (P Q : A  uPred M) :
438
439
  ( a, P a  Q a)  ( a, P a)%I  ( a, Q a)%I.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
440
441
  intros HPQ. apply forall_intro; intros a; rewrite <-(HPQ a).
  apply forall_elim.
442
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Lemma exist_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
  intros HPQ. apply exist_elim; intros a; rewrite (HPQ a); apply exist_intro.
447
448
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
449
450
451
452
453
454
455
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' :
456
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
459
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
460
461
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
462
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
463
Proof. intros P1 P2; apply exist_mono. Qed.
464

Robbert Krebbers's avatar
Robbert Krebbers committed
465
466
467
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.
468
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
  refine (eq_rewrite _ (λ b, b  a)%I a b _ _); auto using eq_refl.
470
471
  intros n; solve_proper.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
472
473

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

(* Derived BI Stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
525
526
527
528
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.
529
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
  intros HP HQ; apply wand_intro; rewrite HP, <-HQ; apply wand_elim.
531
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
534

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

(* Later *)
Robbert Krebbers's avatar
Robbert Krebbers committed
561
Lemma later_mono P Q : P  Q  ( P)%I  ( Q)%I.
562
Proof. intros HP x [|n] ??; [done|apply HP; auto using cmra_valid_S]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Lemma later_intro P : P  ( P)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
564
565
Proof.
  intros x [|n] ??; simpl in *; [done|].
Robbert Krebbers's avatar
Robbert Krebbers committed
566
  apply uPred_weaken with x (S n); auto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
567
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
568
Lemma lub P : ( P  P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
569
570
Proof.
  intros x n ? HP; induction n as [|n IH]; [by apply HP|].
Robbert Krebbers's avatar
Robbert Krebbers committed
571
  apply HP, IH, uPred_weaken with x (S n); eauto using cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
572
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
573
Lemma later_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
574
Proof. by intros x [|n]; split. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
Lemma later_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
576
Proof. intros x [|n]; simpl; tauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
Lemma later_forall `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
578
Proof. by intros x [|n]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
579
Lemma later_exist `(P : A  uPred M) : ( a,  P a)%I  (  a, P a)%I.
580
Proof. by intros x [|[|n]]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
581
Lemma later_exist' `{Inhabited A} (P : A  uPred M) :
582
  (  a, P a)%I  ( a,  P a)%I.
583
Proof. intros x [|[|n]]; split; done || by exists inhabitant; simpl. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
584
Lemma later_sep P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
586
Proof.
  intros x n ?; split.
587
  * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
Robbert Krebbers's avatar
Robbert Krebbers committed
588
    destruct (cmra_extend_op n x x1 x2)
Robbert Krebbers's avatar
Robbert Krebbers committed
589
      as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
590
    exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
Robbert Krebbers's avatar
Robbert Krebbers committed
591
  * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
592
    exists x1, x2; eauto using (dist_S (A:=M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
593
594
Qed.

595
(* Later derived *)
Robbert Krebbers's avatar
Robbert Krebbers committed
596
597
598
Global Instance later_mono' : Proper (() ==> ()) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
Lemma later_impl P Q : ( (P  Q))%I  ( P   Q)%I.
599
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
600
601
  apply impl_intro; rewrite <-later_and.
  apply later_mono, impl_elim with P; auto.
602
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
603
604
Lemma later_wand P Q : ( (P - Q))%I  ( P -  Q)%I.
Proof. apply wand_intro; rewrite <-later_sep; apply later_mono, wand_elim. Qed.
605

Robbert Krebbers's avatar
Robbert Krebbers committed
606
(* Always *)
Robbert Krebbers's avatar
Robbert Krebbers committed
607
Lemma always_const (P : Prop) : ( uPred_const P : uPred M)%I  uPred_const P.
608
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
609
Lemma always_elim P : ( P)%I  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
610
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
611
  intros x n ??; apply uPred_weaken with (unit x) n;auto using ra_included_unit.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
Lemma always_intro P Q : ( P)%I  Q  ( P)%I  ( Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
615
616
617
Proof.
  intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_valid.
  by rewrite ra_unit_idempotent.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
618
Lemma always_and P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
Lemma always_or P Q : ( (P  Q))%I  ( P   Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
Lemma always_forall `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
624
Lemma always_exist `(P : A  uPred M) : (  a, P a)%I  ( a,  P a)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
626
Lemma always_and_sep' P Q : ( (P  Q))%I  ( (P  Q))%I.
627
628
629
Proof.
  intros x n ? [??]; exists (unit x), (unit x); rewrite ra_unit_unit; auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
630
Lemma always_and_sep_l P Q : ( P  Q)%I  ( P  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
631
Proof.
632
  intros x n ? [??]; exists (unit x), x; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
633
634
  by rewrite ra_unit_l, ra_unit_idempotent.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
Lemma always_later P : (  P)%I  (  P)%I.
636
637
638
Proof. done. Qed.

(* Always derived *)
Robbert Krebbers's avatar
Robbert Krebbers committed
639
Lemma always_always P : (  P)%I  ( P)%I.
640
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
641
  apply (anti_symmetric ()); auto using always_elim, always_intro.
642
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
643
644
645
646
647
648
Lemma always_mono P Q : P  Q  ( P)%I  ( Q)%I.
Proof. intros. apply always_intro. by rewrite always_elim. Qed.
Hint Resolve always_mono.
Global Instance always_mono' : Proper (() ==> ()) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.
Lemma always_impl P Q : ( (P  Q))%I  ( P   Q)%I.
649
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
650
651
  apply impl_intro; rewrite <-always_and.
  apply always_mono, impl_elim with P; auto.
Robbert Krebbers's avatar