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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
223
Module uPred. Section uPred_logic.
224
Context {M : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Implicit Types P Q : uPred M.
226
Implicit Types Ps Qs : list (uPred M).
227
Implicit Types A : Type.
228
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
Robbert Krebbers's avatar
Robbert Krebbers committed
229

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

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

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

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
537
Global Instance sep_True : RightId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
538
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
539
Lemma sep_elim_l P Q : (P  Q)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
Proof. by rewrite ->(True_intro Q), (right_id _ _). Qed.
541
Lemma sep_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
542
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
543
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
544
Proof. intros ->; apply sep_elim_l. Qed.
545
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
546
547
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
548