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.

Ralf Jung's avatar
Ralf Jung committed
220
221
222
223
Lemma uPred_lock_conclusion {M} (P Q : uPred M) :
  P  locked Q  P  Q.
Proof. by rewrite -lock. Qed.

224
225
Class TimelessP {M} (P : uPred M) := timelessP :  P  (P   False).
Arguments timelessP {_} _ {_} _ _ _ _.
226
227
Class AlwaysStable {M} (P : uPred M) := always_stable : P   P.
Arguments always_stable {_} _ {_} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
228

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

237
Global Instance: PreOrder (@uPred_entails M).
Robbert Krebbers's avatar
Robbert Krebbers committed
238
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
239
Global Instance: AntiSymm () (@uPred_entails M).
240
Proof. intros P Q HPQ HQP; split; auto. Qed.
241
Lemma equiv_spec P Q : P  Q  P  Q  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
242
Proof.
243
  split; [|by intros [??]; apply (anti_symm ())].
244
  intros HPQ; split; intros x i; apply HPQ.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
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.

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

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


Robbert Krebbers's avatar
Robbert Krebbers committed
558
(* BI connectives *)
559
Lemma sep_mono P P' Q Q' : P  Q  P'  Q'  (P  P')  (Q  Q').
Robbert Krebbers's avatar
Robbert Krebbers committed
560
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
561
  intros HQ HQ' n' x ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
562
    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
564
Global Instance True_sep : LeftId () True%I (@uPred_sep M).
Robbert Krebbers's avatar
Robbert Krebbers committed
565
Proof.
Robbert Krebbers's avatar