upred.v 68.4 KB
Newer Older
1
From iris.algebra Require Export cmra updates.
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 : ucmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
8
  uPred_mono n x1 x2 : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
9
  uPred_closed n1 n2 x : uPred_holds n1 x  n2  n1  {n2} x  uPred_holds n2 x
Robbert Krebbers's avatar
Robbert Krebbers committed
10
}.
11
Arguments uPred_holds {_} _ _ _ : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
14

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

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

  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'.
28
  Program Instance uPred_compl : Compl (uPred M) := λ c,
29
    {| uPred_holds n x := c n n x |}.
30
  Next Obligation. naive_solver eauto using uPred_mono. Qed.
31
  Next Obligation.
32 33
    intros c n1 n2 x ???; simpl in *.
    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
34 35 36 37
  Qed.
  Definition uPred_cofe_mixin : CofeMixin (uPred M).
  Proof.
    split.
38 39 40
    - intros P Q; split.
      + by intros HPQ n; split=> i x ??; apply HPQ.
      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
41
    - intros n; split.
42 43 44 45 46
      + 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.
47
    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
48
  Qed.
49
  Canonical Structure uPredC : cofeT := CofeT (uPred M) uPred_cofe_mixin.
50 51 52
End cofe.
Arguments uPredC : clear implicits.

Ralf Jung's avatar
Ralf Jung committed
53
Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
54 55 56
Proof.
  intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
Qed.
57
Instance uPred_proper {M} (P : uPred M) n : Proper (() ==> iff) (P n).
Ralf Jung's avatar
Ralf Jung committed
58 59 60 61 62 63 64 65
Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.

Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
  P {n2} Q  n2  n1  {n2} x  Q n1 x  P n2 x.
Proof.
  intros [Hne] ???. eapply Hne; try done.
  eapply uPred_closed; eauto using cmra_validN_le.
Qed.
66

Robbert Krebbers's avatar
Robbert Krebbers committed
67
(** functor *)
68
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
69 70
  `{!CMRAMonotone f} (P : uPred M1) :
  uPred M2 := {| uPred_holds n x := P n (f x) |}.
71
Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
72
Next Obligation. naive_solver eauto using uPred_closed, cmra_monotone_validN. Qed.
73

74
Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
77
  intros x1 x2 Hx; split=> n' y ??.
78
  split; apply Hx; auto using cmra_monotone_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80
Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P  P.
81
Proof. by split=> n x ?. Qed.
82
Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (f : M1 -n> M2) (g : M2 -n> M3)
Robbert Krebbers's avatar
Robbert Krebbers committed
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 : ucmraT} (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 : ucmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1  uPredC M2).
92
Lemma uPredC_map_ne {M1 M2 : ucmraT} (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
Program Definition uPredCF (F : urFunctor) : cFunctor := {|
  cFunctor_car A B := uPredC (urFunctor_car F B A);
  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
103
|}.
104 105
Next Obligation.
  intros F A1 A2 B1 B2 n P Q HPQ.
106
  apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
107
Qed.
108 109
Next Obligation.
  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
110
  apply uPred_map_ext=>y. by rewrite urFunctor_id.
111 112 113
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
114
  apply uPred_map_ext=>y; apply urFunctor_compose.
115 116
Qed.

117
Instance uPredCF_contractive F :
118
  urFunctorContractive F  cFunctorContractive (uPredCF F).
119 120
Proof.
  intros ? A1 A2 B1 B2 n P Q HPQ.
121
  apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
122 123
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
124
(** logical entailement *)
125 126
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails :  n x, {n} x  P n x  Q n x }.
127
Hint Extern 0 (uPred_entails _ _) => reflexivity.
128
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
129

130
Hint Resolve uPred_mono uPred_closed : uPred_def.
131

Robbert Krebbers's avatar
Robbert Krebbers committed
132
(** logical connectives *)
133
Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
134
  {| uPred_holds n x := φ |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Solve Obligations with done.
136 137 138 139
Definition uPred_pure_aux : { x | x = @uPred_pure_def }. by eexists. Qed.
Definition uPred_pure {M} := proj1_sig uPred_pure_aux M.
Definition uPred_pure_eq :
  @uPred_pure = @uPred_pure_def := proj2_sig uPred_pure_aux.
140

141
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_pure True).
Robbert Krebbers's avatar
Robbert Krebbers committed
142

143
Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  {| uPred_holds n x := P n x  Q n x |}.
145
Solve Obligations with naive_solver eauto 2 with uPred_def.
146 147 148 149 150
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 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  {| uPred_holds n x := P n x  Q n x |}.
152
Solve Obligations with naive_solver eauto 2 with uPred_def.
153 154 155 156 157
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 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  {| uPred_holds n x :=  n' x',
Robbert Krebbers's avatar
Robbert Krebbers committed
159
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
Next Obligation.
161 162 163
  intros M P Q n1 x1 x1' HPQ [x2 Hx1'] n2 x3 [x4 Hx3] ?; simpl in *.
  rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
  eapply HPQ; auto. exists (x2  x4); by rewrite assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Qed.
165
Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed.
166 167 168 169
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
170

171
Program Definition uPred_forall_def {M A} (Ψ : A  uPred M) : uPred M :=
172
  {| uPred_holds n x :=  a, Ψ a n x |}.
173
Solve Obligations with naive_solver eauto 2 with uPred_def.
174 175 176 177 178 179
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 :=
180
  {| uPred_holds n x :=  a, Ψ a n x |}.
181
Solve Obligations with naive_solver eauto 2 with uPred_def.
182 183 184
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
185

186
Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
187
  {| uPred_holds n x := a1 {n} a2 |}.
188
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
189 190 191
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
192

193
Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
194
  {| uPred_holds n x :=  x1 x2, x {n} x1  x2  P n x1  Q n x2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
Next Obligation.
196
  intros M P Q n x y (x1&x2&Hx&?&?) [z Hy].
197
  exists x1, (x2  z); split_and?; eauto using uPred_mono, cmra_includedN_l.
198 199 200 201 202 203
  by rewrite Hy Hx assoc.
Qed.
Next Obligation.
  intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
  exists x1, x2; cofe_subst; split_and!;
    eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
Qed.
205 206 207
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
208

209
Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
210
  {| uPred_holds n x :=  n' x',
Robbert Krebbers's avatar
Robbert Krebbers committed
211
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
Next Obligation.
213
  intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
214
  apply uPred_mono with (x1  x3);
215
    eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
Qed.
217
Next Obligation. naive_solver. Qed.
218 219 220 221
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
222

223
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
Ralf Jung's avatar
Ralf Jung committed
224
  {| uPred_holds n x := P n (core x) |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Next Obligation.
226
  intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. 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
  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
236 237 238
Next Obligation.
  intros M P [|n] x1 x2; eauto using uPred_mono, cmra_includedN_S.
Qed.
239
Next Obligation.
240
  intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia.
241
Qed.
242 243 244 245
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
246

247
Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
248
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
Next Obligation.
250 251
  intros M a n x1 x [a' Hx1] [x2 ->].
  exists (a'  x2). by rewrite (assoc op) Hx1.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
Qed.
253
Next Obligation. naive_solver eauto using cmra_includedN_le. Qed.
254 255 256 257 258
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.

259
Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
260
  {| uPred_holds n x := {n} a |}.
261
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
262 263 264 265
Definition uPred_cmra_valid_aux : { x | x = @uPred_cmra_valid_def }. by eexists. Qed.
Definition uPred_cmra_valid {M A} := proj1_sig uPred_cmra_valid_aux M A.
Definition uPred_cmra_valid_eq :
  @uPred_cmra_valid = @uPred_cmra_valid_def := proj2_sig uPred_cmra_valid_aux.
Robbert Krebbers's avatar
Robbert Krebbers committed
266

267 268
Program Definition uPred_rvs_def {M} (Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  k yf,
269
      k  n  {k} (x  yf)   x', {k} (x'  yf)  Q k x' |}.
270 271 272 273 274 275 276 277 278 279 280 281
Next Obligation.
  intros M Q n x1 x2 HQ [x3 Hx] k yf Hk.
  rewrite (dist_le _ _ _ _ Hx); last lia. intros Hxy.
  destruct (HQ k (x3  yf)) as (x'&?&?); [auto|by rewrite assoc|].
  exists (x'  x3); split; first by rewrite -assoc.
  apply uPred_mono with x'; eauto using cmra_includedN_l.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_rvs_aux : { x | x = @uPred_rvs_def }. by eexists. Qed.
Definition uPred_rvs {M} := proj1_sig uPred_rvs_aux M.
Definition uPred_rvs_eq : @uPred_rvs = @uPred_rvs_def := proj2_sig uPred_rvs_aux.

282 283
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
  (at level 99, Q at level 200, right associativity) : C_scope.
284
Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
285 286
Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
  (at level 95, no associativity) : C_scope.
287
Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
288
Notation "■ φ" := (uPred_pure φ%C%type)
289
  (at level 20, right associativity) : uPred_scope.
290 291 292 293
Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) : uPred_scope.
Notation "x ⊥ y" := (uPred_pure (x%C%type  y%C%type)) : uPred_scope.
Notation "'False'" := (uPred_pure False) : uPred_scope.
Notation "'True'" := (uPred_pure True) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
Infix "∧" := uPred_and : uPred_scope.
295
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Infix "∨" := uPred_or : uPred_scope.
297
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
298 299
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
300
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
301
Notation "P -★ Q" := (uPred_wand P Q)
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  (at level 99, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Notation "∀ x .. y , P" :=
304
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
Notation "∃ x .. y , P" :=
306
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
307 308
Notation "□ P" := (uPred_always P)
  (at level 20, right associativity) : uPred_scope.
309 310
Notation "▷ P" := (uPred_later P)
  (at level 20, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
Infix "≡" := uPred_eq : uPred_scope.
312
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope.
313 314 315 316 317 318
Notation "|=r=> Q" := (uPred_rvs Q)
  (at level 99, Q at level 200, format "|=r=>  Q") : uPred_scope.
Notation "P =r=> Q" := (P  |=r=> Q)
  (at level 99, Q at level 200, only parsing) : C_scope.
Notation "P =r=★ Q" := (P - |=r=> Q)%I
  (at level 99, Q at level 200, format "P  =r=★  Q") : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
319

320
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
321
Instance: Params (@uPred_iff) 1.
322 323
Infix "↔" := uPred_iff : uPred_scope.

324 325 326 327 328 329 330
Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
  (if p then  P else P)%I.
Instance: Params (@uPred_always_if) 2.
Arguments uPred_always_if _ !_ _/.
Notation "□? p P" := (uPred_always_if p P)
  (at level 20, p at level 0, P at level 20, format "□? p  P").

331 332
Definition uPred_except_last {M} (P : uPred M) : uPred M :=  False  P.
Notation "◇ P" := (uPred_except_last P)
333
  (at level 20, right associativity) : uPred_scope.
334 335
Instance: Params (@uPred_except_last) 1.
Typeclasses Opaque uPred_except_last.
336 337

Class TimelessP {M} (P : uPred M) := timelessP :  P   P.
338
Arguments timelessP {_} _ {_}.
339

340 341
Class PersistentP {M} (P : uPred M) := persistentP : P   P.
Arguments persistentP {_} _ {_}.
Robbert Krebbers's avatar
Robbert Krebbers committed
342

343 344
Module uPred.
Definition unseal :=
345
  (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
346
  uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
347
  uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_rvs_eq).
348
Ltac unseal := rewrite !unseal /=.
349 350

Section uPred_logic.
351
Context {M : ucmraT}.
352
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
Implicit Types P Q : uPred M.
354
Implicit Types A : Type.
355 356
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
357
Arguments uPred_holds {_} !_ _ _ /.
358
Hint Immediate uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
359

360
Global Instance: PreOrder (@uPred_entails M).
361 362
Proof.
  split.
363 364
  - by intros P; split=> x i.
  - by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
365
Qed.
366
Global Instance: AntiSymm () (@uPred_entails M).
367
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
368

369
Lemma equiv_spec P Q : (P  Q)  (P  Q)  (Q  P).
Robbert Krebbers's avatar
Robbert Krebbers committed
370
Proof.
371
  split; [|by intros [??]; apply (anti_symm ())].
372
  intros HPQ; split; split=> x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
Qed.
374
Lemma equiv_entails P Q : (P  Q)  (P  Q).
375
Proof. apply equiv_spec. Qed.
376
Lemma equiv_entails_sym P Q : (Q  P)  (P  Q).
377
Proof. apply equiv_spec. Qed.
378
Global Instance entails_proper :
379
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
380
Proof.
381
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
382 383
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Robbert Krebbers's avatar
Robbert Krebbers committed
384
Qed.
385
Lemma entails_equiv_l (P Q R : uPred M) : (P  Q)  (Q  R)  (P  R).
386
Proof. by intros ->. Qed.
387
Lemma entails_equiv_r (P Q R : uPred M) : (P  Q)  (Q  R)  (P  R).
388
Proof. by intros ? <-. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
389

390
(** Non-expansiveness and setoid morphisms *)
391
Global Instance pure_proper : Proper (iff ==> ()) (@uPred_pure M).
392
Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed.
393
Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
394
Proof.
395
  intros P P' HP Q Q' HQ; unseal; split=> x n' ??.
396
  split; (intros [??]; split; [by apply HP|by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
397
Qed.
398
Global Instance and_proper :
399
  Proper (() ==> () ==> ()) (@uPred_and M) := ne_proper_2 _.
400
Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
401
Proof.
402
  intros P P' HP Q Q' HQ; split=> x n' ??.
403
  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Robbert Krebbers's avatar
Robbert Krebbers committed
404
Qed.
405
Global Instance or_proper :
406
  Proper (() ==> () ==> ()) (@uPred_or M) := ne_proper_2 _.
407
Global Instance impl_ne n :
Robbert Krebbers's avatar
Robbert Krebbers committed
408
  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
409
Proof.
410
  intros P P' HP Q Q' HQ; split=> x n' ??.
411
  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
412
Qed.
413
Global Instance impl_proper :
414
  Proper (() ==> () ==> ()) (@uPred_impl M) := ne_proper_2 _.
415
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
416
Proof.
417
  intros P P' HP Q Q' HQ; split=> n' x ??.
418
  unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
419
    exists x1, x2; split_and!; try (apply HP || apply HQ);
420
    eauto using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
Qed.
422
Global Instance sep_proper :
423
  Proper (() ==> () ==> ()) (@uPred_sep M) := ne_proper_2 _.
424
Global Instance wand_ne n :
Robbert Krebbers's avatar
Robbert Krebbers committed
425
  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Robbert Krebbers's avatar
Robbert Krebbers committed
426
Proof.
427
  intros P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
428
    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
429
Qed.
430
Global Instance wand_proper :
431
  Proper (() ==> () ==> ()) (@uPred_wand M) := ne_proper_2 _.
432
Global Instance eq_ne (A : cofeT) n :
Robbert Krebbers's avatar
Robbert Krebbers committed
433
  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
434
Proof.
435
  intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
436 437
  - 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
438
Qed.
439
Global Instance eq_proper (A : cofeT) :
440
  Proper (() ==> () ==> ()) (@uPred_eq M A) := ne_proper_2 _.
441
Global Instance forall_ne A n :
Robbert Krebbers's avatar
Robbert Krebbers committed
442
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
443 444 445
Proof.
  by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
446
Global Instance forall_proper A :
447
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
448 449 450
Proof.
  by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
451
Global Instance exist_ne A n :
Robbert Krebbers's avatar
Robbert Krebbers committed
452
  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
453
Proof.
454 455
  intros Ψ1 Ψ2 HΨ.
  unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
456
Qed.
457
Global Instance exist_proper A :
458
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
459
Proof.
460 461
  intros Ψ1 Ψ2 HΨ.
  unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
462
Qed.
463
Global Instance later_contractive : Contractive (@uPred_later M).
Robbert Krebbers's avatar
Robbert Krebbers committed
464
Proof.
465
  intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
466
  apply (HPQ n'); eauto using cmra_validN_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
468
Global Instance later_proper' :
469
  Proper (() ==> ()) (@uPred_later M) := ne_proper _.
470 471
Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
Proof.
472
  intros P1 P2 HP.
Robbert Krebbers's avatar
Robbert Krebbers committed
473
  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
474
Qed.
475
Global Instance always_proper :
476
  Proper (() ==> ()) (@uPred_always M) := ne_proper _.
477
Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
478
Proof.
479 480
  intros a b Ha.
  unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
481
Qed.
482
Global Instance ownM_proper: Proper (() ==> ()) (@uPred_ownM M) := ne_proper _.
483 484
Global Instance cmra_valid_ne {A : cmraT} n :
Proper (dist n ==> dist n) (@uPred_cmra_valid M A).
485
Proof.
486 487
  intros a b Ha; unseal; split=> n' x ? /=.
  by rewrite (dist_le _ _ _ _ Ha); last lia.
488
Qed.
489 490
Global Instance cmra_valid_proper {A : cmraT} :
  Proper (() ==> ()) (@uPred_cmra_valid M A) := ne_proper _.
491 492 493 494 495 496 497 498
Global Instance rvs_ne n : Proper (dist n ==> dist n) (@uPred_rvs M).
Proof.
  intros P Q HPQ.
  unseal; split=> n' x; split; intros HP k yf ??;
    destruct (HP k yf) as (x'&?&?); auto;
    exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
Qed.
Global Instance rvs_proper : Proper (() ==> ()) (@uPred_rvs M) := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
499 500

(** Introduction and elimination rules *)
501
Lemma pure_intro φ P : φ  P   φ.
502
Proof. by intros ?; unseal; split. Qed.
503
Lemma pure_elim φ Q R : (Q   φ)  (φ  Q  R)  Q  R.
504 505 506
Proof.
  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
507 508 509
Lemma pure_forall_2 {A} (φ : A  Prop) : ( x : A,  φ x)   ( x : A, φ x).
Proof. by unseal. Qed.

510
Lemma and_elim_l P Q : P  Q  P.
511
Proof. by unseal; split=> n x ? [??]. Qed.
512
Lemma and_elim_r P Q : P  Q  Q.
513
Proof. by unseal; split=> n x ? [??]. Qed.
514
Lemma and_intro P Q R : (P  Q)  (P  R)  P  Q  R.
515
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
516

517
Lemma or_intro_l P Q : P  P  Q.
518
Proof. unseal; split=> n x ??; left; auto. Qed.
519
Lemma or_intro_r P Q : Q  P  Q.
520
Proof. unseal; split=> n x ??; right; auto. Qed.
521
Lemma or_elim P Q R : (P  R)  (Q  R)  P  Q  R.
522
Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
523

524
Lemma impl_intro_r P Q R : (P  Q  R)  P  Q  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
525
Proof.
526 527
  unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
    naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN.
Robbert Krebbers's avatar
Robbert Krebbers committed
528
Qed.
529
Lemma impl_elim P Q R : (P  Q  R)  (P  Q)  P  R.
530
Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
531

532
Lemma forall_intro {A} P (Ψ : A  uPred M): ( a, P  Ψ a)  P   a, Ψ a.
533
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
534
Lemma forall_elim {A} {Ψ : A  uPred M} a : ( a, Ψ a)  Ψ a.
535
Proof. unseal; split=> n x ? HP; apply HP. Qed.
536

537
Lemma exist_intro {A} {Ψ : A  uPred M} a : Ψ a   a, Ψ a.
538
Proof. unseal; split=> n x ??; by exists a. Qed.
539
Lemma exist_elim {A} (Φ : A  uPred M) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
540
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
541

542
Lemma eq_refl {A : cofeT} (a : A) : True  a  a.
543
Proof. unseal; by split=> n x ??; simpl. Qed.
544
Lemma eq_rewrite {A : cofeT} a b (Ψ : A  uPred M) P
545
  {HΨ :  n, Proper (dist n ==> dist n) Ψ} : (P  a  b)  (P  Ψ a)  P  Ψ b.
546
Proof.
547 548 549
  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
  - by symmetry; apply Hab with x.
  - by apply Ha.
550
Qed.
551
Lemma eq_equiv {A : cofeT} (a b : A) : (True  a  b)  a  b.
552
Proof.
553
  unseal=> Hab; apply equiv_dist; intros n; apply Hab with ; last done.
554
  apply cmra_valid_validN, ucmra_unit_valid.
555
Qed.
556
Lemma eq_rewrite_contractive {A : cofeT} a b (Ψ : A  uPred M) P
557
  {HΨ : Contractive Ψ} : (P   (a  b))  (P  Ψ a)  P  Ψ b.
558 559 560 561 562 563
Proof.
  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n)).
  - by apply Ha.
Qed.
564 565

(* Derived logical stuff *)
566
Lemma False_elim P : False  P.
567
Proof. by apply (pure_elim False). Qed.
568
Lemma True_intro P : P  True.
569
Proof. by apply pure_intro. Qed.
570

571
Lemma and_elim_l' P Q R : (P  R)  P  Q  R.
572
Proof. by rewrite and_elim_l. Qed.
573
Lemma and_elim_r' P Q R : (Q  R)  P  Q  R.
574
Proof. by rewrite and_elim_r. Qed.
575
Lemma or_intro_l' P Q R : (P  Q)  P  Q  R.
576
Proof. intros ->; apply or_intro_l. Qed.
577
Lemma or_intro_r' P Q R : (P  R)  P  Q  R.
578
Proof. intros ->; apply or_intro_r. Qed.
579
Lemma exist_intro' {A} P (Ψ : A  uPred M) a : (P  Ψ a)  P   a, Ψ a.
580
Proof. intros ->; apply exist_intro. Qed.
581
Lemma forall_elim' {A} P (Ψ : A  uPred M) : (P   a, Ψ a)   a, P  Ψ a.
582
Proof. move=> HP a. by rewrite HP forall_elim. Qed.
583

584
Hint Resolve pure_intro.
585
Hint Resolve or_elim or_intro_l' or_intro_r'.
586 587
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
588

589
Lemma impl_intro_l P Q R : (Q  P  R)  P  Q  R.
590
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
591
Lemma impl_elim_l P Q : (P  Q)  P  Q.
592
Proof. apply impl_elim with P; auto. Qed.
593
Lemma impl_elim_r P Q : P  (P  Q)  Q.
594
Proof. apply impl_elim with P; auto. Qed.
595
Lemma impl_elim_l' P Q R : (P  Q  R)  P  Q  R.
596
Proof. intros; apply impl_elim with Q; auto. Qed.
597
Lemma impl_elim_r' P Q R : (Q  P  R)  P  Q  R.
598
Proof. intros; apply impl_elim with P; auto. Qed.
599
Lemma impl_entails P Q : (True  P  Q)  P  Q.
600
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
601
Lemma entails_impl P Q : (P  Q)  True  P  Q.
602
Proof. auto using impl_intro_l. Qed.
603

604
Lemma and_mono P P' Q Q' : (P  Q)  (P'  Q')  P  P'  Q  Q'.
605
Proof. auto. Qed.
606
Lemma and_mono_l P P' Q : (P  Q)  P  P'  Q  P'.
607
Proof. by intros; apply and_mono. Qed.
608
Lemma and_mono_r P P' Q' : (P'  Q')  P  P'  P  Q'.
609
Proof. by apply and_mono. Qed.
610