upred.v 44.7 KB
Newer Older
1
Require Export algebra.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5
Local Hint Extern 1 (_  _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_  _) => etransitivity; [|eassumption].
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;
8
  uPred_ne x1 x2 n : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
Robbert Krebbers's avatar
Robbert Krebbers committed
9
  uPred_weaken x1 x2 n1 n2 :
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 22 23 24
Section cofe.
  Context {M : cmraT}.
  Instance uPred_equiv : Equiv (uPred M) := λ P Q,  x n,
    {n} x  P n x  Q n x.
  Instance uPred_dist : Dist (uPred M) := λ n P Q,  x n',
    n'  n  {n'} x  P n' x  Q n' x.
  Program Instance uPred_compl : Compl (uPred M) := λ c,
25
    {| uPred_holds n x := c (S n) n x |}.
26 27 28
  Next Obligation. by intros c x y n ??; simpl in *; apply uPred_ne with x. Qed.
  Next Obligation.
    intros c x1 x2 n1 n2 ????; simpl in *.
29
    apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
30 31 32 33 34 35 36 37 38
  Qed.
  Definition uPred_cofe_mixin : CofeMixin (uPred M).
  Proof.
    split.
    * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
      intros HPQ x n ?; apply HPQ with n; auto.
    * intros n; split.
      + by intros P x i.
      + by intros P Q HPQ x i ??; symmetry; apply HPQ.
39
      + by intros P Q Q' HP HQ x i ??; transitivity (Q i x);[apply HP|apply HQ].
40
    * intros n P Q HPQ x i ??; apply HPQ; auto.
41
    * intros c n x i ??; symmetry; apply (chain_cauchy c i (S n)); auto.
42 43 44 45 46
  Qed.
  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
Arguments uPredC : clear implicits.

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
105 106 107 108 109 110 111 112
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 :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
113
       x  x'  n'  n  {n'} x'  P n' x'  Q n' x' |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Next Obligation.
115
  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto.
117
  assert (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
118
  assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  eauto using uPred_weaken, uPred_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Qed.
121
Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
122

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
149 150
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
  {| uPred_holds n x :=  x' n',
Robbert Krebbers's avatar
Robbert Krebbers committed
151
       n'  n  {n'} (x  x')  P n' x'  Q n' (x  x') |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Next Obligation.
153
  intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
154
  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157
  by rewrite (dist_le _ _ _ n2 Hx).
Qed.
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
158 159
  intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
  apply uPred_weaken with (x1  x3) n3;
160
    eauto using cmra_validN_included, cmra_preserving_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162
Qed.

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

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

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

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

219 220
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
221 222
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
223 224
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) :=
  match Ps with [] => True | P :: Ps => P  uPred_big_sep Ps end%I.
225 226
Instance: Params (@uPred_big_sep) 1.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
227

228 229
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
Arguments timelessP {_} _ {_} _ _ _ _.
230 231
Class AlwaysStable {M} (P : uPred M) := always_stable : P   P.
Arguments always_stable {_} _ {_} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
232

Robbert Krebbers's avatar
Robbert Krebbers committed
233 234 235 236
Class AlwaysStableL {M} (Ps : list (uPred M)) :=
  always_stableL : Forall AlwaysStable Ps.
Arguments always_stableL {_} _ {_}.

237
Module uPred. Section uPred_logic.
238
Context {M : cmraT}.
239
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
240
Implicit Types P Q : uPred M.
241
Implicit Types Ps Qs : list (uPred M).
242
Implicit Types A : Type.
243
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
244
Arguments uPred_holds {_} !_ _ _ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
245

246
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
248
Global Instance: AntiSymmetric () (@uPred_entails M).
249
Proof. intros P Q HPQ HQP; split; auto. Qed.
250
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
Proof.
252
  split; [|by intros [??]; apply (anti_symmetric ())].
253
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
Qed.
255
Global Instance entails_proper :
256
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Proof.
258 259 260
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
  * by transitivity P1; [|transitivity Q1].
  * by transitivity P2; [|transitivity Q2].
Robbert Krebbers's avatar
Robbert Krebbers committed
261
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
262

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

(** Introduction and elimination rules *)
347
Lemma const_intro φ P : φ  P   φ.
348
Proof. by intros ???. Qed.
349
Lemma const_elim φ Q R : Q   φ  (φ  Q  R)  Q  R.
350
Proof. intros HQP HQR x n ??; apply HQR; first eapply (HQP _ n); eauto. Qed.
351
Lemma True_intro P : P  True.
352
Proof. by apply const_intro. Qed.
353
Lemma False_elim P : False  P.
354
Proof. by intros x n ?. Qed.
355
Lemma and_elim_l P Q : (P  Q)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
356
Proof. by intros x n ? [??]. Qed.
357
Lemma and_elim_r P Q : (P  Q)  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
Proof. by intros x n ? [??]. Qed.
359
Lemma and_intro P Q R : P  Q  P  R  P  (Q  R).
360
Proof. intros HQ HR x n ??; split; auto. Qed.
361
Lemma or_intro_l P Q : P  (P  Q).
362
Proof. intros x n ??; left; auto. Qed.
363
Lemma or_intro_r P Q : Q  (P  Q).
364
Proof. intros x n ??; right; auto. Qed.
365
Lemma or_elim P Q R : P  R  Q  R  (P  Q)  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
366
Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
367
Lemma impl_intro_r P Q R : (P  Q)  R  P  (Q  R).
Robbert Krebbers's avatar
Robbert Krebbers committed
368
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
369
  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using uPred_weaken.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
Qed.
371
Lemma impl_elim P Q R : P  (Q  R)  P  Q  P  R.
372
Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
373
Lemma forall_intro {A} P (Q : A  uPred M): ( a, P  Q a)  P  ( a, Q a).
374
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
375
Lemma forall_elim {A} {P : A  uPred M} a : ( a, P a)  P a.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
Proof. intros x n ? HP; apply HP. Qed.
377
Lemma exist_intro {A} {P : A  uPred M} a : P a  ( a, P a).
378
Proof. by intros x n ??; exists a. Qed.
379
Lemma exist_elim {A} (P : A  uPred M) Q : ( a, P a  Q)  ( a, P a)  Q.
380
Proof. by intros HPQ x n ? [a ?]; apply HPQ with a. Qed.
381
Lemma eq_refl {A : cofeT} (a : A) P : P  (a  a).
382
Proof. by intros x n ??; simpl. Qed.
Ralf Jung's avatar
Ralf Jung committed
383 384
Lemma eq_rewrite {A : cofeT} a b (Q : A  uPred M) P
  `{HQ:∀ n, Proper (dist n ==> dist n) Q} : P  (a  b)  P  Q a  P  Q b.
385 386 387
Proof.
  intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
388
Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
389
  True  (a  b)  a  b.
390
Proof.
391 392
  intros Hab; apply equiv_dist; intros n; apply Hab with ; last done.
  apply cmra_valid_validN, cmra_empty_valid.
393
Qed.
394
Lemma iff_equiv P Q : True  (P  Q)  P  Q.
395
Proof. by intros HPQ x n ?; split; intros; apply HPQ with x n. Qed.
396 397

(* Derived logical stuff *)
398
Lemma and_elim_l' P Q R : P  R  (P  Q)  R.
399
Proof. by rewrite and_elim_l. Qed.
400
Lemma and_elim_r' P Q R : Q  R  (P  Q)  R.
401
Proof. by rewrite and_elim_r. Qed.
402
Lemma or_intro_l' P Q R : P  Q  P  (Q  R).
403
Proof. intros ->; apply or_intro_l. Qed.
404
Lemma or_intro_r' P Q R : P  R  P  (Q  R).
405
Proof. intros ->; apply or_intro_r. Qed.
406
Lemma exist_intro' {A} P (Q : A  uPred M) a : P  Q a  P  ( a, Q a).
407
Proof. intros ->; apply exist_intro. Qed.
408

409
Hint Resolve or_elim or_intro_l' or_intro_r'.
410 411
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
412

413 414
Lemma impl_intro_l P Q R : (Q  P)  R  P  (Q  R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
415 416 417 418 419 420 421 422
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.
423
Lemma impl_entails P Q : True  (P  Q)  P  Q.
424
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
425
Lemma entails_impl P Q : (P  Q)  True  (P  Q).
426
Proof. auto using impl_intro_l. Qed.
427

428 429
Lemma const_intro_l φ Q R : φ  (■φ  Q)  R  Q  R.
Proof. intros ? <-; auto using const_intro. Qed.
430
Lemma const_intro_r φ Q R : φ  (Q  ■φ)  R  Q  R.
431
Proof. intros ? <-; auto using const_intro. Qed.
432 433 434 435
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
436 437
Lemma const_equiv (φ : Prop) : φ  ( φ : uPred M)%I  True%I.
Proof. intros; apply (anti_symmetric _); auto using const_intro. Qed.
438 439 440
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).
441
Proof.
Ralf Jung's avatar
Ralf Jung committed
442
  apply (eq_rewrite a b (λ b, b  a)%I); auto using eq_refl.
443
  intros n; solve_proper.
444
Qed.
445

446 447
Lemma const_mono φ1 φ2 : (φ1  φ2)   φ1   φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
448
Lemma and_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
449
Proof. auto. Qed.
450
Lemma or_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
451
Proof. auto. Qed.
452
Lemma impl_mono P P' Q Q' : Q  P  P'  Q'  (P  P')  (Q  Q').
453
Proof.
454
  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
455
  apply impl_elim with P; eauto.
456
Qed.
457
Lemma forall_mono {A} (P Q : A  uPred M) :
458
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
459
Proof.
460
  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
461
Qed.
462
Lemma exist_mono {A} (P Q : A  uPred M) :
463
  ( a, P a  Q a)  ( a, P a)  ( a, Q a).
464
Proof. intros HP. apply exist_elim=> a; rewrite (HP a); apply exist_intro. Qed.
465
Global Instance const_mono' : Proper (impl ==> ()) (@uPred_const M).
466
Proof. intros φ1 φ2; apply const_mono. Qed.
467
Global Instance and_mono' : Proper (() ==> () ==> ()) (@uPred_and M).
468
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
469 470 471
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.
472
Global Instance or_mono' : Proper (() ==> () ==> ()) (@uPred_or M).
473
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
474 475 476
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.
477
Global Instance impl_mono' :
478
  Proper (flip () ==> () ==> ()) (@uPred_impl M).
479 480
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
481
  Proper (pointwise_relation _ () ==> ()) (@uPred_forall M A).
482 483
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
484
  Proper (pointwise_relation _ () ==> ()) (@uPred_exist M A).
485
Proof. intros P1 P2; apply exist_mono. Qed.
486

487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514
Global Instance and_idem : Idempotent () (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_idem : Idempotent () (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_comm : Commutative () (@uPred_and M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance True_and : LeftId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_True : RightId () True%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_and : LeftAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_False : RightAbsorb () False%I (@uPred_and M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance True_or : LeftAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_True : RightAbsorb () True%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance False_or : LeftId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance or_False : RightId () False%I (@uPred_or M).
Proof. intros P; apply (anti_symmetric ()); auto. Qed.
Global Instance and_assoc : Associative () (@uPred_and M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Global Instance or_comm : Commutative () (@uPred_or M).
Proof. intros P Q; apply (anti_symmetric ()); auto. Qed.
Global Instance or_assoc : Associative () (@uPred_or M).
Proof. intros P Q R; apply (anti_symmetric ()); auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516 517 518 519 520
Global Instance True_impl : LeftId () True%I (@uPred_impl M).
Proof.
  intros P; apply (anti_symmetric ()).
  * by rewrite -(left_id True%I uPred_and (_  _)%I) impl_elim_r.
  * by apply impl_intro_l; rewrite left_id.
Qed.
521
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
522
Proof.
523
  apply (anti_symmetric ()); first auto.
524
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
525
Qed.
526 527 528 529 530
Lemma or_and_r P Q R : (P  Q  R)%I  ((P  R)  (Q  R))%I.
Proof. by rewrite -!(commutative _ R) or_and_l. Qed.
Lemma and_or_l P Q R : (P  (Q  R))%I  (P  Q  P  R)%I.
Proof.
  apply (anti_symmetric ()); last auto.
531
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
532 533 534
Qed.
Lemma and_or_r P Q R : ((P  Q)  R)%I  (P  R  Q  R)%I.
Proof. by rewrite -!(commutative _ R) and_or_l. Qed.
535 536 537 538 539 540 541 542
Lemma and_exist_l {A} P (Q : A  uPred M) : (P   a, Q a)%I  ( a, P  Q a)%I.
Proof.
  apply (anti_symmetric ()).
  - 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.
Ralf Jung's avatar
Ralf Jung committed
543 544 545 546 547
Lemma and_exist_r {A} P (Q : A  uPred M) : (( a, Q a)  P)%I  ( a, Q a  P)%I.
Proof.
  rewrite -(commutative _ P) and_exist_l.
  apply exist_proper=>a. by rewrite commutative.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
548 549

(* BI connectives *)
550
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
551
Proof.
552
  intros HQ HQ' x n' ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
553
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
Qed.
555
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
556 557
Proof.
  intros P x n Hvalid; split.
558
  * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
559
  * by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
560
Qed. 
561
Global Instance sep_commutative : Commutative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
562 563
Proof.
  by intros P Q x n ?; split;
564
    intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
Robbert Krebbers's avatar
Robbert Krebbers committed
565
Qed.
566
Global Instance sep_associative : Associative () (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
567 568
Proof.
  intros P Q R x n ?; split.
569
  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1  y1), y2; split_ands; auto.
570
    + by rewrite -(associative op) -Hy -Hx.
571 572
    + by exists x1, y1.
  * intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2  x2); split_ands; auto.
573
    + by rewrite (associative op) -Hy -Hx.
574
    + by exists y2, x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
Qed.
576
Lemma wand_intro_r P Q R : (P  Q)  R  P  (Q - R).
Robbert Krebbers's avatar
Robbert Krebbers committed
577
Proof.
578
  intros HPQR x n ?? x' n' ???; apply HPQR; auto.
579
  exists x, x'; split_ands; auto.
580
  eapply uPred_weaken with x n; eauto using cmra_validN_op_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
581
Qed.
582
Lemma wand_elim_l P Q : ((P - Q)  P)  Q.
583
Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
584 585

(* Derived BI Stuff *)
586
Hint Resolve sep_mono.
587
Global Instance sep_mono' : Proper (() ==> () ==> ()) (@uPred_sep M).
588
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
589 590 591
Global Instance sep_flip_mono' :
  Proper (flip () ==> flip () ==> flip ()) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
592
Lemma wand_mono P P' Q Q' : Q  P  P'  Q'  (P - P')  (Q - Q').
593
Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
594
Global Instance wand_mono' : Proper (flip () ==> () ==> ()) (@uPred_wand M).
595
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
596

597
Global Instance sep_True : RightId () True%I (@uPred_sep M).
598
Proof. by intros P; rewrite (commutative _) (left_id _ _). Qed.
599
Lemma sep_elim_l P Q : (P  Q)  P.
600
Proof. by rewrite (True_intro Q) (right_id _ _). Qed.
601
Lemma sep_elim_r P Q : (P  Q)  Q.
602
Proof. by rewrite (commutative ())%I; apply sep_elim_l. Qed.
603
Lemma sep_elim_l' P Q R : P  R  (P  Q)  R.
604
Proof. intros ->; apply sep_elim_l. Qed.
605
Lemma sep_elim_r' P Q R : Q  R  (P  Q)  R.
606 607
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
608
Lemma sep_intro_True_l P Q R : True  P  R  Q  R  (P  Q).
609
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
610
Lemma sep_intro_True_r P Q R : R  P  True  Q  R  (P  Q).
611
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
612 613
Lemma wand_intro_l P Q R : (Q  P)  R  P  (Q - R).
Proof. rewrite (commutative _); apply wand_intro_r. Qed.
614 615 616 617 618 619
Lemma wand_elim_r P Q : (P  (P - Q))  Q.
Proof. rewrite (commutative _ P); apply wand_elim_l. Qed.
Lemma wand_elim_l' P Q R : P  (Q - R)  (P  Q)  R.
Proof. intros ->; apply wand_elim_l. Qed.
Lemma wand_elim_r' P Q