upred.v 52.1 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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)
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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 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.

113 114 115 116 117 118 119
Instance uPredCF_contractive F :
  rFunctorContractive F  cFunctorContractive (uPredCF F).
Proof.
  intros ? A1 A2 B1 B2 n P Q HPQ.
  apply uPredC_map_ne, rFunctor_contractive=> i ?; split; by apply HPQ.
Qed.

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

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

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

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

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

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

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

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

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

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

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

295 296 297
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

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

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

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

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

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

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

526
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
527 528
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
529

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

545 546
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.