upred.v 45.7 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.
13 14
Global Opaque uPred_holds.
Local Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

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

22 23
Section cofe.
  Context {M : cmraT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  Instance uPred_equiv : Equiv (uPred M) := λ P Q,  n x,
25
    {n} x  P n x  Q n x.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  Instance uPred_dist : Dist (uPred M) := λ n P Q,  n' x,
27 28
    n'  n  {n'} x  P n' x  Q n' x.
  Program Instance uPred_compl : Compl (uPred M) := λ c,
29
    {| uPred_holds n x := c (S n) n x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
31
  Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
    intros c n1 n2 x1 x2 ????; simpl in *.
33
    apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
34 35 36 37
  Qed.
  Definition uPred_cofe_mixin : CofeMixin (uPred M).
  Proof.
    split.
38
    - intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
Robbert Krebbers's avatar
Robbert Krebbers committed
39
      intros HPQ n x ?; apply HPQ with n; auto.
40
    - intros n; split.
41 42
      + by intros P x i.
      + by intros P Q HPQ x i ??; symmetry; apply HPQ.
43
      + by intros P Q Q' HP HQ i x ??; trans (Q i x);[apply HP|apply HQ].
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45
    - intros n P Q HPQ i x ??; apply HPQ; auto.
    - intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
46 47 48 49 50
  Qed.
  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.

51
Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
53 54 55 56
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 :
57
  P1 {n} P2  {n} x  P1 n x  P2 n x.
58
Proof. intros HP ?; apply HP; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Lemma uPred_weaken' {M} (P : uPred M) n1 n2 x1 x2 :
60
  x1  x2  n2  n1  {n2} x2  P n1 x1  P n2 x2.
61
Proof. eauto using uPred_weaken. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62 63

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

(** logical entailement *)
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Definition uPred_entails {M} (P Q : uPred M) :=  n x, {n} x  P n x  Q n x.
98
Hint Extern 0 (uPred_entails _ _) => reflexivity.
99
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
100 101

(** logical connectives *)
102
Program Definition uPred_const {M} (φ : Prop) : uPred M :=
103
  {| uPred_holds n x := φ |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Solve Obligations with done.
105
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Robbert Krebbers's avatar
Robbert Krebbers committed
106

Robbert Krebbers's avatar
Robbert Krebbers committed
107 108 109 110 111 112 113
Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_or {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x := P n x  Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_impl {M} (P Q : uPred M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  {| uPred_holds n x :=  n' x',
Robbert Krebbers's avatar
Robbert Krebbers committed
115
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
117 118
  intros M P Q n1 x1' x1 HPQ Hx1 n2 x2 ????.
  destruct (cmra_included_dist_l n1 x1 x2 x1') as (x2'&?&Hx2); auto.
119
  assert (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
120
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
124

125 126
Program Definition uPred_forall {M A} (Ψ : A  uPred M) : uPred M :=
  {| uPred_holds n x :=  a, Ψ a n x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
128 129
Program Definition uPred_exist {M A} (Ψ : A  uPred M) : uPred M :=
  {| uPred_holds n x :=  a, Ψ a n x |}.
130
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
131

Robbert Krebbers's avatar
Robbert Krebbers committed
132
Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
133
  {| uPred_holds n x := a1 {n} a2 |}.
134
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Robbert Krebbers's avatar
Robbert Krebbers committed
135

Robbert Krebbers's avatar
Robbert Krebbers committed
136
Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
137
  {| uPred_holds n x :=  x1 x2, x {n} x1  x2  P n x1  Q n x2 |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
  by intros M P Q n x y (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) Hxy ??.
143
  assert ( x2', y {n2} x1  x2'  x2  x2') as (x2'&Hy&?).
144
  { destruct Hxy as [z Hy]; exists (x2  z); split; eauto using cmra_included_l.
145
    apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
146
  clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148
  - 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
149 150
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
151
Program Definition uPred_wand {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
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  intros M P Q n1 x1 x2 HPQ Hx n2 x3 ???; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  by rewrite (dist_le _ _ _ _ Hx).
Robbert Krebbers's avatar
Robbert Krebbers committed
158 159
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
  intros M P Q n1 n2 x1 x2 HPQ ??? n3 x3 ???; simpl in *.
  apply uPred_weaken with n3 (x1  x3);
162
    eauto using cmra_validN_included, cmra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
165 166
Program Definition uPred_later {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
Next Obligation. intros M P [|n] ??; eauto using uPred_ne,(dist_le (A:=M)). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  intros M P [|n1] [|n2] x1 x2; eauto using uPred_weaken,cmra_validN_S; try lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
171 172
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
  {| uPred_holds n x := P n (unit x) |}.
173
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
176
    eauto using cmra_unit_preserving, cmra_unit_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178
Qed.

Ralf Jung's avatar
Ralf Jung committed
179
Program Definition uPred_ownM {M : cmraT} (a : M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
  intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??.
184
  exists (a'  x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  {| uPred_holds n x := {n} a |}.
188
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
189

190 191
Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
192 193
Notation "■ φ" := (uPred_const φ%C%type)
  (at level 20, right associativity) : uPred_scope.
Ralf Jung's avatar
Ralf Jung committed
194
Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
195 196 197
Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
198
Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
Infix "∨" := uPred_or : uPred_scope.
200
Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202
Infix "→" := uPred_impl : uPred_scope.
Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
203
Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
204
Notation "P -★ Q" := (uPred_wand P Q)
205
  (at level 199, Q at level 200, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
Notation "∀ x .. y , P" :=
207
  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
Notation "∃ x .. y , P" :=
209
  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
210 211 212 213
Notation "▷ P" := (uPred_later P)
  (at level 20, right associativity) : uPred_scope.
Notation "□ P" := (uPred_always P)
  (at level 20, right associativity) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
Infix "≡" := uPred_eq : uPred_scope.
215
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

217 218 219
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P  Q)  (Q  P))%I.
Infix "↔" := uPred_iff : uPred_scope.

220 221
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
Arguments timelessP {_} _ {_} _ _ _ _.
222 223
Class AlwaysStable {M} (P : uPred M) := always_stable : P   P.
Arguments always_stable {_} _ {_} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
224

Robbert Krebbers's avatar
Robbert Krebbers committed
225
Module uPred. Section uPred_logic.
226
Context {M : cmraT}.
227
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
228
Implicit Types P Q : uPred M.
229
Implicit Types A : Type.
230
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
231
Arguments uPred_holds {_} !_ _ _ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
232

233
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
234
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
235
Global Instance: AntiSymm () (@uPred_entails M).
236
Proof. intros P Q HPQ HQP; split; auto. Qed.
237
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
Proof.
239
  split; [|by intros [??]; apply (anti_symm ())].
240
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
Global Instance entails_proper :
243
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
244
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
246 247
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Robbert Krebbers's avatar
Robbert Krebbers committed
248
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
249

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

(** Introduction and elimination rules *)
335
Lemma const_intro φ P : φ  P   φ.
336
Proof. by intros ???. Qed.
337
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Proof. intros HQP HQR n x ??; apply HQR; first eapply (HQP n); eauto. Qed.
339
Lemma False_elim P : False  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Proof. by intros n x ?. Qed.
341
Lemma and_elim_l P Q : (P  Q)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
Proof. by intros n x ? [??]. Qed.
343
Lemma and_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
Proof. by intros n x ? [??]. Qed.
345
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
346
Proof. intros HQ HR n x ??; split; auto. Qed.
347
Lemma or_intro_l P Q : P  (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
348
Proof. intros n x ??; left; auto. Qed.
349
Lemma or_intro_r P Q : Q  (P  Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
350
Proof. intros n x ??; right; auto. Qed.
351
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
Proof. intros HP HQ n x ? [?|?]. by apply HP. by apply HQ. Qed.
353
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
354
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
355
  intros HQ; repeat intro; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Qed.
357
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
Proof. by intros HP HP' n x ??; apply HP with n x, HP'. Qed.
359
Lemma forall_intro {A} P (Ψ : A  uPred M): ( a, P  Ψ a)  P  ( a, Ψ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
360
Proof. by intros HPΨ n x ?? a; apply HPΨ. Qed.
361
Lemma forall_elim {A} {Ψ : A  uPred M} a : ( a, Ψ a)  Ψ a.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Proof. intros n x ? HP; apply HP. Qed.
363
Lemma exist_intro {A} {Ψ : A  uPred M} a : Ψ a  ( a, Ψ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
364
Proof. by intros n x ??; exists a. Qed.
365
Lemma exist_elim {A} (Φ : A  uPred M) Q : ( a, Φ a  Q)  ( a, Φ a)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
Proof. by intros HΦΨ n x ? [a ?]; apply HΦΨ with a. Qed.
367
Lemma eq_refl {A : cofeT} (a : A) P : P  (a  a).
Robbert Krebbers's avatar
Robbert Krebbers committed
368
Proof. by intros n x ??; simpl. Qed.
369 370
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.
371
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
  intros Hab Ha n x ??; apply HΨ with n a; auto. by symmetry; apply Hab with x.
373
Qed.
374
Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
375
  True  (a  b)  a  b.
376
Proof.
377 378
  intros Hab; apply equiv_dist; intros n; apply Hab with ; last done.
  apply cmra_valid_validN, cmra_empty_valid.
379
Qed.
380
Lemma iff_equiv P Q : True  (P  Q)  P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
381
Proof. by intros HPQ n x ?; split; intros; apply HPQ with n x. Qed.
382 383

(* Derived logical stuff *)
Robbert Krebbers's avatar
Robbert Krebbers committed
384 385
Lemma True_intro P : P  True.
Proof. by apply const_intro. Qed.
386
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
387
Proof. by rewrite and_elim_l. Qed.
388
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
389
Proof. by rewrite and_elim_r. Qed.
390
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
391
Proof. intros ->; apply or_intro_l. Qed.
392
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
393
Proof. intros ->; apply or_intro_r. Qed.
394
Lemma exist_intro' {A} P (Ψ : A  uPred M) a : P  Ψ a  P  ( a, Ψ a).
395
Proof. intros ->; apply exist_intro. Qed.
Ralf Jung's avatar
Ralf Jung committed
396 397
Lemma forall_elim' {A} P (Ψ : A  uPred M) : P  ( a, Ψ a)  ( a, P  Ψ a).
Proof. move=>EQ ?. rewrite EQ. by apply forall_elim. Qed.
398

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

403 404
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
405 406 407 408 409 410 411 412
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.
413
Lemma impl_entails P Q : True  (P  Q)  P  Q.
414
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
415
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
416
Proof. auto using impl_intro_l. Qed.
417

418 419
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
420
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
421
Proof. auto. Qed.
422 423 424 425
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.
426
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
427
Proof. auto. Qed.
428 429 430 431
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.
432
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
433
Proof.
434
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
435
  apply impl_elim with P; eauto.
436
Qed.
437 438
Lemma forall_mono {A} (Φ Ψ : A  uPred M) :
  ( a, Φ a  Ψ a)  ( a, Φ a)  ( a, Ψ a).
439
Proof.
440
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
441
Qed.
442 443 444
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.
445
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
446
Proof. intros φ1 φ2; apply const_mono. Qed.
447
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
Robbert Krebbers's avatar
Robbert Krebbers committed
448
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
449 450 451
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.
452
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
Robbert Krebbers's avatar
Robbert Krebbers committed
453
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
454 455 456
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
Global Instance impl_mono' :
458
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
Robbert Krebbers's avatar
Robbert Krebbers committed
459 460
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
461
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
462 463
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
464
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
Robbert Krebbers's avatar
Robbert Krebbers committed
465
Proof. intros P1 P2; apply exist_mono. Qed.
466

467 468 469 470 471 472
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.
473
Global Instance True_and : LeftId () True%I (@uPred_and M).
474
Proof. intros P; apply (anti_symm ()); auto. Qed.
475
Global Instance and_True : RightId () True%I (@uPred_and M).
476
Proof. intros P; apply (anti_symm ()); auto. Qed.
477
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
478
Proof. intros P; apply (anti_symm ()); auto. Qed.
479
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
480
Proof. intros P; apply (anti_symm ()); auto. Qed.
481
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
482
Proof. intros P; apply (anti_symm ()); auto. Qed.
483
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
484
Proof. intros P; apply (anti_symm ()); auto. Qed.
485
Global Instance False_or : LeftId () False%I (@uPred_or M).
486
Proof. intros P; apply (anti_symm ()); auto. Qed.
487
Global Instance or_False : RightId () False%I (@uPred_or M).
488 489 490 491 492 493 494
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
495 496
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.
497
  intros P; apply (anti_symm ()).
498 499
  - by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
501 502 503
Lemma iff_refl Q P : Q  (P  P).
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.

504
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
505
Proof.
506
  apply (anti_symm ()); first auto.
507
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
508
Qed.
509
Lemma or_and_r P Q R : (P  Q  R)%I  ((P  R)  (Q  R))%I.
510
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
511 512
Lemma and_or_l P Q R : (P  (Q  R))%I  (P  Q  P  R)%I.
Proof.
513
  apply (anti_symm ()); last auto.
514
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
515 516
Qed.
Lemma and_or_r P Q R : ((P  Q)  R)%I  (P  R  Q  R)%I.
517
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
518
Lemma and_exist_l {A} P (Ψ : A  uPred M) : (P   a, Ψ a)%I  ( a, P  Ψ a)%I.
519
Proof.
520
  apply (anti_symm ()).
521 522 523 524 525
  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
    by rewrite -(exist_intro a).
  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
    by rewrite -(exist_intro a) and_elim_r.
Qed.
526
Lemma and_exist_r {A} P (Φ: A  uPred M) : (( a, Φ a)  P)%I  ( a, Φ a  P)%I.
Ralf Jung's avatar
Ralf Jung committed
527
Proof.
528
  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
529
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
530

Ralf Jung's avatar
Ralf Jung committed
531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553
Lemma const_intro_l φ Q R : φ  (■φ  Q)  R  Q  R.
Proof. intros ? <-; auto using const_intro. Qed.
Lemma const_intro_r φ Q R : φ  (Q  ■φ)  R  Q  R.
Proof. intros ? <-; auto using const_intro. Qed.
Lemma const_intro_impl φ Q R : φ  Q  ( φ  R)  Q  R.
Proof.
  intros ? ->; apply (const_intro_l φ); first done. by rewrite impl_elim_r.
Qed.
Lemma const_elim_l φ Q R : (φ  Q  R)  ( φ  Q)  R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_elim_r φ Q R : (φ  Q  R)  (Q   φ)  R.
Proof. intros; apply const_elim with φ; eauto. Qed.
Lemma const_equiv (φ : Prop) : φ  ( φ : uPred M)%I  True%I.
Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
Lemma equiv_eq {A : cofeT} P (a b : A) : a  b  P  (a  b).
Proof. intros ->; apply eq_refl. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : (a  b)  (b  a).
Proof.
  apply (eq_rewrite a b (λ b, b  a)%I); auto using eq_refl.
  intros n; solve_proper.
Qed.


Robbert Krebbers's avatar
Robbert Krebbers committed
554
(* BI connectives *)
555
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
556
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
557
  intros HQ HQ' n' x ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
558
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
560
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
561
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
562
  intros P n x Hvalid; split.
563 564
  - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
  - by intros ?; exists (unit x), x; rewrite cmra_unit_l.