upred.v 45.8 KB
Newer Older
1
From algebra Require Export cmra.
2 3
Local Hint Extern 1 (_  _) => etrans; [eassumption|].
Local Hint Extern 1 (_  _) => etrans; [|eassumption].
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
Local Hint Extern 10 (_  _) => omega.

Robbert Krebbers's avatar
Robbert Krebbers committed
6
Record uPred (M : cmraT) : Type := IProp {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
  uPred_holds :> nat  M  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9
  uPred_ne n x1 x2 : uPred_holds n x1  x1 {n} x2  uPred_holds n x2;
  uPred_weaken  n1 n2 x1 x2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
10
    uPred_holds n1 x1  x1  x2  n2  n1  {n2} x2  uPred_holds n2 x2
Robbert Krebbers's avatar
Robbert Krebbers committed
11
}.
12
Arguments uPred_holds {_} _ _ _ : simpl never.
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.
242 243 244 245
Lemma equiv_entails P Q : P  Q  P  Q.
Proof. apply equiv_spec. Qed.
Lemma equiv_entails_sym P Q : Q  P  P  Q.
Proof. apply equiv_spec. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246
Global Instance entails_proper :
247
  Proper (() ==> () ==> iff) (() : relation (uPred M)).
Robbert Krebbers's avatar
Robbert Krebbers committed
248
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
250 251
  - by trans P1; [|trans Q1].
  - by trans P2; [|trans Q2].
Robbert Krebbers's avatar
Robbert Krebbers committed
252
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
253

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

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

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

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

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

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

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