upred.v 51.8 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.

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 9
  uPred_ne n x1 x2 : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
  uPred_weaken  n1 n2 x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
32
  Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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)
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 78
  intros x1 x2 Hx; split=> n' y ??.
  split; apply Hx; auto using validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
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)
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 : 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} :
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 : 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 105 106 107 108 109 110 111 112 113 114 115
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.
  intros F A1 A2 B1 B2 n P Q [??]. by apply uPredC_map_ne, rFunctor_ne.
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
116
(** logical entailement *)
117 118
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
  { uPred_in_entails :  n x, {n} x  P n x  Q n x }.
119
Hint Extern 0 (uPred_entails _ _) => reflexivity.
120
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122

(** logical connectives *)
123
Program Definition uPred_const_def {M} (φ : Prop) : uPred M :=
124
  {| uPred_holds n x := φ |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Solve Obligations with done.
126 127 128 129 130
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.

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

133
Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
136 137 138 139 140
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
141 142
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
143 144 145 146 147
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
148
  {| uPred_holds n x :=  n' x',
Robbert Krebbers's avatar
Robbert Krebbers committed
149
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152
  intros M P Q n1 x1' x1 HPQ Hx1 n2 x2 ????.
  destruct (cmra_included_dist_l n1 x1 x2 x1') as (x2'&?&Hx2); auto.
153
  assert (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
154
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed.
158 159 160 161
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
162

163
Program Definition uPred_forall_def {M A} (Ψ : A  uPred M) : uPred M :=
164
  {| uPred_holds n x :=  a, Ψ a n x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
166 167 168 169 170 171
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 :=
172
  {| uPred_holds n x :=  a, Ψ a n x |}.
173
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
174 175 176
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
177

178
Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
179
  {| uPred_holds n x := a1 {n} a2 |}.
180
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
181 182 183
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
184

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

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

221
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
222
  {| uPred_holds n x := P n (unit x) |}.
223
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
  intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
226
    eauto using cmra_unit_preserving, cmra_unit_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
Qed.
228 229 230 231 232 233
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 :=
234 235 236 237 238
  {| 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.
239 240 241 242
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
243

244
Program Definition uPred_ownM_def {M : cmraT} (a : M) : uPred M :=
245
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
  intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??.
249
  exists (a'  x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
250
Qed.
251 252 253 254 255 256
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 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
257
  {| uPred_holds n x := {n} a |}.
258
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
259 260 261 262
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
263

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

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

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

299 300 301 302 303 304 305 306
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.
307
Context {M : cmraT}.
308
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Implicit Types P Q : uPred M.
310
Implicit Types A : Type.
311
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
312
Arguments uPred_holds {_} !_ _ _ /.
313
Hint Immediate uPred_in_entails.
Robbert Krebbers's avatar
Robbert Krebbers committed
314

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

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

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

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

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

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

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

590 591 592 593 594 595
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.
596
Global Instance True_and : LeftId () True%I (@uPred_and M).
597
Proof. intros P; apply (anti_symm ()); auto. Qed.
598
Global Instance and_True : RightId () True%I (@uPred_and M).
599
Proof. intros P; apply (anti_symm ()); auto. Qed.
600
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
601
Proof. intros P; apply (anti_symm ()); auto. Qed.
602
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
603
Proof. intros P; apply (anti_symm ()); auto. Qed.
604
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
605
Proof. intros P; apply (anti_symm ()); auto. Qed.
606
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
607
Proof. intros P; apply (anti_symm ()); auto. Qed.
608
Global Instance False_or : LeftId () False%I (@uPred_or M).
609
Proof. intros P; apply (anti_symm ()); auto. Qed.
610
Global Instance or_False : RightId () False%I (@uPred_or M).
611 612 613 614 615 616 617
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
618 619
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.