upred.v 51.9 KB
Newer Older
1
From algebra Require Export cmra.
2 3
Local Hint Extern 1 (_  _) => etrans; [eassumption|].
Local Hint Extern 1 (_  _) => etrans; [|eassumption].
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
Local Hint Extern 10 (_  _) => omega.

6
Record uPred (M : cmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
8 9
  uPred_ne n x1 x2 : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
  uPred_weaken  n1 n2 x1 x2 :
10
    uPred_holds n1 x1  x1  x2  n2  n1  {n2} x2  uPred_holds n2 x2
Robbert Krebbers's avatar
Robbert Krebbers committed
11
}.
12
Arguments uPred_holds {_} _ _ _ : simpl never.
13 14
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

16 17 18 19
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _.

20 21
Section cofe.
  Context {M : cmraT}.
22 23 24 25 26 27 28

  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
    { uPred_in_equiv :  n x, {n} x  P n x  Q n x }.
  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
    { uPred_in_dist :  n' x, n'  n  {n'} x  P n' x  Q n' x }.
  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
29
  Program Instance uPred_compl : Compl (uPred M) := λ c,
30
    {| uPred_holds n x := c n n x |}.
31
  Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
32
  Next Obligation.
33
    intros c n1 n2 x1 x2 ????; simpl in *.
34
    apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
35 36 37 38
  Qed.
  Definition uPred_cofe_mixin : CofeMixin (uPred M).
  Proof.
    split.
39 40 41
    - intros P Q; split.
      + by intros HPQ n; split=> i x ??; apply HPQ.
      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
42
    - intros n; split.
43 44 45 46 47
      + by intros P; split=> x i.
      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
      + intros P Q Q' HP HQ; split=> i x ??.
        by trans (Q i x);[apply HP|apply HQ].
    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
48
    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
49 50 51 52 53
  Qed.
  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.

54
Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
55
Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
56 57 58 59
Instance uPred_proper {M} (P : uPred M) n : Proper (() ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.

Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
60
  P1 {n} P2  {n} x  P1 n x  P2 n x.
61
Proof. intros HP ?; apply HP; auto. Qed.
62
Lemma uPred_weaken' {M} (P : uPred M) n1 n2 x1 x2 :
63
  x1  x2  n2  n1  {n2} x2  P n1 x1  P n2 x2.
64
Proof. eauto using uPred_weaken. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65 66

(** functor *)
67 68 69 70
Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
  `{!CMRAMonotone f} (P : uPred M1) :
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Next Obligation.
72
  naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Qed.
74
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
75
  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
76
Proof.
77 78
  intros x1 x2 Hx; split=> n' y ??.
  split; apply Hx; auto using validN_preserving.
79
Qed.
80
Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P  P.
81
Proof. by split=> n x ?. Qed.
82
Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
83
    `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
84
  uPred_map (g  f) P  uPred_map f (uPred_map g P).
85
Proof. by split=> n x Hx. Qed.
86
Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
87
      `{!CMRAMonotone f} `{!CMRAMonotone g}:
88
  ( x, f x  g x)   x, uPred_map f x  uPred_map g x.
89
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
90
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
91
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
92
Lemma uPredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
93
    `{!CMRAMonotone f, !CMRAMonotone g} n :
94
  f {n} g  uPredC_map f {n} uPredC_map g.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Proof.
96
  by intros Hfg P; split=> n' y ??;
97
    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
99

100 101 102 103 104
Program Definition uPredCF (F : rFunctor) : cFunctor := {|
  cFunctor_car A B := uPredC (rFunctor_car F B A);
  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (rFunctor_map F (fg.2, fg.1))
|}.
Next Obligation.
105 106
  intros F A1 A2 B1 B2 n P Q HPQ.
  apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
107 108 109 110 111 112 113 114 115 116
Qed.
Next Obligation.
  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
  apply uPred_map_ext=>y. by rewrite rFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
  apply uPred_map_ext=>y; apply rFunctor_compose.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
117
(** logical entailement *)
118 119
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails :  n x, {n} x  P n x  Q n x }.
120
Hint Extern 0 (uPred_entails _ _) => reflexivity.
121
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
122 123

(** logical connectives *)
124
Program Definition uPred_const_def {M} (φ : Prop) : uPred M :=
125
  {| uPred_holds n x := φ |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Solve Obligations with done.
127 128 129 130 131
Definition uPred_const_aux : { x | x = @uPred_const_def }. by eexists. Qed.
Definition uPred_const {M} := proj1_sig uPred_const_aux M.
Definition uPred_const_eq :
  @uPred_const = @uPred_const_def := proj2_sig uPred_const_aux.

132
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
133

134
Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
135 136
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
137 138 139 140 141
Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed.
Definition uPred_and {M} := proj1_sig uPred_and_aux M.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux.

Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
142 143
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
144 145 146 147 148
Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed.
Definition uPred_or {M} := proj1_sig uPred_or_aux M.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux.

Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
149
  {| uPred_holds n x :=  n' x',
150
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Next Obligation.
152 153
  intros M P Q n1 x1' x1 HPQ Hx1 n2 x2 ????.
  destruct (cmra_included_dist_l n1 x1 x2 x1') as (x2'&?&Hx2); auto.
154
  assert (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
155
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
156
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Qed.
158
Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed.
159 160 161 162
Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
Definition uPred_impl_eq :
  @uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
163

164
Program Definition uPred_forall_def {M A} (Ψ : A  uPred M) : uPred M :=
165
  {| uPred_holds n x :=  a, Ψ a n x |}.
166
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
167 168 169 170 171 172
Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed.
Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A.
Definition uPred_forall_eq :
  @uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux.

Program Definition uPred_exist_def {M A} (Ψ : A  uPred M) : uPred M :=
173
  {| uPred_holds n x :=  a, Ψ a n x |}.
174
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
175 176 177
Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
178

179
Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
180
  {| uPred_holds n x := a1 {n} a2 |}.
181
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
182 183 184
Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed.
Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A.
Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
185

186
Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
187
  {| uPred_holds n x :=  x1 x2, x {n} x1  x2  P n x1  Q n x2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
Next Obligation.
189
  by intros M P Q n x y (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191
Qed.
Next Obligation.
192
  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) Hxy ??.
193
  assert ( x2', y {n2} x1  x2'  x2  x2') as (x2'&Hy&?).
194
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using cmra_included_l.
195
    apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
196
  clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |].
197 198
  - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l.
  - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Qed.
200 201 202
Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
203

204
Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
205
  {| uPred_holds n x :=  n' x',
206
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Next Obligation.
208
  intros M P Q n1 x1 x2 HPQ Hx n2 x3 ???; simpl in *.
209
  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
210
  by rewrite (dist_le _ _ _ _ Hx).
Robbert Krebbers's avatar
Robbert Krebbers committed
211 212
Qed.
Next Obligation.
213 214
  intros M P Q n1 n2 x1 x2 HPQ ??? n3 x3 ???; simpl in *.
  apply uPred_weaken with n3 (x1  x3);
215
    eauto using cmra_validN_included, cmra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
Qed.
217 218 219 220
Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
Definition uPred_wand_eq :
  @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
221

222
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
223
  {| uPred_holds n x := P n (unit x) |}.
224
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Next Obligation.
226
  intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
227
    eauto using cmra_unit_preserving, cmra_unit_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
228
Qed.
229 230 231 232 233 234
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
Definition uPred_always {M} := proj1_sig uPred_always_aux M.
Definition uPred_always_eq :
  @uPred_always = @uPred_always_def := proj2_sig uPred_always_aux.

Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
235 236 237 238 239
  {| 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.
Next Obligation.
  intros M P [|n1] [|n2] x1 x2; eauto using uPred_weaken,cmra_validN_S; try lia.
Qed.
240 241 242 243
Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
Definition uPred_later {M} := proj1_sig uPred_later_aux M.
Definition uPred_later_eq :
  @uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
244

245
Program Definition uPred_ownM_def {M : cmraT} (a : M) : uPred M :=
246
  {| uPred_holds n x := a {n} x |}.
247
Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
248
Next Obligation.
249
  intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??.
250
  exists (a'  x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
251
Qed.
252 253 254 255 256 257
Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
Definition uPred_ownM_eq :
  @uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.

Program Definition uPred_valid_def {M A : cmraT} (a : A) : uPred M :=
258
  {| uPred_holds n x := {n} a |}.
259
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
260 261 262 263
Definition uPred_valid_aux : { x | x = @uPred_valid_def }. by eexists. Qed.
Definition uPred_valid {M A} := proj1_sig uPred_valid_aux M A.
Definition uPred_valid_eq :
  @uPred_valid = @uPred_valid_def := proj2_sig uPred_valid_aux.
264

265 266
Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
267 268
Notation "■ φ" := (uPred_const φ%C%type)
  (at level 20, right associativity) : uPred_scope.
Ralf Jung's avatar
Ralf Jung committed
269
Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
270 271 272
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
273
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
274
Infix "∨" := uPred_or : uPred_scope.
275
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
276 277
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
278
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
279
Notation "P -★ Q" := (uPred_wand P Q)
280
  (at level 199, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
Notation "∀ x .. y , P" :=
282
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Notation "∃ x .. y , P" :=
284
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
285 286
Notation "□ P" := (uPred_always P)
  (at level 20, right associativity) : uPred_scope.
287 288
Notation "▷ P" := (uPred_later P)
  (at level 20, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
Infix "≡" := uPred_eq : uPred_scope.
290
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
291

292 293 294
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

295
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
296
Arguments timelessP {_} _ {_}.
297
Class AlwaysStable {M} (P : uPred M) := always_stable : P   P.
298
Arguments always_stable {_} _ {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
299

300 301 302 303 304 305 306 307
Module uPred.
Definition unseal :=
  (uPred_const_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
  uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
  uPred_later_eq, uPred_ownM_eq, uPred_valid_eq).
Ltac unseal := rewrite !unseal.

Section uPred_logic.
308
Context {M : cmraT}.
309
Implicit Types φ : Prop.
310
Implicit Types P Q : uPred M.
311
Implicit Types A : Type.
312
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
313
Arguments uPred_holds {_} !_ _ _ /.
314
Hint Immediate uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
315

316
Global Instance: PreOrder (@uPred_entails M).
317 318 319 320 321
Proof.
  split.
  * by intros P; split=> x i.
  * by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
Qed.
322
Global Instance: AntiSymm () (@uPred_entails M).
323
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
324
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
325
Proof.
326
  split; [|by intros [??]; apply (anti_symm ())].
327
  intros HPQ; split; split=> x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
Qed.
329 330 331 332
Lemma equiv_entails P Q : P  Q  P  Q.
Proof. apply equiv_spec. Qed.
Lemma equiv_entails_sym P Q : Q  P  P  Q.
Proof. apply equiv_spec. Qed.
333
Global Instance entails_proper :
334
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
335
Proof.
336
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
337 338
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Robbert Krebbers's avatar
Robbert Krebbers committed
339
Qed.
340 341 342 343
Lemma entails_equiv_l (P Q R : uPred M) : P  Q  Q  R  P  R.
Proof. by intros ->. Qed.
Lemma entails_equiv_r (P Q R : uPred M) : P  Q  Q  R  P  R.
Proof. by intros ? <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
344

345
(** Non-expansiveness and setoid morphisms *)
346
Global Instance const_proper : Proper (iff ==> ()) (@uPred_const M).
347
Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed.
348
Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
349
Proof.
350
  intros P P' HP Q Q' HQ; unseal; split=> x n' ??.
351
  split; (intros [??]; split; [by apply HP|by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
352
Qed.
353
Global Instance and_proper :
354
  Proper (() ==> () ==> ()) (@uPred_and M) := ne_proper_2 _.
355
Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Proof.
357
  intros P P' HP Q Q' HQ; split=> x n' ??.
358
  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
359
Qed.
360
Global Instance or_proper :
361
  Proper (() ==> () ==> ()) (@uPred_or M) := ne_proper_2 _.
362
Global Instance impl_ne n :
363
  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Proof.
365
  intros P P' HP Q Q' HQ; split=> x n' ??.
366
  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
367
Qed.
368
Global Instance impl_proper :
369
  Proper (() ==> () ==> ()) (@uPred_impl M) := ne_proper_2 _.
370
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
371
Proof.
372
  intros P P' HP Q Q' HQ; split=> n' x ??.
373
  unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
374
    exists x1, x2; split_and!; try (apply HP || apply HQ);
375
    eauto using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
Qed.
377
Global Instance sep_proper :
378
  Proper (() ==> () ==> ()) (@uPred_sep M) := ne_proper_2 _.
379
Global Instance wand_ne n :
380
  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
381
Proof.
382
  intros P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
383
    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
384
Qed.
385
Global Instance wand_proper :
386
  Proper (() ==> () ==> ()) (@uPred_wand M) := ne_proper_2 _.
387
Global Instance eq_ne (A : cofeT) n :
388
  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
389
Proof.
390
  intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
391 392
  * 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
393
Qed.
394
Global Instance eq_proper (A : cofeT) :
395
  Proper (() ==> () ==> ()) (@uPred_eq M A) := ne_proper_2 _.
396
Global Instance forall_ne A n :
397
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
398 399 400
Proof.
  by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
401
Global Instance forall_proper A :
402
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
403 404 405
Proof.
  by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
406
Global Instance exist_ne A n :
407
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
408
Proof.
409 410
  intros Ψ1 Ψ2 HΨ.
  unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
411
Qed.
412
Global Instance exist_proper A :
413
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
414
Proof.
415 416
  intros Ψ1 Ψ2 HΨ.
  unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
417
Qed.
418
Global Instance later_contractive : Contractive (@uPred_later M).
419
Proof.
420
  intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
421
  apply (HPQ n'); eauto using cmra_validN_S.
422
Qed.
423
Global Instance later_proper :
424
  Proper (() ==> ()) (@uPred_later M) := ne_proper _.
425 426
Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
Proof.
427 428
  intros P1 P2 HP.
  unseal; split=> n' x; split; apply HP; eauto using cmra_unit_validN.
429
Qed.
430
Global Instance always_proper :
431
  Proper (() ==> ()) (@uPred_always M) := ne_proper _.
432
Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
433
Proof.
434 435
  intros a b Ha.
  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
436
Qed.
437 438
Global Instance ownM_proper: Proper (() ==> ()) (@uPred_ownM M) := ne_proper _.
Global Instance valid_ne {A : cmraT} n :
439 440
Proper (dist n ==> dist n) (@uPred_valid M A).
Proof.
441 442
  intros a b Ha; unseal; split=> n' x ? /=.
  by rewrite (dist_le _ _ _ _ Ha); last lia.
443
Qed.
444 445
Global Instance valid_proper {A : cmraT} :
  Proper (() ==> ()) (@uPred_valid M A) := ne_proper _.
446
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
447
Proof. unfold uPred_iff; solve_proper. Qed.
448
Global Instance iff_proper :
449
  Proper (() ==> () ==> ()) (@uPred_iff M) := ne_proper_2 _.
Robbert Krebbers's avatar
Robbert Krebbers committed
450 451

(** Introduction and elimination rules *)
452
Lemma const_intro φ P : φ  P   φ.
453
Proof. by intros ?; unseal; split. Qed.
454
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
455 456 457
Proof.
  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
458
Lemma False_elim P : False  P.
459
Proof. by unseal; split=> n x ?. Qed.
460
Lemma and_elim_l P Q : (P  Q)  P.
461
Proof. by unseal; split=> n x ? [??]. Qed.
462
Lemma and_elim_r P Q : (P  Q)  Q.
463
Proof. by unseal; split=> n x ? [??]. Qed.
464
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
465
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
466
Lemma or_intro_l P Q : P  (P  Q).
467
Proof. unseal; split=> n x ??; left; auto. Qed.
468
Lemma or_intro_r P Q : Q  (P  Q).
469
Proof. unseal; split=> n x ??; right; auto. Qed.
470
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
471
Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
472
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
473
Proof.
474
  unseal; intros HQ; split=> n x ?? n' x' ????.
475
  apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
Qed.
477
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
478
Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
479
Lemma forall_intro {A} P (Ψ : A  uPred M): ( a, P  Ψ a)  P  ( a, Ψ a).
480
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
481
Lemma forall_elim {A} {Ψ : A  uPred M} a : ( a, Ψ a)  Ψ a.
482
Proof. unseal; split=> n x ? HP; apply HP. Qed.
483
Lemma exist_intro {A} {Ψ : A  uPred M} a : Ψ a  ( a, Ψ a).
484
Proof. unseal; split=> n x ??; by exists a. Qed.
485
Lemma exist_elim {A} (Φ : A  uPred M) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
486
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
487
Lemma eq_refl {A : cofeT} (a : A) P : P  (a  a).
488
Proof. unseal; by split=> n x ??; simpl. Qed.
489 490
Lemma eq_rewrite {A : cofeT} a b (Ψ : A  uPred M) P
  `{HΨ :  n, Proper (dist n ==> dist n) Ψ} : P  (a  b)  P  Ψ a  P  Ψ b.
491
Proof.
492
  unseal; intros Hab Ha; split=> n x ??.
493
  apply HΨ with n a; auto. by symmetry; apply Hab with x. by apply Ha.
494
Qed.
495
Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
496
  True  (a  b)  a  b.
497
Proof.
498
  unseal=> Hab; apply equiv_dist; intros n; apply Hab with ; last done.
499
  apply cmra_valid_validN, cmra_empty_valid.
500
Qed.
501
Lemma iff_equiv P Q : True  (P  Q)  P  Q.
502 503 504 505
Proof.
  rewrite /uPred_iff; unseal=> HPQ.
  split=> n x ?; split; intros; by apply HPQ with n x.
Qed.
506 507

(* Derived logical stuff *)
508 509
Lemma True_intro P : P  True.
Proof. by apply const_intro. Qed.
510
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
511
Proof. by rewrite and_elim_l. Qed.
512
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
513
Proof. by rewrite and_elim_r. Qed.
514
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
515
Proof. intros ->; apply or_intro_l. Qed.
516
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
517
Proof. intros ->; apply or_intro_r. Qed.
518
Lemma exist_intro' {A} P (Ψ : A  uPred M) a : P  Ψ a  P  ( a, Ψ a).
519
Proof. intros ->; apply exist_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
520
Lemma forall_elim' {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)  ( a, P  Ψ a).
521
Proof. move=> HP a. by rewrite HP forall_elim. Qed.
522

523
Hint Resolve or_elim or_intro_l' or_intro_r'.
524 525
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
526

527 528
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
529 530 531 532 533 534 535 536
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.
537
Lemma impl_entails P Q : True  (P  Q)  P  Q.
538
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
539
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
540
Proof. auto using impl_intro_l. Qed.
541

542 543
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
544
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
545
Proof. auto. Qed.
546 547 548 549
Lemma and_mono_l P P' Q : P  Q  (P  P')  (Q  P').
Proof. by intros; apply and_mono. Qed.
Lemma and_mono_r P P' Q' : P'  Q'  (P  P')  (P  Q').
Proof. by apply and_mono. Qed.
550
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
551
Proof. auto. Qed.
552 553 554 555
Lemma or_mono_l P P' Q : P  Q  (P  P')  (Q  P').
Proof. by intros; apply or_mono. Qed.
Lemma or_mono_r P P' Q' : P'  Q'  (P  P')  (P  Q').
Proof. by apply or_mono. Qed.
556
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
557
Proof.
558
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
559
  apply impl_elim with P; eauto.
560
Qed.
561 562
Lemma forall_mono {A} (Φ Ψ : A  uPred M) :
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
563
Proof.
564
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
565
Qed.
566 567 568
Lemma exist_mono {A} (Φ Ψ : A  uPred M) :
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.
569
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
570
Proof. intros φ1 φ2; apply const_mono. Qed.
571
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
572
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
573 574 575
Global Instance and_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
576
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
577
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
578 579 580
Global Instance or_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
581
Global Instance impl_mono' :
582
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
583 584
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
585
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
586 587
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
588
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
589
Proof. intros P1 P2; apply exist_mono. Qed.
590

591 592 593 594 595 596
Global Instance and_idem : IdemP () (@uPred_and M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance or_idem : IdemP () (@uPred_or M).
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_comm : Comm () (@uPred_and M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
597
Global Instance True_and : LeftId () True%I (@uPred_and M).
598
Proof. intros P; apply (anti_symm ()); auto. Qed.
599
Global Instance and_True : RightId () True%I (@uPred_and M).
600
Proof. intros P; apply (anti_symm ()); auto. Qed.
601
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
602
Proof. intros P; apply (anti_symm ()); auto. Qed.
603
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
604
Proof. intros P; apply (anti_symm ()); auto. Qed.
605
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
606
Proof. intros P; apply (anti_symm ()); auto. Qed.
607
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
608
Proof. intros P; apply (anti_symm ()); auto. Qed.
609
Global Instance False_or : LeftId () False%I (@uPred_or M).
610
Proof. intros P; apply (anti_symm ()); auto. Qed.
611
Global Instance or_False : RightId () False%I (@uPred_or M).
612 613 614 615 616 617 618
Proof. intros P; apply (anti_symm ()); auto. Qed.
Global Instance and_assoc : Assoc () (@uPred_and M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
Global Instance or_comm : Comm () (@uPred_or M).
Proof. intros P Q; apply (anti_symm ()); auto. Qed.
Global Instance or_assoc : Assoc () (@uPred_or M).
Proof. intros P Q R; apply (anti_symm ()); auto. Qed.
619 620
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.
621
  intros P; apply (anti_symm ()).
622 623
  - by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
624
Qed.
625 626 627
Lemma iff_refl Q P : Q  (P  P).
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.

628
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
629
Proof.
630
  apply (anti_symm ()); first auto.
631
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
632
Qed.
633
Lemma or_and_r P Q R : (P  Q  R)%I  ((P  R)  (Q  R))%I.
634
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
635 636
Lemma and_or_l P Q R : (P  (Q  R))%I  (P  Q  P  R)%I.
Proof.
637
  apply (anti_symm ()); last auto.
638
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
639 640
Qed.
Lemma and_or_r P Q R : ((P  Q)  R)%I  (P  R  Q  R)%I.
641
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
642
Lemma and_exist_l {A} P (Ψ : A  uPred M) : (P   a, Ψ a)%I  ( a, P  Ψ a)%I.
643
Proof.
644
  apply (anti_symm ()).
645 646 647 648 649
  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
    by rewrite -(exist_intro a) and_elim_r.
Qed.
650
Lemma and_exist_r {A} P (Φ: A  uPred M) : (( a, Φ a)  P)%I  ( a, Φ a  P)%I.
Ralf Jung's avatar
Ralf Jung committed
651
Proof.
652
  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
653
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
654

655
Lemma const_intro_l φ Q R : φ  ( φ  Q)  R  Q  R.
Ralf Jung's avatar
Ralf Jung committed
656
Proof. intros ? <-; auto using const_intro. Qed.
657
Lemma const_intro_r φ Q R : φ  (Q   φ)  R  Q  R.
Ralf Jung's avatar
Ralf Jung committed
658 659
Proof. intros ? <-; auto using const_intro. Qed.
Lemma const_intro_impl φ Q R : φ  Q  ( φ  R)  Q  R.
660
Proof. intros ? ->. eauto using const_intro_l, impl_elim_r. Qed.
Ralf Jung's avatar
Ralf Jung committed
661 662 663 664 665 666 667 668 669
Lemma const_elim_l φ Q R : (φ  Q  R)  ( φ  Q)  R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_elim_r φ Q R : (φ  Q  R)  (Q   φ)  R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_equiv (φ : Prop) : φ  ( φ : uPred M)%I  True%I.
Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
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).
670
Proof. apply (eq_rewrite a b (λ b, b  a)%I); auto using eq_refl. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
671

Robbert Krebbers's avatar
Robbert Krebbers committed
672
(* BI connectives *)
673
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
674
Proof.
675 676
  intros HQ HQ'; unseal.
  split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
677
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
678
Qed.
679
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
680
Proof.
681
  intros P; unseal; split=> n x Hvalid; split.
682 683
  - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
  - by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
684
Qed. 
685
Global Instance sep_comm : Comm () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
686
Proof.
687
  by intros P Q; unseal; split=> n x ?; split;
688
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
Robbert Krebbers's avatar
Robbert Krebbers committed
689
Qed.