classes.v 13.5 KB
Newer Older
1
From iris.base_logic Require Export base_logic.
2
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
3
4
Import uPred.

5
6
7
8
9
10
11
12
13
14
(* The Or class is useful for efficiency: instead of having two instances
[P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R],
which avoids the need to derive [P] twice. *)
Inductive Or (P1 P2 : Type) :=
  | Or_l : P1  Or P1 P2
  | Or_r : P2  Or P1 P2.
Existing Class Or.
Existing Instance Or_l | 9.
Existing Instance Or_r | 10.

15
16
17
Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
  from_assumption : ?p P  Q.
Arguments from_assumption {_} _ _ _ {_}.
18
(* No need to restrict Hint Mode, we have a default instance that will persistently
19
20
be used in case of evars *)
Hint Mode FromAssumption + + - - : typeclass_instances.
21
22
23
24
25

Class IntoPure {M} (P : uPred M) (φ : Prop) := into_pure : P  ⌜φ⌝.
Arguments into_pure {_} _ _ {_}.
Hint Mode IntoPure + ! - : typeclass_instances.

26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
some shortcoming of unification in Coq's type class search. An example where we
use this workaround is to repair the following instance:

  Global Instance into_exist_and_pure P Q (φ : Prop) :
    IntoPure P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).

Coq is unable to use this instance: [class_apply] -- which is used by type class
search -- fails with the error that it cannot unify [Prop] and [Type]. This is
probably caused because [class_apply] uses an ancient unification algorith. The
[refine] tactic -- which uses a better unification algorithm -- succeeds to
apply the above instance.

Since we do not want to define [Hint Extern] declarations using [refine] for
any instance like [into_exist_and_pure], we factor this out in the class
[IntoPureT]. This way, we only have to declare a [Hint Extern] using [refine]
once, and use [IntoPureT] in any instance like [into_exist_and_pure].

TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
to be finished and merged someday. *)
Class IntoPureT {M} (P : uPred M) (φ : Type) :=
  into_pureT :  ψ : Prop, φ = ψ  IntoPure P ψ.
Lemma into_pureT_hint {M} (P : uPred M) (φ : Prop) : IntoPure P φ  IntoPureT P φ.
Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) =>
  notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.

53
54
55
56
Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝  P.
Arguments from_pure {_} _ _ {_}.
Hint Mode FromPure + ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
59
60
61
62
63
Class FromPureT {M} (P : uPred M) (φ : Type) :=
  from_pureT :  ψ : Prop, φ = ψ  FromPure P ψ.
Lemma from_pureT_hint {M} (P : uPred M) (φ : Prop) : FromPure P φ  FromPureT P φ.
Proof. by exists φ. Qed.
Hint Extern 0 (FromPureT _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.

64
65
66
67
68
Class IntoInternalEq {M} {A : ofeT} (P : uPred M) (x y : A) :=
  into_internal_eq : P  x  y.
Arguments into_internal_eq {_ _} _ _ _ {_}.
Hint Mode IntoInternalEq + - ! - - : typeclass_instances.

69
70
71
72
Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
  into_persistent : ?p P   Q.
Arguments into_persistent {_} _ _ _ {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances.
73

74
75
76
77
78
Class FromAlways {M} (p : bool) (P Q : uPred M) :=
  from_always : (if p then  Q else  Q)  P.
Arguments from_always {_} _ _ _ {_}.
Hint Mode FromAlways + - ! - : typeclass_instances.

79
(* The class [MaybeIntoLaterN] has only two instances:
80

81
82
83
84
- The default instance [MaybeIntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN n P Q → MaybeIntoLaterN n P Q], where [IntoLaterN]
  is identical to [MaybeIntoLaterN], but is supposed to make progress, i.e. it
  should actually strip a later.
85

86
87
88
The point of using the auxilary class [IntoLaterN] is to ensure that the
default instance is not applied deeply inside a term, which may result in too
many definitions being unfolded (see issue #55).
89
90
91
92

For binary connectives we have the following instances:

<<
93
IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
94
------------------------------------------
95
     IntoLaterN n (P /\ Q) (P' /\ Q')
96
97


98
      IntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
99
-------------------------------
100
IntoLaterN n (P /\ Q) (P /\ Q')
101
>>
102
103
104
105
106
107
108
109
110
111

The Boolean [only_head] indicates whether laters should only be stripped in
head position or also below other logical connectives. For [iNext] it should
strip laters below other logical connectives, but this should not happen while
framing, e.g. the following should succeed:

<<
Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Qed.
>>
112
*)
113
Class MaybeIntoLaterN {M} (only_head : bool) (n : nat) (P Q : uPred M) :=
114
  maybe_into_laterN : P  ^n Q.
115
116
Arguments maybe_into_laterN {_} _ _ _ _ {_}.
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
117

118
119
Class IntoLaterN {M} (only_head : bool) (n : nat) (P Q : uPred M) :=
  into_laterN :> MaybeIntoLaterN only_head n P Q.
120
Arguments into_laterN {_} _ _ _ {_}.
121
Hint Mode IntoLaterN + + + ! - : typeclass_instances.
122

123
124
Instance maybe_into_laterN_default {M} only_head n (P : uPred M) :
  MaybeIntoLaterN only_head n P P | 1000.
125
Proof. apply laterN_intro. Qed.
126
127
128
129
130

Class FromLaterN {M} (n : nat) (P Q : uPred M) := from_laterN : ^n Q  P.
Arguments from_laterN {_} _ _ _ {_}.
Hint Mode FromLaterN + - ! - : typeclass_instances.

131
132
133
134
135
136
137
138
139
140
141
142
Class WandWeaken {M} (p : bool) (P Q P' Q' : uPred M) :=
  wand_weaken : (P - Q)  (?p P' - Q').
Hint Mode WandWeaken + + - - - - : typeclass_instances.

Class WandWeaken' {M} (p : bool) (P Q P' Q' : uPred M) :=
  wand_weaken' :> WandWeaken p P Q P' Q'.
Hint Mode WandWeaken' + + - - ! - : typeclass_instances.
Hint Mode WandWeaken' + + - - - ! : typeclass_instances.

Class IntoWand {M} (p : bool) (R P Q : uPred M) := into_wand : R  ?p P - Q.
Arguments into_wand {_} _ _ _ _ {_}.
Hint Mode IntoWand + + ! - - : typeclass_instances.
143

144
145
146
147
148
Class FromAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
  from_and : (if p then Q1  Q2 else Q1  Q2)  P.
Arguments from_and {_} _ _ _ _ {_}.
Hint Mode FromAnd + + ! - - : typeclass_instances.
Hint Mode FromAnd + + - ! ! : typeclass_instances. (* For iCombine *)
149

150
151
152
Lemma mk_from_and_and {M} p (P Q1 Q2 : uPred M) :
  (Q1  Q2  P)  FromAnd p P Q1 Q2.
Proof. rewrite /FromAnd=><-. destruct p; auto using sep_and. Qed.
153
Lemma mk_from_and_persistent {M} (P Q1 Q2 : uPred M) :
154
  Or (Persistent Q1) (Persistent Q2)  (Q1  Q2  P)  FromAnd true P Q1 Q2.
155
156
Proof.
  intros [?|?] ?; rewrite /FromAnd.
157
158
  - by rewrite and_sep_l.
  - by rewrite and_sep_r.
159
Qed.
160
161

Class IntoAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
162
  into_and : P  if p then Q1  Q2 else Q1  Q2.
163
164
Arguments into_and {_} _ _ _ _ {_}.
Hint Mode IntoAnd + + ! - - : typeclass_instances.
165

166
167
Lemma mk_into_and_sep {M} p (P Q1 Q2 : uPred M) :
  (P  Q1  Q2)  IntoAnd p P Q1 Q2.
168
Proof. rewrite /IntoAnd=>->. destruct p; auto using sep_and. Qed.
169

170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
(* There are various versions of [IsOp] with different modes:

- [IsOp a b1 b2]: this one has no mode, it can be used regardless of whether
  any of the arguments is an evar. This class has only one direct instance:
  [IsOp (a ⋅ b) a b].
- [IsOp' a b1 b2]: requires either [a] to start with a constructor, OR [b1] and
  [b2] to start with a constructor. All usual instances should be of this
  class to avoid loops.
- [IsOp'LR a b1 b2]: requires either [a] to start with a constructor. This one
  has just one instance: [IsOp'LR (a ⋅ b) a b] with a very low precendence.
  This is important so that when performing, for example, an [iDestruct] on
  [own γ (q1 + q2)] where [q1] and [q2] are fractions, we actually get
  [own γ q1] and [own γ q2] instead of [own γ ((q1 + q2)/2)] twice.
*)
Class IsOp {A : cmraT} (a b1 b2 : A) := is_op : a  b1  b2.
Arguments is_op {_} _ _ _ {_}.
Hint Mode IsOp + - - - : typeclass_instances.

Instance is_op_op {A : cmraT} (a b : A) : IsOp (a  b) a b | 100.
Proof. by rewrite /IsOp. Qed.

Class IsOp' {A : cmraT} (a b1 b2 : A) := is_op' :> IsOp a b1 b2.
Hint Mode IsOp' + ! - - : typeclass_instances.
Hint Mode IsOp' + - ! ! : typeclass_instances.

Class IsOp'LR {A : cmraT} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
Existing Instance is_op_lr | 0.
Hint Mode IsOp'LR + ! - - : typeclass_instances.
Instance is_op_lr_op {A : cmraT} (a b : A) : IsOp'LR (a  b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
200

201
202
203
204
Class Frame {M} (p : bool) (R P Q : uPred M) := frame : ?p R  Q  P.
Arguments frame {_ _} _ _ _ {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.

205
206
207
208
209
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
Class MaybeFrame {M} (p : bool) (R P Q : uPred M) (progress : bool) :=
  maybe_frame : ?p R  Q  P.
210
Arguments maybe_frame {_} _ _ _ {_}.
211
Hint Mode MaybeFrame + + ! ! - - : typeclass_instances.
212
213

Instance maybe_frame_frame {M} p (R P Q : uPred M) :
214
  Frame p R P Q  MaybeFrame p R P Q true.
215
Proof. done. Qed.
216
217
Instance maybe_frame_default {M} p (R P : uPred M) :
  MaybeFrame p R P P false | 100.
218
Proof. apply sep_elim_r. Qed.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
219

220
221
222
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1  Q2  P.
Arguments from_or {_} _ _ _ {_}.
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
223

224
225
226
Class IntoOr {M} (P Q1 Q2 : uPred M) := into_or : P  Q1  Q2.
Arguments into_or {_} _ _ _ {_}.
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
227

228
Class FromExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
229
  from_exist : ( x, Φ x)  P.
230
231
Arguments from_exist {_ _} _ _ {_}.
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
232

233
Class IntoExist {M A} (P : uPred M) (Φ : A  uPred M) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
234
  into_exist : P   x, Φ x.
235
236
Arguments into_exist {_ _} _ _ {_}.
Hint Mode IntoExist + - ! - : typeclass_instances.
237

238
239
240
241
242
Class IntoForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  into_forall : P   x, Φ x.
Arguments into_forall {_ _} _ _ {_}.
Hint Mode IntoForall + - ! - : typeclass_instances.

243
244
245
246
247
Class FromForall {M A} (P : uPred M) (Φ : A  uPred M) :=
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

248
249
250
Class FromModal {M} (P Q : uPred M) := from_modal : Q  P.
Arguments from_modal {_} _ _ {_}.
Hint Mode FromModal + ! - : typeclass_instances.
251

252
Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
253
  elim_modal : P  (P' - Q')  Q.
254
255
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
256

257
258
259
260
261
262
263
264
265
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
Class AddModal {M} (P P' : uPred M) (Q : uPred M) :=
  add_modal : P  (P' - Q)  Q.
Arguments add_modal {_} _ _ _ {_}.
Hint Mode AddModal + - ! ! : typeclass_instances.

Lemma add_modal_id {M} (P Q : uPred M) : AddModal P P Q.
Proof. by rewrite /AddModal wand_elim_r. Qed.
266

267
268
269
Class IsExcept0 {M} (Q : uPred M) := is_except_0 :  Q  Q.
Arguments is_except_0 {_} _ {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.
270
271
272
273
274
275
276
277
278
279

Class IsCons {A} (l : list A) (x : A) (k : list A) := is_cons : l = x :: k.
Class IsApp {A} (l k1 k2 : list A) := is_app : l = k1 ++ k2.
Global Hint Mode IsCons + ! - - : typeclass_instances.
Global Hint Mode IsApp + ! - - : typeclass_instances.

Instance is_cons_cons {A} (x : A) (l : list A) : IsCons (x :: l) x l.
Proof. done. Qed.
Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.
280
281
282
283
284
285
286
287
288
289
290
291
292
293

(* We make sure that tactics that perform actions on *specific* hypotheses or
parts of the goal look through the [tc_opaque] connective, which is used to make
definitions opaque for type class search. For example, when using `iDestruct`,
an explicit hypothesis is affected, and as such, we should look through opaque
definitions. However, when using `iFrame` or `iNext`, arbitrary hypotheses or
parts of the goal are affected, and as such, type class opacity should be
respected.

This means that there are [tc_opaque] instances for all proofmode type classes
with the exception of:

- [FromAssumption] used by [iAssumption]
- [Frame] used by [iFrame]
294
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
295
- [IntoPersistent] used by [iPersistent]
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
*)
Instance into_pure_tc_opaque {M} (P : uPred M) φ :
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
Instance from_pure_tc_opaque {M} (P : uPred M) φ :
  FromPure P φ  FromPure (tc_opaque P) φ := id.
Instance from_laterN_tc_opaque {M} n (P Q : uPred M) :
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
Instance into_wand_tc_opaque {M} p (R P Q : uPred M) :
  IntoWand p R P Q  IntoWand p (tc_opaque R) P Q := id.
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Instance from_and_tc_opaque {M} p (P Q1 Q2 : uPred M) :
  FromAnd p P Q1 Q2  FromAnd p (tc_opaque P) Q1 Q2 | 102 := id.
Instance into_and_tc_opaque {M} p (P Q1 Q2 : uPred M) :
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Instance from_or_tc_opaque {M} (P Q1 Q2 : uPred M) :
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Instance into_or_tc_opaque {M} (P Q1 Q2 : uPred M) :
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Instance from_exist_tc_opaque {M A} (P : uPred M) (Φ : A  uPred M) :
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Instance into_exist_tc_opaque {M A} (P : uPred M) (Φ : A  uPred M) :
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Instance into_forall_tc_opaque {M A} (P : uPred M) (Φ : A  uPred M) :
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
Instance from_modal_tc_opaque {M} (P Q : uPred M) :
  FromModal P Q  FromModal (tc_opaque P) Q := id.
Instance elim_modal_tc_opaque {M} (P P' Q Q' : uPred M) :
  ElimModal P P' Q Q'  ElimModal (tc_opaque P) P' Q Q' := id.