classes.v 28.8 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.bi Require Export bi.
2
From iris.proofmode Require Import base.
3
From iris.proofmode Require Export modalities.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
4
From stdpp Require Import namespaces.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
8
Import bi.

Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
9
  from_assumption : ?p P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
Arguments FromAssumption {_} _ _%I _%I : simpl never.
Arguments from_assumption {_} _ _%I _%I {_}.
12
Hint Mode FromAssumption + + - - : typeclass_instances.
13

14
15
16
17
18
19
20
21
22
23
24
25
Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
  knownl_from_assumption :> FromAssumption p P Q.
Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
Arguments knownl_from_assumption {_} _ _%I _%I {_}.
Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.

Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
  knownr_from_assumption :> FromAssumption p P Q.
Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
Arguments knownr_from_assumption {_} _ _%I _%I {_}.
Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
Class IntoPure {PROP : bi} (P : PROP) (φ : Prop) :=
  into_pure : P  ⌜φ⌝.
Arguments IntoPure {_} _%I _%type_scope : simpl never.
Arguments into_pure {_} _%I _%type_scope {_}.
30
31
Hint Mode IntoPure + ! - : typeclass_instances.

32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
(* [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
52
Class IntoPureT {PROP : bi} (P : PROP) (φ : Type) :=
53
  into_pureT :  ψ : Prop, φ = ψ  IntoPure P ψ.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Lemma into_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ  IntoPureT P φ.
55
56
57
58
Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) =>
  notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
(** [FromPure a P φ] is used when introducing a pure assertion. It is used by
[iPureIntro] and the [[%]] specialization pattern.
61

Robbert Krebbers's avatar
Robbert Krebbers committed
62
63
64
The Boolean [a] specifies whether introduction of [P] needs [emp] in addition
to [φ]. Concretely, for the [iPureIntro] tactic, this means it specifies whether
the spatial context should be empty or not.
65

Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
Note that the Boolean [a] is not needed for the (dual) [IntoPure] class, because
there we can just ask that [P] is [Affine]. *)
68
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
69
  from_pure : <affine>?a ⌜φ⌝  P.
70
71
Arguments FromPure {_} _ _%I _%type_scope : simpl never.
Arguments from_pure {_} _ _%I _%type_scope {_}.
72
Hint Mode FromPure + - ! - : typeclass_instances.
73
74
75
76
77

Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
  from_pureT :  ψ : Prop, φ = ψ  FromPure a P ψ.
Lemma from_pureT_hint {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
  FromPure a P φ  FromPureT a P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Proof. by exists φ. Qed.
79
80
Hint Extern 0 (FromPureT _ _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
81

82
Class IntoInternalEq {PROP : sbi} {A : ofeT} (P : PROP) (x y : A) :=
83
  into_internal_eq : P  x  y.
84
85
Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
86
87
Hint Mode IntoInternalEq + - ! - - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
88
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
89
  into_persistent : <pers>?p P  <pers> Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
92
Hint Mode IntoPersistent + + ! - : typeclass_instances.
93

Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
(** The [FromModal M P Q] class is used by the [iModIntro] tactic to transform
a goal [P] into a modality [M] and proposition [Q].

97
98
99
100
101
102
103
The inputs are [P] and [sel] and the outputs are [M] and [Q].

The input [sel] can be used to specify which modality to introduce in case there
are multiple choices to turn [P] into a modality. For example, given [⎡|==> R⎤],
[sel] can be either [|==> ?e] or [⎡ ?e ⎤], which turn it into an update modality
or embedding, respectively. In case there is no need to specify the modality to
introduce, [sel] should be an evar.
104

Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
107
For modalities [N] that do not need to augment the proof mode environment, one
can define an instance [FromModal modality_id (N P) P]. Defining such an
instance only imposes the proof obligation [P ⊢ N P]. Examples of such
108
modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
109
[bi_absorbingly]. *)
110
111
Class FromModal {PROP1 PROP2 : bi} {A}
    (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
112
  from_modal : M Q  P.
113
114
115
Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
Hint Mode FromModal - + - - - ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
116

117
118
119
120
(** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
proposition [Q].

The input is [Q] and the output is [P]. *)
121
Class FromAffinely {PROP : bi} (P Q : PROP) :=
122
  from_affinely : <affine> Q  P.
123
124
Arguments FromAffinely {_} _%I _%I : simpl never.
Arguments from_affinely {_} _%I _%I {_}.
125
Hint Mode FromAffinely + - ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
126

127
128
129
130
(** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
the proposition [Q].

The input is [Q] and the output is [P]. *)
131
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
132
  into_absorbingly : P  <absorb> Q.
133
134
135
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
136

Robbert Krebbers's avatar
Robbert Krebbers committed
137
138
139
140
141
142
143
144
145
(*
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.
146
*)
147

Robbert Krebbers's avatar
Robbert Krebbers committed
148
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
149
  into_wand : ?p R  ?q P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
154
155
156
157
158
159
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.

160
161
162
163
164
165
166
167
168
169
Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 - Q2)  P.
Arguments FromWand {_} _%I _%I _%I : simpl never.
Arguments from_wand {_} _%I _%I _%I {_}.
Hint Mode FromWand + ! - - : typeclass_instances.

Class FromImpl {PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1  Q2)  P.
Arguments FromImpl {_} _%I _%I _%I : simpl never.
Arguments from_impl {_} _%I _%I _%I {_}.
Hint Mode FromImpl + ! - - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
173
174
175
176
177
178
179
180
181
182
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) :=
183
  into_and : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
186
Hint Mode IntoAnd + + ! - - : typeclass_instances.
187

188
189
190
191
192
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
193

Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
196
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 {_}.
197
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
198

Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
201
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 {_}.
202
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
203

Robbert Krebbers's avatar
Robbert Krebbers committed
204
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
205
  from_exist : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
208
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
209

Robbert Krebbers's avatar
Robbert Krebbers committed
210
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!    
Robbert Krebbers committed
211
  into_exist : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
213
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
214
Hint Mode IntoExist + - ! - : typeclass_instances.
215

Robbert Krebbers's avatar
Robbert Krebbers committed
216
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
217
  into_forall : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
220
221
Hint Mode IntoForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
222
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
223
  from_forall : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
225
Arguments FromForall {_ _} _%I _%I : simpl never.
Arguments from_forall {_ _} _%I _%I {_}.
226
227
Hint Mode FromForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
230
231
232
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
(** The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.

The inputs are [p], [P] and [Q], and the outputs are [φ], [p'], [P'] and [Q'].

The class is used to transform a hypothesis [P] into a hypothesis [P'], given
a goal [Q], which is simultaniously transformed into [Q']. The Booleans [p]
and [p'] indicate whether the original, respectively, updated hypothesis reside
in the persistent context (iff [true]). The proposition [φ] can be used to
express a side-condition that [iMod] will generate (if not [True]).

An example instance is:

  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).

This instance expresses that to eliminate [|={E1,E2}=> P] the goal is
transformed from [|={E1,E3}=> Q] into [|={E2,E3}=> Q], and the resulting
hypothesis is moved into the spatial context (regardless of where it was
originally). A corresponding [ElimModal] instance for the Iris 1/2-style update
modality, would have a side-condition [φ] on the masks. *)
252
253
254
255
256
Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
  elim_modal : φ  ?p P  (?p' P' - Q')  Q.
Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
257

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

266
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
267
Proof. by rewrite /AddModal wand_elim_r. Qed.
268

269
270
271
(** We use the classes [IsCons] and [IsApp] to make sure that instances such as
[frame_big_sepL_cons] and [frame_big_sepL_app] cannot be applied repeatedly
often when having [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
272
273
274
275
276
277
278
279
280
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.
281

282
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Arguments Frame {_} _ _%I _%I _%I.
284
Arguments frame {_} _ _%I _%I _%I {_}.
285
Hint Mode Frame + + ! ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
286

287
288
289
290
(* 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 {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
291
  maybe_frame : ?p R  Q  P.
292
293
Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
294
Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
296

Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
297
  Frame p R P Q  MaybeFrame p R P Q true.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Proof. done. Qed.
299

Robbert Krebbers's avatar
Robbert Krebbers committed
300
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
301
  MaybeFrame true R P P false | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
304
  TCOr (Affine R) (Absorbing P)  MaybeFrame false R P P false | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
306
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
307
308
309
310
311
312
313
314
315
(* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx]
   variant, that only succeeds if the parameter(s) is not an evar. In
   the case the parameter(s) is an evar, then [MakeXxxx] will not
   instantiate it arbitrarily.

   The reason for this is that if given an evar, these typeclasses
   would typically try to instantiate this evar with some arbitrary
   logical constructs such as emp or True. Therefore, we use an Hint
   Mode to disable all the instances that would have this behavior. *)
316
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
317
  make_embed : P  Q.
318
319
320
Arguments MakeEmbed {_ _ _} _%I _%I.
Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
321
  known_make_embed :> MakeEmbed P Q.
322
323
Arguments KnownMakeEmbed {_ _ _} _%I _%I.
Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
324
325
326
327

Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P  Q  PQ .
Arguments MakeSep {_} _%I _%I _%I.
Hint Mode MakeSep + - - - : typeclass_instances.
328
329
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_sep :> MakeSep P Q PQ.
330
331
Arguments KnownLMakeSep {_} _%I _%I _%I.
Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
332
333
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
  knownr_make_sep :> MakeSep P Q PQ.
334
335
336
337
338
339
Arguments KnownRMakeSep {_} _%I _%I _%I.
Hint Mode KnownRMakeSep + - ! - : typeclass_instances.

Class MakeAnd {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P  Q  PQ.
Arguments MakeAnd {_} _%I _%I _%I.
Hint Mode MakeAnd + - - - : typeclass_instances.
340
341
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_and :> MakeAnd P Q PQ.
342
343
Arguments KnownLMakeAnd {_} _%I _%I _%I.
Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
344
345
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
  knownr_make_and :> MakeAnd P Q PQ.
346
347
348
349
350
351
Arguments KnownRMakeAnd {_} _%I _%I _%I.
Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.

Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P  Q  PQ.
Arguments MakeOr {_} _%I _%I _%I.
Hint Mode MakeOr + - - - : typeclass_instances.
352
353
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_or :> MakeOr P Q PQ.
354
355
Arguments KnownLMakeOr {_} _%I _%I _%I.
Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
356
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
357
358
359
360
Arguments KnownRMakeOr {_} _%I _%I _%I.
Hint Mode KnownRMakeOr + - ! - : typeclass_instances.

Class MakeAffinely {PROP : bi} (P Q : PROP) :=
361
  make_affinely : <affine> P  Q.
362
363
364
Arguments MakeAffinely {_} _%I _%I.
Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
365
  known_make_affinely :> MakeAffinely P Q.
366
367
368
Arguments KnownMakeAffinely {_} _%I _%I.
Hint Mode KnownMakeAffinely + ! - : typeclass_instances.

369
370
371
372
373
374
375
376
377
Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
  make_intuitionistically :  P  Q.
Arguments MakeIntuitionistically {_} _%I _%I.
Hint Mode MakeIntuitionistically + - - : typeclass_instances.
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
  known_make_intuitionistically :> MakeIntuitionistically P Q.
Arguments KnownMakeIntuitionistically {_} _%I _%I.
Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.

378
Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
379
  make_absorbingly : <absorb> P  Q.
380
381
382
Arguments MakeAbsorbingly {_} _%I _%I.
Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
383
  known_make_absorbingly :> MakeAbsorbingly P Q.
384
385
386
387
Arguments KnownMakeAbsorbingly {_} _%I _%I.
Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.

Class MakePersistently {PROP : bi} (P Q : PROP) :=
388
  make_persistently : <pers> P  Q.
389
390
391
Arguments MakePersistently {_} _%I _%I.
Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
392
  known_make_persistently :> MakePersistently P Q.
393
394
395
396
397
398
399
400
Arguments KnownMakePersistently {_} _%I _%I.
Hint Mode KnownMakePersistently + ! - : typeclass_instances.

Class MakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
  make_laterN : ^n P  lP.
Arguments MakeLaterN {_} _%nat _%I _%I.
Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
401
  known_make_laterN :> MakeLaterN n P lP.
402
403
404
405
406
407
408
409
Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.

Class MakeExcept0 {PROP : sbi} (P Q : PROP) :=
  make_except_0 : sbi_except_0 P  Q.
Arguments MakeExcept0 {_} _%I _%I.
Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : sbi} (P Q : PROP) :=
410
  known_make_except_0 :> MakeExcept0 P Q.
411
412
413
Arguments KnownMakeExcept0 {_} _%I _%I.
Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.

414
415
416
417
418
419
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.

420
(* The class [MaybeIntoLaterN] has only two instances:
Robbert Krebbers's avatar
Robbert Krebbers committed
421

422
423
424
425
- 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
426

427
428
429
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
430
431
432
433

For binary connectives we have the following instances:

<<
434
IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
435
------------------------------------------
436
     IntoLaterN n (P /\ Q) (P' /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
437
438


439
      IntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
440
-------------------------------
441
IntoLaterN n (P /\ Q) (P /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
442
>>
443
444
445
446
447
448
449
450
451
452

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.
>>
Robbert Krebbers's avatar
Robbert Krebbers committed
453
*)
454
Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
455
  maybe_into_laterN : P  ^n Q.
456
457
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
458
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
459

460
Class IntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
461
  into_laterN :> MaybeIntoLaterN only_head n P Q.
462
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
463
Hint Mode IntoLaterN + + + ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
464

465
Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
466
  MaybeIntoLaterN only_head n P P | 1000.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
Proof. apply laterN_intro. Qed.
468
469
470
(* In the case both parameters are evars and n=0, we have to stop the
   search and unify both evars immediately instead of looping using
   other instances. *)
471
472
Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
473
Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
474

475
476
477
(** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
embeddings using [iModIntro].

478
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
479
480
481
482
483
484
Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
  into_embed : P  Q.
Arguments IntoEmbed {_ _ _} _%I _%I.
Arguments into_embed {_ _ _} _%I _%I {_}.
Hint Mode IntoEmbed + + + ! -  : typeclass_instances.

Ralf Jung's avatar
Ralf Jung committed
485
486
(* We use two type classes for [AsEmpValid], in order to avoid loops in
   typeclass search. Indeed, the [as_emp_valid_embed] instance would try
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
487
   to add an arbitrary number of embeddings. To avoid this, the
Ralf Jung's avatar
Ralf Jung committed
488
489
   [AsEmpValid0] type class cannot handle embeddings, and therefore
   [as_emp_valid_embed] only tries to add one embedding, and we never try
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
490
   to insert nested embeddings. This has the additional advantage of
Ralf Jung's avatar
Ralf Jung committed
491
   always trying [as_emp_valid_embed] as a second option, so that this
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
492
493
494
495
496
   instance is never used when the BI is unknown.

   No Hint Modes are declared here. The appropriate one would be
   [Hint Mode - ! -], but the fact that Coq ignores primitive
   projections for hints modes would make this fail.*)
497
498
Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
  as_emp_valid : φ  bi_emp_valid P.
Ralf Jung's avatar
Ralf Jung committed
499
500
501
502
503
504
Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
  as_emp_valid_here : AsEmpValid φ P.
Arguments AsEmpValid0 {_} _%type _%I.
Existing Instance as_emp_valid_here | 0.

505
506
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
  φ  bi_emp_valid P.
Ralf Jung's avatar
Ralf Jung committed
507
Proof. by apply as_emp_valid. Qed.
508
509
Lemma as_emp_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
  bi_emp_valid P  φ.
Ralf Jung's avatar
Ralf Jung committed
510
Proof. by apply as_emp_valid. Qed.
511

512
513
(* Input: [P]; Outputs: [N],
   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Joseph Tassarotti's avatar
Joseph Tassarotti committed
514
515
516
517
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Arguments IntoInv {_} _%I _.
Hint Mode IntoInv + ! - : typeclass_instances.

518
519
520
(** Accessors.
    This definition only exists for the purpose of the proof mode; a truly
    usable and general form would use telescopes and also allow binders for the
Ralf Jung's avatar
Ralf Jung committed
521
    closing view shift.  [γ] is an [option] to make it easy for ElimAcc
522
    instances to recognize the [emp] case and make it look nicer. *)
523
Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP  PROP)
524
           (α β : X  PROP) (mγ : X  option PROP) : PROP :=
525
  M1 ( x, α x  (β x - M2 (default emp (mγ x))))%I.
526
527

(* Typeclass for assertions around which accessors can be elliminated.
528
   Inputs: [Q], [E1], [E2], [α], [β], [γ]
529
530
531
532
   Outputs: [Q']

   Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
   into [Q'] with a new assumption [α x]. *)
533
Class ElimAcc {PROP : bi} {X : Type} (M1 M2 : PROP  PROP)
534
      (α β : X  PROP) (mγ : X  option PROP)
535
      (Q : PROP) (Q' : X  PROP) :=
536
  elim_acc : (( x, α x - Q' x) - accessor M1 M2 α β mγ - Q).
537
538
539
Arguments ElimAcc {_} {_} _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_acc {_} {_} _%I _%I _%I _%I _%I _%I {_}.
Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
540
541
542
543
544
545
546
547

(* Turn [P] into an accessor.
   Inputs:
   - [Pacc]: the assertion to be turned into an accessor (e.g. an invariant)
   Outputs:
   - [Pin]: additional logic assertion needed for starting the accessor.
   - [φ]: additional Coq assertion needed for starting the accessor.
   - [X] [α], [β], [γ]: the accessor parameters.
548
549
   - [M1], [M2]: the two accessor modalities (they will typically still have
     some evars though, e.g. for the masks)
550
*)
551
Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
552
553
      (M1 M2 : PROP  PROP) (α β : X  PROP) (mγ : X  option PROP) :=
  into_acc : φ  Pacc - Pin - accessor M1 M2 α β mγ.
554
555
556
Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
557
558
559

(* The typeclass used for the [iInv] tactic.
   Input: [Pinv]
560
561
   Arguments:
   - [Pinv] is an invariant assertion
562
563
   - [Pin] is an additional logic assertion needed for opening an invariant
   - [φ] is an additional Coq assertion needed for opening an invariant
564
   - [Pout] is the assertion obtained by opening the invariant
565
566
567
   - [Pclose] is the closing view shift.  It must be (Some _) or None
     when doing typeclass search as instances are allowed to make a
     case distinction on whether the user wants a closing view-shift or not.
568
569
   - [Q] is a goal on which iInv may be invoked
   - [Q'] is the transformed goal that must be proved after opening the invariant.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
570

571
   Most users will never want to instantiate this; there is a general instance
Ralf Jung's avatar
Ralf Jung committed
572
   based on [ElimAcc] and [IntoAcc].  However, logics like Iris 2 that support
573
574
575
576
   invariants but not mask-changing fancy updates can use this class directly to
   still benefit from [iInv].

   TODO: Add support for a binder (like accessors have it).
Joseph Tassarotti's avatar
Joseph Tassarotti committed
577
*)
578
Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
579
      (Pinv Pin : PROP) (Pout : X  PROP) (mPclose : option (X  PROP))
580
      (Q : PROP) (Q' : X  PROP) :=
581
  elim_inv : φ  Pinv  Pin  ( x, Pout x  (default (λ _, emp) mPclose) x - Q' x)  Q.
582
583
584
Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
585

Robbert Krebbers's avatar
Robbert Krebbers committed
586
(** We make sure that tactics that perform actions on *specific* hypotheses or
587
parts of the goal look through the [tc_opaque] connective, which is used to make
Robbert Krebbers's avatar
Robbert Krebbers committed
588
definitions opaque for type class search. For example, when using [iDestruct],
589
an explicit hypothesis is affected, and as such, we should look through opaque
Robbert Krebbers's avatar
Robbert Krebbers committed
590
definitions. However, when using [iFrame] or [iNext], arbitrary hypotheses or
591
592
593
594
595
596
597
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
598
- [Frame] and [MaybeFrame] used by [iFrame]
599
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
600
- [IntoPersistent] used by [iIntuitionistic]
601
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
602
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
603
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
604
605
Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
  FromPure a P φ  FromPure a (tc_opaque P) φ := id.
606
607
Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromWand P Q1 Q2  FromWand (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
608
609
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.
610
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
611
612
613
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) :
614
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
615
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
616
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
617
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
618
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
620
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
622
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
624
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
625
626
627
Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
    M (sel : A) (P : PROP2) (Q : PROP1) :
  FromModal M sel P Q  FromModal M sel (tc_opaque P) Q := id.
628
629
Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
  ElimModal φ p p' P P' Q Q'  ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
630
631
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
  IntoInv P N  IntoInv (tc_opaque P) N := id.
632
633
Instance elim_inv_tc_opaque {PROP : sbi} {X} φ Pinv Pin Pout Pclose Q Q' :
  ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q' 
634
  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.