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

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

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
47 48
(** [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
49
    pattern when using [iAssert].
50

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
51 52 53
    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
54 55
    use [true] for specialization patterns and [false] for the
    [iPureIntro] tactic.
56

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
57 58 59
    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]. *)
60 61 62 63 64 65 66 67 68 69
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
  from_pure : bi_affinely_if a ⌜φ⌝  P.
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
70
Proof. by exists φ. Qed.
71 72
Hint Extern 0 (FromPureT _ _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
73

74
Class IntoInternalEq {PROP : sbi} {A : ofeT} (P : PROP) (x y : A) :=
75
  into_internal_eq : P  x  y.
76 77
Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
78 79
Hint Mode IntoInternalEq + - ! - - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
80
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
81
  into_persistent : bi_persistently_if p P  bi_persistently Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83
Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
84
Hint Mode IntoPersistent + + ! - : typeclass_instances.
85

86 87
(* The `iModIntro` tactic is not tied the Iris modalities, but can be
instantiated with a variety of modalities.
88

89 90
In order to plug in a modality, one has to decide for both the persistent and
spatial what action should be performed upon introducing the modality:
91 92 93 94

- Introduction is only allowed when the context is empty.
- Introduction is only allowed when all hypotheses satisfy some predicate
  `C : PROP → Prop` (where `C` should be a type class).
95 96 97 98
- Introduction will transform each hypotheses using a type class
  `C : PROP → PROP → Prop`, where the first parameter is the input and the
  second parameter is the output. Hypotheses that cannot be transformed (i.e.
  for which no instance of `C` can be found) will be cleared.
99 100 101 102
- Introduction will clear the context.
- Introduction will keep the context as-if.

Formally, these actions correspond to the following inductive type: *)
103

104 105 106 107 108 109 110
Inductive modality_intro_spec (PROP1 : bi) : bi  Type :=
  | MIEnvIsEmpty {PROP2 : bi} : modality_intro_spec PROP1 PROP2
  | MIEnvForall (C : PROP1  Prop) : modality_intro_spec PROP1 PROP1
  | MIEnvTransform {PROP2 : bi} (C : PROP2  PROP1  Prop) : modality_intro_spec PROP1 PROP2
  | MIEnvClear {PROP2} : modality_intro_spec PROP1 PROP2
  | MIEnvId : modality_intro_spec PROP1 PROP1.
Arguments MIEnvIsEmpty {_ _}.
111
Arguments MIEnvForall {_} _.
112 113
Arguments MIEnvTransform {_ _} _.
Arguments MIEnvClear {_ _}.
114 115 116 117
Arguments MIEnvId {_}.

Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).

118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141
Definition modality_intro_spec_persistent {PROP1 PROP2}
    (s : modality_intro_spec PROP1 PROP2) : (PROP1  PROP2)  Prop :=
  match s with
  | MIEnvIsEmpty => λ M, True
  | MIEnvForall C => λ M,
     ( P, C P   P  M ( P)) 
     ( P Q, M P  M Q  M (P  Q))
  | MIEnvTransform C => λ M,
     ( P Q, C P Q   P  M ( Q)) 
     ( P Q, M P  M Q  M (P  Q))
  | MIEnvClear => λ M, True
  | MIEnvId => λ M,  P,  P  M ( P)
  end.

Definition modality_intro_spec_spatial {PROP1 PROP2}
    (s : modality_intro_spec PROP1 PROP2) : (PROP1  PROP2)  Prop :=
  match s with
  | MIEnvIsEmpty => λ M, True
  | MIEnvForall C => λ M,  P, C P  P  M P
  | MIEnvTransform C => λ M,  P Q, C P Q  P  M Q
  | MIEnvClear => λ M,  P, Absorbing (M P)
  | MIEnvId => λ M,  P, P  M P
  end.

142 143
(* A modality is then a record packing together the modality with the laws it
should satisfy to justify the given actions for both contexts: *)
144 145 146 147
Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1  PROP2)
    (pspec sspec : modality_intro_spec PROP1 PROP2) := {
  modality_mixin_persistent : modality_intro_spec_persistent pspec M;
  modality_mixin_spatial : modality_intro_spec_spatial sspec M;
148 149 150
  modality_mixin_emp : emp  M emp;
  modality_mixin_mono P Q : (P  Q)  M P  M Q;
  modality_mixin_sep P Q : M P  M Q  M (P  Q)
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152
}.

153 154 155 156
Record modality (PROP1 PROP2 : bi) := Modality {
  modality_car :> PROP1  PROP2;
  modality_persistent_spec : modality_intro_spec PROP1 PROP2;
  modality_spatial_spec : modality_intro_spec PROP1 PROP2;
157 158
  modality_mixin_of :
    modality_mixin modality_car modality_persistent_spec modality_spatial_spec
Robbert Krebbers's avatar
Robbert Krebbers committed
159
}.
160 161 162
Arguments Modality {_ _} _ {_ _} _.
Arguments modality_persistent_spec {_ _} _.
Arguments modality_spatial_spec {_ _} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
163

164
Section modality.
165
  Context {PROP1 PROP2} (M : modality PROP1 PROP2).
Robbert Krebbers's avatar
Robbert Krebbers committed
166

167 168
  Lemma modality_persistent_transform C P Q :
    modality_persistent_spec M = MIEnvTransform C  C P Q   P  M ( Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  Proof. destruct M as [??? []]; naive_solver. Qed.
170 171
  Lemma modality_and_transform C P Q :
    modality_persistent_spec M = MIEnvTransform C  M P  M Q  M (P  Q).
172
  Proof. destruct M as [??? []]; naive_solver. Qed.
173 174
  Lemma modality_spatial_transform C P Q :
    modality_spatial_spec M = MIEnvTransform C  C P Q  P  M Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  Proof. destruct M as [??? []]; naive_solver. Qed.
176 177
  Lemma modality_spatial_clear P :
    modality_spatial_spec M = MIEnvClear  Absorbing (M P).
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179
  Proof. destruct M as [??? []]; naive_solver. Qed.

180 181 182 183 184 185 186 187 188 189 190 191
  Lemma modality_emp : emp  M emp.
  Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
  Lemma modality_mono P Q : (P  Q)  M P  M Q.
  Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
  Lemma modality_sep P Q : M P  M Q  M (P  Q).
  Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
  Global Instance modality_mono' : Proper (() ==> ()) M.
  Proof. intros P Q. apply modality_mono. Qed.
  Global Instance modality_flip_mono' : Proper (flip () ==> flip ()) M.
  Proof. intros P Q. apply modality_mono. Qed.
  Global Instance modality_proper : Proper (() ==> ()) M.
  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
End modality.

Section modality1.
  Context {PROP} (M : modality PROP PROP).

  Lemma modality_persistent_forall C P :
    modality_persistent_spec M = MIEnvForall C  C P   P  M ( P).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma modality_and_forall C P Q :
    modality_persistent_spec M = MIEnvForall C  M P  M Q  M (P  Q).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma modality_persistent_id P :
    modality_persistent_spec M = MIEnvId   P  M ( P).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma modality_spatial_forall C P :
    modality_spatial_spec M = MIEnvForall C  C P  P  M P.
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma modality_spatial_id P :
    modality_spatial_spec M = MIEnvId  P  M P.
  Proof. destruct M as [??? []]; naive_solver. Qed.
212 213 214

  Lemma modality_persistent_forall_big_and C Ps :
    modality_persistent_spec M = MIEnvForall C 
Robbert Krebbers's avatar
Robbert Krebbers committed
215 216 217
    Forall C Ps   [] Ps  M ( [] Ps).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
218 219 220
    - by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
    - rewrite affinely_persistently_and -modality_and_forall // -IH.
      by rewrite {1}(modality_persistent_forall _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
221
  Qed.
222 223
  Lemma modality_spatial_forall_big_sep C Ps :
    modality_spatial_spec M = MIEnvForall C 
Robbert Krebbers's avatar
Robbert Krebbers committed
224 225 226
    Forall C Ps  [] Ps  M ([] Ps).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
227 228
    - by rewrite -modality_emp.
    - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
229
  Qed.
230
End modality1.
Robbert Krebbers's avatar
Robbert Krebbers committed
231

232 233
Class FromModal {PROP1 PROP2 : bi}
    (M : modality PROP1 PROP2) (P : PROP2) (Q : PROP1) :=
234
  from_modal : M Q  P.
235 236 237
Arguments FromModal {_ _} _ _%I _%I : simpl never.
Arguments from_modal {_ _} _ _%I _%I {_}.
Hint Mode FromModal - + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
238

239 240 241 242 243 244 245 246 247 248
(** The identity modality [modality_id] can be used in combination with
[FromModal modality_id] to support introduction for modalities that enjoy
[P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
which will instruct [iModIntro] to introduce the modality without modifying the
proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
[monPred_relatively] and [bi_absorbingly]. *)
Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
Proof. split; simpl; eauto. Qed.
Definition modality_id {PROP : bi} := Modality (@id PROP) modality_id_mixin.

249 250 251 252 253 254
Class FromAffinely {PROP : bi} (P Q : PROP) :=
  from_affinely : bi_affinely Q  P.
Arguments FromAffinely {_} _%I _%type_scope : simpl never.
Arguments from_affinely {_} _%I _%type_scope {_}.
Hint Mode FromAffinely + ! - : typeclass_instances.
Hint Mode FromAffinely + - ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
255

256 257
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
  into_absorbingly : P  bi_absorbingly Q.
258 259 260 261
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
262

Robbert Krebbers's avatar
Robbert Krebbers committed
263 264 265 266 267 268 269 270 271
(*
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.
272
*)
273

Robbert Krebbers's avatar
Robbert Krebbers committed
274
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
275
  into_wand : ?p R  ?q P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291
Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
Arguments into_wand {_} _ _ _%I _%I _%I {_}.
Hint Mode IntoWand + + + ! - - : typeclass_instances.

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

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

293 294 295 296 297 298 299 300 301 302
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
303 304 305 306 307 308 309 310 311 312 313 314 315
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) :=
316
  into_and : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
317 318
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
319
Hint Mode IntoAnd + + ! - - : typeclass_instances.
320

321 322 323 324 325
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
326

Robbert Krebbers's avatar
Robbert Krebbers committed
327 328 329
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 {_}.
330
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
331

Robbert Krebbers's avatar
Robbert Krebbers committed
332 333 334
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 {_}.
335
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
336

Robbert Krebbers's avatar
Robbert Krebbers committed
337
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
338
  from_exist : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
339 340
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
341
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
342

Robbert Krebbers's avatar
Robbert Krebbers committed
343
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
344
  into_exist : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
345 346
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
347
Hint Mode IntoExist + - ! - : typeclass_instances.
348

Robbert Krebbers's avatar
Robbert Krebbers committed
349
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
350
  into_forall : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
351 352
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
353 354
Hint Mode IntoForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
355
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
356 357 358 359
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
360 361 362 363 364
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.

365 366 367 368 369
Class ElimModal {PROP : bi} (φ : Prop) (P P' : PROP) (Q Q' : PROP) :=
  elim_modal : φ  P  (P' - Q')  Q.
Arguments ElimModal {_} _ _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _ _%I _%I _%I _%I {_}.
Hint Mode ElimModal + - ! - ! - : typeclass_instances.
370

371 372
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
373
Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
374
  add_modal : P  (P' - Q)  Q.
375 376
Arguments AddModal {_} _%I _%I _%I : simpl never.
Arguments add_modal {_} _%I _%I _%I {_}.
377 378
Hint Mode AddModal + - ! ! : typeclass_instances.

379
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
380
Proof. by rewrite /AddModal wand_elim_r. Qed.
381

382 383 384 385 386 387 388 389 390
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.
391

392
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
393 394 395 396
Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.

397 398 399 400
(* 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) :=
401
  maybe_frame : ?p R  Q  P.
402 403 404
Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
Hint Mode MaybeFrame + + ! ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
405 406

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

Robbert Krebbers's avatar
Robbert Krebbers committed
410
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
411
  MaybeFrame true R P P false | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
412 413
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
414
  TCOr (Affine R) (Absorbing P)  MaybeFrame false R P P false | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
415 416
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
417 418 419 420 421 422 423 424 425
(* 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. *)
426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509
Class MakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
  make_embed : P  Q.
Arguments MakeEmbed {_ _ _ _} _%I _%I.
Hint Mode MakeEmbed + + + + - - : typeclass_instances.
Class KnownMakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
  go_make_embed :> MakeEmbed P Q.
Arguments KnownMakeEmbed {_ _ _ _} _%I _%I.
Hint Mode KnownMakeEmbed + + + + ! - : typeclass_instances.

Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P  Q  PQ .
Arguments MakeSep {_} _%I _%I _%I.
Hint Mode MakeSep + - - - : typeclass_instances.
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) := gol_make_sep :> MakeSep P Q PQ.
Arguments KnownLMakeSep {_} _%I _%I _%I.
Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) := gor_make_sep :> MakeSep P Q PQ.
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.
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) := gol_make_and :> MakeAnd P Q PQ.
Arguments KnownLMakeAnd {_} _%I _%I _%I.
Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) := gor_make_and :> MakeAnd P Q PQ.
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.
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) := gol_make_or :> MakeOr P Q PQ.
Arguments KnownLMakeOr {_} _%I _%I _%I.
Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := gor_make_or :> MakeOr P Q PQ.
Arguments KnownRMakeOr {_} _%I _%I _%I.
Hint Mode KnownRMakeOr + - ! - : typeclass_instances.

Class MakeAffinely {PROP : bi} (P Q : PROP) :=
  make_affinely :> bi_affinely P  Q.
Arguments MakeAffinely {_} _%I _%I.
Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
  go_make_affinely : MakeAffinely P Q.
Arguments KnownMakeAffinely {_} _%I _%I.
Hint Mode KnownMakeAffinely + ! - : typeclass_instances.

Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
  make_absorbingly : bi_absorbingly P  Q.
Arguments MakeAbsorbingly {_} _%I _%I.
Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
  go_make_absorbingly :> MakeAbsorbingly P Q.
Arguments KnownMakeAbsorbingly {_} _%I _%I.
Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.

Class MakePersistently {PROP : bi} (P Q : PROP) :=
  make_persistently : bi_persistently P  Q.
Arguments MakePersistently {_} _%I _%I.
Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
  go_make_persistently :> MakePersistently P Q.
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) :=
  go_make_laterN :> MakeLaterN n P lP.
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) :=
  go_make_except_0 :> MakeExcept0 P Q.
Arguments KnownMakeExcept0 {_} _%I _%I.
Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.

510 511 512 513 514 515
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.

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

518 519 520 521
- 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
522

523 524 525
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
526 527 528 529

For binary connectives we have the following instances:

<<
530
IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
531
------------------------------------------
532
     IntoLaterN n (P /\ Q) (P' /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
533 534


535
      IntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
536
-------------------------------
537
IntoLaterN n (P /\ Q) (P /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
538
>>
539 540 541 542 543 544 545 546 547 548

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
549
*)
550
Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
551
  maybe_into_laterN : P  ^n Q.
552 553
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
554
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
555

556
Class IntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
557
  into_laterN :> MaybeIntoLaterN only_head n P Q.
558
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
559
Hint Mode IntoLaterN + + + ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
560

561
Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
562
  MaybeIntoLaterN only_head n P P | 1000.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
Proof. apply laterN_intro. Qed.
564 565 566
(* 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. *)
567 568
Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
569
Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
570 571 572 573 574 575

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

576 577 578 579 580 581 582 583 584 585
(** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
embeddings using [iModIntro].

Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤] *)
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.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
586 587 588 589 590 591 592 593 594 595 596 597
(* We use two type classes for [AsValid], in order to avoid loops in
   typeclass search. Indeed, the [as_valid_embed] instance would try
   to add an arbitrary number of embeddings. To avoid this, the
   [AsValid0] type class cannot handle embeddings, and therefore
   [as_valid_embed] only tries to add one embedding, and we never try
   to insert nested embeddings. This has the additional advantage of
   always trying [as_valid_embed] as a second option, so that this
   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.*)
598 599 600 601 602 603 604 605 606 607 608 609
Class AsValid {PROP : bi} (φ : Prop) (P : PROP) := as_valid : φ  P.
Arguments AsValid {_} _%type _%I.
Class AsValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
  as_valid_here : AsValid φ P.
Arguments AsValid0 {_} _%type _%I.
Existing Instance as_valid_here | 0.

Lemma as_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : φ  P.
Proof. by apply as_valid. Qed.
Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P  φ.
Proof. by apply as_valid. Qed.

610 611
(* Input: [P]; Outputs: [N],
   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Joseph Tassarotti's avatar
Joseph Tassarotti committed
612 613 614 615
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Arguments IntoInv {_} _%I _.
Hint Mode IntoInv + ! - : typeclass_instances.

616 617 618 619 620
(* Input: [Pinv]
   Arguments:
   - [Pinv] is an invariant assertion
   - [Pin] is an additional assertion needed for opening an invariant
   - [Pout] is the assertion obtained by opening the invariant
621
   - [Pclose] is the assertion which contains an update modality to close the invariant
622 623
   - [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
624 625 626 627 628 629

   There are similarities to the definition of ElimModal, however we
   want to be general enough to support uses in settings where there
   is not a clearly associated instance of ElimModal of the right form
   (e.g. to handle Iris 2.0 usage of iInv).
*)
630 631
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
  elim_inv : φ  Pinv  Pin  (Pout  Pclose - Q')  Q.
632 633
Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I _%I.
634
Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
635

636 637 638 639 640 641 642 643 644 645 646 647
(* 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
648
- [Frame] and [MaybeFrame] used by [iFrame]
649
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
Robbert Krebbers's avatar
Robbert Krebbers committed
650
- [IntoPersistent] used by [iPersistent]
651
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
652
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
653
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
654 655
Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
  FromPure a P φ  FromPure a (tc_opaque P) φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
656
Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
657
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
658 659
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
660 661
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.
662
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
663 664 665
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) :
666
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
667
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
668
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
669
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
670
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
671
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
672
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
673
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
674
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
675
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
676
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
677 678
Instance from_modal_tc_opaque {PROP : bi} M (P Q : PROP) :
  FromModal M P Q  FromModal M (tc_opaque P) Q := id.
679 680
Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
  ElimModal φ P P' Q Q'  ElimModal φ (tc_opaque P) P' Q Q' := id.
681 682
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
  IntoInv P N  IntoInv (tc_opaque P) N := id.
683 684 685
Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Pclose Q Q' : PROP) :
  ElimInv φ Pinv Pin Pout Pclose Q Q' 
  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.