classes.v 13.6 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.bi Require Export bi.
2
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
Import bi.

Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
6
  from_assumption : ?p P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
Arguments FromAssumption {_} _ _%I _%I : simpl never.
Arguments from_assumption {_} _ _%I _%I {_}.
(* No need to restrict Hint Mode, we have a default instance that will always
10
11
be used in case of evars *)
Hint Mode FromAssumption + + - - : typeclass_instances.
12

Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
Class IntoPure {PROP : bi} (P : PROP) (φ : Prop) :=
  into_pure : P  ⌜φ⌝.
Arguments IntoPure {_} _%I _%type_scope : simpl never.
Arguments into_pure {_} _%I _%type_scope {_}.
17
18
Hint Mode IntoPure + ! - : typeclass_instances.

19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
(* [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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
39
Class IntoPureT {PROP : bi} (P : PROP) (φ : Type) :=
40
  into_pureT :  ψ : Prop, φ = ψ  IntoPure P ψ.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Lemma into_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ  IntoPureT P φ.
42
43
44
45
Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) =>
  notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
49
Class FromPure {PROP : bi} (P : PROP) (φ : Prop) :=
  from_pure : ⌜φ⌝  P.
Arguments FromPure {_} _%I _%type_scope : simpl never.
Arguments from_pure {_} _%I _%type_scope {_}.
50
51
Hint Mode FromPure + ! - : typeclass_instances.

52
Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
53
  into_internal_eq : P  x  y.
54
55
Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
56
57
Hint Mode IntoInternalEq + - ! - - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
58
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
59
  into_persistent : bi_persistently_if p P  bi_persistently Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
62
Hint Mode IntoPersistent + + ! - : typeclass_instances.
63

64
65
66
67
68
Class FromAlways {PROP : bi} (a pe pl : bool) (P Q : PROP) :=
  from_always : bi_affinely_if a (bi_persistently_if pe (bi_plainly_if pl Q))  P.
Arguments FromAlways {_} _ _ _ _%I _%I : simpl never.
Arguments from_always {_} _ _ _ _%I _%I {_}.
Hint Mode FromAlways + - - - ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
69

70
71
72
73
74
75
Class FromAffinely {PROP : bi} (P Q : PROP) :=
  from_affinely : bi_affinely Q  P.
Arguments FromAffinely {_} _%I _%type_scope : simpl never.
Arguments from_affinely {_} _%I _%type_scope {_}.
Hint Mode FromAffinely + ! - : typeclass_instances.
Hint Mode FromAffinely + - ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
76

77
78
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
  into_absorbingly : P  bi_absorbingly Q.
79
80
81
82
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
83

Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
87
88
89
90
91
92
(*
Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:

- Strip modalities and universal quantifiers of [R] until an arrow or a wand
  has been obtained.
- Balance modalities in the arguments [P] and [Q] to match the goal (which used
  for [iApply]) or the premise (when used with [iSpecialize] and a specific
  hypothesis).
- Instantiate the premise of the wand or implication.
93
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
94
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
95
  into_wand : ?p R  ?q P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
Arguments into_wand {_} _ _ _%I _%I _%I {_}.
Hint Mode IntoWand + + + ! - - : typeclass_instances.

Class IntoWand' {PROP : bi} (p q : bool) (R P Q : PROP) :=
  into_wand' : IntoWand p q R P Q.
Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
Hint Mode IntoWand' + + + ! - ! : typeclass_instances.

Instance into_wand_wand' {PROP : bi} p q (P Q P' Q' : PROP) :
  IntoWand' p q (P - Q) P' Q'  IntoWand p q (P - Q) P' Q' | 100.
Proof. done. Qed.
Instance into_wand_impl' {PROP : bi} p q (P Q P' Q' : PROP) :
  IntoWand' p q (P  Q) P' Q'  IntoWand p q (P  Q) P' Q' | 100.
Proof. done. Qed.
112

Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
115
116
117
118
119
120
121
122
123
124
125
Class FromSep {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1  Q2  P.
Arguments FromSep {_} _%I _%I _%I : simpl never.
Arguments from_sep {_} _%I _%I _%I {_}.
Hint Mode FromSep + ! - - : typeclass_instances.
Hint Mode FromSep + - ! ! : typeclass_instances. (* For iCombine *)

Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1  Q2  P.
Arguments FromAnd {_} _%I _%I _%I : simpl never.
Arguments from_and {_} _%I _%I _%I {_}.
Hint Mode FromAnd + ! - - : typeclass_instances.
Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)

Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
126
  into_and : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
129
Hint Mode IntoAnd + + ! - - : typeclass_instances.
130

131
132
133
134
135
Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
  into_sep : P  Q1  Q2.
Arguments IntoSep {_} _%I _%I _%I : simpl never.
Arguments into_sep {_} _%I _%I _%I {_}.
Hint Mode IntoSep + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
136

Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
139
Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1  Q2  P.
Arguments FromOr {_} _%I _%I _%I : simpl never.
Arguments from_or {_} _%I _%I _%I {_}.
140
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
141

Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
Class IntoOr {PROP : bi} (P Q1 Q2 : PROP) := into_or : P  Q1  Q2.
Arguments IntoOr {_} _%I _%I _%I : simpl never.
Arguments into_or {_} _%I _%I _%I {_}.
145
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
146

Robbert Krebbers's avatar
Robbert Krebbers committed
147
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
148
  from_exist : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
150
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
151
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
152

Robbert Krebbers's avatar
Robbert Krebbers committed
153
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
154
  into_exist : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
157
Hint Mode IntoExist + - ! - : typeclass_instances.
158

Robbert Krebbers's avatar
Robbert Krebbers committed
159
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
160
  into_forall : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
163
164
Hint Mode IntoForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
165
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
166
167
168
169
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
173
174
175
176
177
Class IsExcept0 {PROP : sbi} (Q : PROP) := is_except_0 :  Q  Q.
Arguments IsExcept0 {_} _%I : simpl never.
Arguments is_except_0 {_} _%I {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.

Class FromModal {PROP : bi} (P Q : PROP) := from_modal : Q  P.
Arguments FromModal {_} _%I _%I : simpl never.
Arguments from_modal {_} _%I _%I {_}.
178
Hint Mode FromModal + ! - : typeclass_instances.
179

Robbert Krebbers's avatar
Robbert Krebbers committed
180
Class ElimModal {PROP : bi} (P P' : PROP) (Q Q' : PROP) :=
181
  elim_modal : P  (P' - Q')  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
Arguments ElimModal {_} _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _%I _%I _%I _%I {_}.
184
185
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
186

Robbert Krebbers's avatar
Robbert Krebbers committed
187
Lemma elim_modal_dummy {PROP : bi} (P Q : PROP) : ElimModal P P Q Q.
188
Proof. by rewrite /ElimModal wand_elim_r. Qed.
189

190
191
192
193
194
195
196
197
198
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.
199

200
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
203
204
205
Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.

Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
206
  maybe_frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
209
210
211
212
213
214
215
216
217
218
219
220
Arguments MaybeFrame {_} _ _%I _%I _%I.
Arguments maybe_frame {_} _%I _%I _%I {_}.
Hint Mode MaybeFrame + + ! ! - : typeclass_instances.

Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
  Frame p R P Q  MaybeFrame p R P Q.
Proof. done. Qed.
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
  MaybeFrame true R P P | 100.
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
  TCOr (Affine R) (Absorbing P)  MaybeFrame false R P P | 100.
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.

221
222
223
224
225
226
Class IntoExcept0 {PROP : sbi} (P Q : PROP) := into_except_0 : P   Q.
Arguments IntoExcept0 {_} _%I _%I : simpl never.
Arguments into_except_0 {_} _%I _%I {_}.
Hint Mode IntoExcept0 + ! - : typeclass_instances.
Hint Mode IntoExcept0 + - ! : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
(* The class [IntoLaterN] has only two instances:

- The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN' n P Q → IntoLaterN n P Q], where [IntoLaterN']
  is identical to [IntoLaterN], but computationally is supposed to make
  progress, i.e. its instances should actually strip a later.

The point of using the auxilary class [IntoLaterN'] is to ensure that the
default instance is not applied deeply in the term, which may cause in too many
definitions being unfolded (see issue #55).

For binary connectives we have the following instances:

<<
IntoLaterN' n P P'       IntoLaterN n Q Q'
------------------------------------------
     IntoLaterN' n (P /\ Q) (P' /\ Q')


      IntoLaterN' n Q Q'
-------------------------------
IntoLaterN n (P /\ Q) (P /\ Q')
>>
*)
Class IntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) := into_laterN : P  ^n Q.
Arguments IntoLaterN {_} _%nat_scope _%I _%I.
Arguments into_laterN {_} _%nat_scope _%I _%I {_}.
Hint Mode IntoLaterN + - - - : typeclass_instances.

Class IntoLaterN' {PROP : sbi} (n : nat) (P Q : PROP) :=
  into_laterN' :> IntoLaterN n P Q.
Arguments IntoLaterN' {_} _%nat_scope _%I _%I.
Hint Mode IntoLaterN' + - ! - : typeclass_instances.

Instance into_laterN_default {PROP : sbi} n (P : PROP) : IntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.

Class FromLaterN {PROP : sbi} (n : nat) (P Q : PROP) := from_laterN : ^n Q  P.
Arguments FromLaterN {_} _%nat_scope _%I _%I.
Arguments from_laterN {_} _%nat_scope _%I _%I {_}.
Hint Mode FromLaterN + - ! - : typeclass_instances.

269
270
271
272
273
274
275
276
277
278
279
280
(* 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]
Robbert Krebbers's avatar
Robbert Krebbers committed
281
- [Frame] and [MaybeFrame] used by [iFrame]
282
- [IntoLaterN] and [FromLaterN] used by [iNext]
Robbert Krebbers's avatar
Robbert Krebbers committed
283
- [IntoPersistent] used by [iPersistent]
284
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
285
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
286
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
Instance from_pure_tc_opaque {PROP : bi} (P : PROP) φ :
288
  FromPure P φ  FromPure (tc_opaque P) φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
289
Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
290
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
292
Instance into_wand_tc_opaque {PROP : bi} p q (R P Q : PROP) :
  IntoWand p q R P Q  IntoWand p q (tc_opaque R) P Q := id.
293
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
294
295
296
Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromAnd P Q1 Q2  FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
297
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
299
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
301
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
303
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
305
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
307
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
309
  FromModal P Q  FromModal (tc_opaque P) Q := id.
310
311
(* Higher precedence than [elim_modal_timeless], so that [iAssert] does not
   loop (see test [test_iAssert_modality] in proofmode.v). *)
Robbert Krebbers's avatar
Robbert Krebbers committed
312
Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
313
  ElimModal P P' Q Q'  ElimModal (tc_opaque P) P' Q Q' | 100 := id.