classes.v 28.9 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.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
59
60
(** [FromPure] is used when introducing a pure assertion. It is used
    by iPure, the "[%]" specialization pattern, and the [with "[%]"]
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
61
    pattern when using [iAssert].
62

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
63
64
65
    The [a] Boolean asserts whether we introduce the pure assertion in
    an affine way or in an absorbing way. When [FromPure true P φ] is
    derived, then [FromPure false P φ] can always be derived too. We
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
66
67
    use [true] for specialization patterns and [false] for the
    [iPureIntro] tactic.
68

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
69
70
71
    This Boolean is not needed for [IntoPure], because in the case of
    [IntoPure], we can have the same behavior by asking that [P] be
    [Affine]. *)
72
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
73
  from_pure : <affine>?a ⌜φ⌝  P.
74
75
76
77
78
79
80
81
Arguments FromPure {_} _ _%I _%type_scope : simpl never.
Arguments from_pure {_} _ _%I _%type_scope {_}.
Hint Mode FromPure + + ! - : typeclass_instances.

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
82
Proof. by exists φ. Qed.
83
84
Hint Extern 0 (FromPureT _ _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
85

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

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

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

101
102
103
104
105
106
107
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.
108

Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
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
112
modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
113
[bi_absorbingly]. *)
114
115
Class FromModal {PROP1 PROP2 : bi} {A}
    (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
116
  from_modal : M Q  P.
117
118
119
Arguments FromModal {_ _ _} _ _%I _%I _%I : simpl never.
Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
Hint Mode FromModal - + - - - ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
120

121
122
123
124
(** 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]. *)
125
Class FromAffinely {PROP : bi} (P Q : PROP) :=
126
  from_affinely : <affine> Q  P.
127
128
Arguments FromAffinely {_} _%I _%I : simpl never.
Arguments from_affinely {_} _%I _%I {_}.
129
Hint Mode FromAffinely + - ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
130

131
132
133
134
(** 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]. *)
135
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
136
  into_absorbingly : P  <absorb> Q.
137
138
139
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
140

Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
143
144
145
146
147
148
149
(*
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.
150
*)
151

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

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

192
193
194
195
196
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
197

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

Robbert Krebbers's avatar
Robbert Krebbers committed
203
204
205
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 {_}.
206
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
207

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
234
235
236
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
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
(** 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. *)
256
257
258
259
260
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.
261

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

270
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
271
Proof. by rewrite /AddModal wand_elim_r. Qed.
272

273
274
275
(** 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. *)
276
277
278
279
280
281
282
283
284
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.
285

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

291
292
293
294
(* 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) :=
295
  maybe_frame : ?p R  Q  P.
296
297
Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
298
Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
300

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
311
312
313
314
315
316
317
318
319
(* 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. *)
320
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
321
  make_embed : P  Q.
322
323
324
Arguments MakeEmbed {_ _ _} _%I _%I.
Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
325
  known_make_embed :> MakeEmbed P Q.
326
327
Arguments KnownMakeEmbed {_ _ _} _%I _%I.
Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
328
329
330
331

Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P  Q  PQ .
Arguments MakeSep {_} _%I _%I _%I.
Hint Mode MakeSep + - - - : typeclass_instances.
332
333
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_sep :> MakeSep P Q PQ.
334
335
Arguments KnownLMakeSep {_} _%I _%I _%I.
Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
336
337
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
  knownr_make_sep :> MakeSep P Q PQ.
338
339
340
341
342
343
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.
344
345
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_and :> MakeAnd P Q PQ.
346
347
Arguments KnownLMakeAnd {_} _%I _%I _%I.
Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
348
349
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
  knownr_make_and :> MakeAnd P Q PQ.
350
351
352
353
354
355
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.
356
357
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_or :> MakeOr P Q PQ.
358
359
Arguments KnownLMakeOr {_} _%I _%I _%I.
Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
360
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
361
362
363
364
Arguments KnownRMakeOr {_} _%I _%I _%I.
Hint Mode KnownRMakeOr + - ! - : typeclass_instances.

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

373
374
375
376
377
378
379
380
381
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.

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

Class MakePersistently {PROP : bi} (P Q : PROP) :=
392
  make_persistently : <pers> P  Q.
393
394
395
Arguments MakePersistently {_} _%I _%I.
Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
396
  known_make_persistently :> MakePersistently P Q.
397
398
399
400
401
402
403
404
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) :=
405
  known_make_laterN :> MakeLaterN n P lP.
406
407
408
409
410
411
412
413
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) :=
414
  known_make_except_0 :> MakeExcept0 P Q.
415
416
417
Arguments KnownMakeExcept0 {_} _%I _%I.
Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.

418
419
420
421
422
423
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.

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

426
427
428
429
- 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
430

431
432
433
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
434
435
436
437

For binary connectives we have the following instances:

<<
438
IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
439
------------------------------------------
440
     IntoLaterN n (P /\ Q) (P' /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
441
442


443
      IntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
444
-------------------------------
445
IntoLaterN n (P /\ Q) (P /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
446
>>
447
448
449
450
451
452
453
454
455
456

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
457
*)
458
Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
459
  maybe_into_laterN : P  ^n Q.
460
461
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
462
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
463

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

469
Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
470
  MaybeIntoLaterN only_head n P P | 1000.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
Proof. apply laterN_intro. Qed.
472
473
474
(* 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. *)
475
476
Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
477
Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
478

479
480
481
(** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
embeddings using [iModIntro].

482
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
483
484
485
486
487
488
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
489
490
(* 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
491
   to add an arbitrary number of embeddings. To avoid this, the
Ralf Jung's avatar
Ralf Jung committed
492
493
   [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
494
   to insert nested embeddings. This has the additional advantage of
Ralf Jung's avatar
Ralf Jung committed
495
   always trying [as_emp_valid_embed] as a second option, so that this
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
496
497
498
499
500
   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.*)
501
502
Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
  as_emp_valid : φ  bi_emp_valid P.
Ralf Jung's avatar
Ralf Jung committed
503
504
505
506
507
508
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.

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

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

522
523
524
(** 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
525
    closing view shift.  [γ] is an [option] to make it easy for ElimAcc
526
    instances to recognize the [emp] case and make it look nicer. *)
527
Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP  PROP)
528
           (α β : X  PROP) (mγ : X  option PROP) : PROP :=
529
  M1 ( x, α x  (β x - M2 (default emp (mγ x))))%I.
530
531

(* Typeclass for assertions around which accessors can be elliminated.
532
   Inputs: [Q], [E1], [E2], [α], [β], [γ]
533
534
535
536
   Outputs: [Q']

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

(* 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.
552
553
   - [M1], [M2]: the two accessor modalities (they will typically still have
     some evars though, e.g. for the masks)
554
*)
555
Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
556
557
      (M1 M2 : PROP  PROP) (α β : X  PROP) (mγ : X  option PROP) :=
  into_acc : φ  Pacc - Pin - accessor M1 M2 α β mγ.
558
559
560
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.
561
562
563

(* The typeclass used for the [iInv] tactic.
   Input: [Pinv]
564
565
   Arguments:
   - [Pinv] is an invariant assertion
566
567
   - [Pin] is an additional logic assertion needed for opening an invariant
   - [φ] is an additional Coq assertion needed for opening an invariant
568
   - [Pout] is the assertion obtained by opening the invariant
569
570
571
   - [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.
572
573
   - [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
574

575
   Most users will never want to instantiate this; there is a general instance
Ralf Jung's avatar
Ralf Jung committed
576
   based on [ElimAcc] and [IntoAcc].  However, logics like Iris 2 that support
577
578
579
580
   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
581
*)
582
Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
583
      (Pinv Pin : PROP) (Pout : X  PROP) (mPclose : option (X  PROP))
584
      (Q : PROP) (Q' : X  PROP) :=
585
  elim_inv : φ  Pinv  Pin  ( x, Pout x  (default (λ _, emp) mPclose) x - Q' x)  Q.
586
587
588
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
589

590
591
592
593
594
595
596
597
598
599
600
601
(* 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
602
- [Frame] and [MaybeFrame] used by [iFrame]
603
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
Robbert Krebbers's avatar
Robbert Krebbers committed
604
- [IntoPersistent] used by [iPersistent]
605
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
606
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
607
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
608
609
Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
  FromPure a P φ  FromPure a (tc_opaque P) φ := id.
610
611
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
612
613
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.
614
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
615
616
617
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) :
618
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
620
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
622
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
624
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
626
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
627
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
628
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
629
630
631
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.
632
633
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.
634
635
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
  IntoInv P N  IntoInv (tc_opaque P) N := id.
636
637
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' 
638
  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.