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.