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

Robbert Krebbers's avatar
Robbert Krebbers committed
177
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  {| uPred_holds n x := a {n} x |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
  intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
Notation "✓" := uPred_valid (at level 1) : 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
Module uPred. Section uPred_logic.
234
Context {M : cmraT}.
235
Implicit Types φ : Prop.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
Implicit Types P Q : uPred M.
237
Implicit Types Ps Qs : list (uPred M).
238
Implicit Types A : Type.
239
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
240
Arguments uPred_holds {_} !_ _ _ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
241

242
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
243
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
244
Global Instance: AntiSymmetric () (@uPred_entails M).
245
Proof. intros P Q HPQ HQP; split; auto. Qed.
246
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Proof.
248
  split; [|by intros [??]; apply (anti_symmetric ())].
249
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
250
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
Global Instance entails_proper :
252
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
253
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
254 255 256
  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
257
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
258

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

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

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

405
Hint Resolve or_elim or_intro_l' or_intro_r'.
Robbert Krebbers's avatar
Robbert Krebbers committed
406 407
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
408

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

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

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

483 484 485 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
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
511 512 513 514 515 516
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.
517
Lemma or_and_l P Q R : (P  Q  R)%I  ((P  Q)  (P  R))%I.
518
Proof.
519
  apply (anti_symmetric ()); first auto.
520
  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
521
Qed.
522 523 524 525 526
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.
527
  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
528 529 530
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.
531 532 533 534 535 536 537 538
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
539 540 541 542 543
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
544 545

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

(* Derived BI Stuff *)