classes.v 29 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 88 89 90 91 92 93 94 95 96 97 98 99 100 101
(* The `iAlways` tactic is not tied to `persistently` and `affinely`, but can be
instantiated with a variety of comonadic (always-style) modalities.

In order to plug in an always-style modality, one has to decide for both the
persistent and spatial what action should be performed upon introducing the
modality:

- 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).
- Introduction will only keep the hypotheses that satisfy some predicate
  `C : PROP → Prop` (where `C` should be a type class).
- Introduction will clear the context.
- Introduction will keep the context as-if.

Formally, these actions correspond to the following inductive type: *)
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105 106 107 108 109 110 111 112 113
Inductive always_intro_spec (PROP : bi) :=
  | AIEnvIsEmpty
  | AIEnvForall (C : PROP  Prop)
  | AIEnvFilter (C : PROP  Prop)
  | AIEnvClear
  | AIEnvId.
Arguments AIEnvIsEmpty {_}.
Arguments AIEnvForall {_} _.
Arguments AIEnvFilter {_} _.
Arguments AIEnvClear {_}.
Arguments AIEnvId {_}.

114 115
(* An always-style modality is then a record packing together the modality with
the laws it should satisfy to justify the given actions for both contexts: *)
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
Record always_modality_mixin {PROP : bi} (M : PROP  PROP)
    (pspec sspec : always_intro_spec PROP) := {
  always_modality_mixin_persistent :
    match pspec with
    | AIEnvIsEmpty => True
    | AIEnvForall C | AIEnvFilter C =>  P, C P   P  M ( P)
    | AIEnvClear => True
    | AIEnvId =>  P,  P  M ( P)
    end;
  always_modality_mixin_spatial :
    match sspec with
    | AIEnvIsEmpty => True
    | AIEnvForall C =>  P, C P  P  M P
    | AIEnvFilter C => ( P, C P  P  M P)  ( P, Absorbing (M P))
    | AIEnvClear =>  P, Absorbing (M P)
    | AIEnvId => False
    end;
  always_modality_mixin_emp : emp  M emp;
  always_modality_mixin_mono P Q : (P  Q)  M P  M Q;
  always_modality_mixin_and P Q : M P  M Q  M (P  Q);
  always_modality_mixin_sep P Q : M P  M Q  M (P  Q)
}.

Record always_modality (PROP : bi) := AlwaysModality {
  always_modality_car :> PROP  PROP;
  always_modality_persistent_spec : always_intro_spec PROP;
  always_modality_spatial_spec : always_intro_spec PROP;
  always_modality_mixin_of : always_modality_mixin
    always_modality_car
    always_modality_persistent_spec always_modality_spatial_spec
}.
Arguments AlwaysModality {_} _ {_ _} _.
Arguments always_modality_persistent_spec {_} _.
Arguments always_modality_spatial_spec {_} _.

Section always_modality.
  Context {PROP} (M : always_modality PROP).

  Lemma always_modality_persistent_forall C P :
    always_modality_persistent_spec M = AIEnvForall C  C P   P  M ( P).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma always_modality_persistent_filter C P :
    always_modality_persistent_spec M = AIEnvFilter C  C P   P  M ( P).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma always_modality_persistent_id P :
    always_modality_persistent_spec M = AIEnvId   P  M ( P).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma always_modality_spatial_forall C P :
    always_modality_spatial_spec M = AIEnvForall C  C P  P  M P.
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma always_modality_spatial_filter C P :
    always_modality_spatial_spec M = AIEnvFilter C  C P  P  M P.
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma always_modality_spatial_filter_absorbing C P :
    always_modality_spatial_spec M = AIEnvFilter C  Absorbing (M P).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma always_modality_spatial_clear P :
    always_modality_spatial_spec M = AIEnvClear  Absorbing (M P).
  Proof. destruct M as [??? []]; naive_solver. Qed.
  Lemma always_modality_spatial_id :
    always_modality_spatial_spec M  AIEnvId.
  Proof. destruct M as [??? []]; naive_solver. Qed.

  Lemma always_modality_emp : emp  M emp.
  Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
  Lemma always_modality_mono P Q : (P  Q)  M P  M Q.
  Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
  Lemma always_modality_and P Q : M P  M Q  M (P  Q).
  Proof. eapply always_modality_mixin_and, always_modality_mixin_of. Qed.
  Lemma always_modality_sep P Q : M P  M Q  M (P  Q).
  Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
  Global Instance always_modality_mono' : Proper (() ==> ()) M.
  Proof. intros P Q. apply always_modality_mono. Qed.
  Global Instance always_modality_flip_mono' : Proper (flip () ==> flip ()) M.
  Proof. intros P Q. apply always_modality_mono. Qed.
  Global Instance always_modality_proper : Proper (() ==> ()) M.
  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using always_modality_mono. Qed.

  Lemma always_modality_persistent_forall_big_and C Ps :
    always_modality_persistent_spec M = AIEnvForall C 
    Forall C Ps   [] Ps  M ( [] Ps).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
    - by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
    - rewrite affinely_persistently_and -always_modality_and -IH.
      by rewrite {1}(always_modality_persistent_forall _ P).
  Qed.
  Lemma always_modality_spatial_forall_big_sep C Ps :
    always_modality_spatial_spec M = AIEnvForall C 
    Forall C Ps  [] Ps  M ([] Ps).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
    - by rewrite -always_modality_emp.
    - by rewrite -always_modality_sep -IH {1}(always_modality_spatial_forall _ P).
  Qed.
End always_modality.

Class FromAlways {PROP : bi} (M : always_modality PROP) (P Q : PROP) :=
  from_always : M Q  P.
Arguments FromAlways {_} _ _%I _%I : simpl never.
Arguments from_always {_} _ _%I _%I {_}.
Hint Mode FromAlways + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
218

219 220 221 222 223 224
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
225

226 227
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
  into_absorbingly : P  bi_absorbingly Q.
228 229 230 231
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
232

Robbert Krebbers's avatar
Robbert Krebbers committed
233 234 235 236 237 238 239 240 241
(*
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.
242
*)
243

Robbert Krebbers's avatar
Robbert Krebbers committed
244
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
245
  into_wand : ?p R  ?q P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
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.
262

263 264 265 266 267 268 269 270 271 272
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
273 274 275 276 277 278 279 280 281 282 283 284 285
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) :=
286
  into_and : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
289
Hint Mode IntoAnd + + ! - - : typeclass_instances.
290

291 292 293 294 295
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
296

Robbert Krebbers's avatar
Robbert Krebbers committed
297 298 299
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 {_}.
300
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
301

Robbert Krebbers's avatar
Robbert Krebbers committed
302 303 304
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 {_}.
305
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
306

Robbert Krebbers's avatar
Robbert Krebbers committed
307
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
308
  from_exist : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
309 310
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
311
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
312

Robbert Krebbers's avatar
Robbert Krebbers committed
313
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
314
  into_exist : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
315 316
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
317
Hint Mode IntoExist + - ! - : typeclass_instances.
318

Robbert Krebbers's avatar
Robbert Krebbers committed
319
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
320
  into_forall : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
323 324
Hint Mode IntoForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
325
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
326 327 328 329
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
330 331 332 333 334 335 336 337
Class IsExcept0 {PROP : sbi} (Q : PROP) := is_except_0 :  Q  Q.
Arguments IsExcept0 {_} _%I : simpl never.
Arguments is_except_0 {_} _%I {_}.
Hint Mode IsExcept0 + ! : typeclass_instances.

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

340 341 342 343 344
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.
345

346 347
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
348
Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
349
  add_modal : P  (P' - Q)  Q.
350 351
Arguments AddModal {_} _%I _%I _%I : simpl never.
Arguments add_modal {_} _%I _%I _%I {_}.
352 353
Hint Mode AddModal + - ! ! : typeclass_instances.

354
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
355
Proof. by rewrite /AddModal wand_elim_r. Qed.
356

357 358 359 360 361 362 363 364 365
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.
366

367
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
368 369 370 371
Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.

372 373 374 375
(* 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) :=
376
  maybe_frame : ?p R  Q  P.
377 378 379
Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
Hint Mode MaybeFrame + + ! ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
380 381

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

Robbert Krebbers's avatar
Robbert Krebbers committed
385
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
386
  MaybeFrame true R P P false | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
387 388
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
389
  TCOr (Affine R) (Absorbing P)  MaybeFrame false R P P false | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
390 391
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
392 393 394 395 396 397 398 399 400
(* 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. *)
401 402 403 404 405
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') :=
406
  known_make_embed :> MakeEmbed P Q.
407 408 409 410 411 412
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.
413 414
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_sep :> MakeSep P Q PQ.
415 416
Arguments KnownLMakeSep {_} _%I _%I _%I.
Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
417 418
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
  knownr_make_sep :> MakeSep P Q PQ.
419 420 421 422 423 424
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.
425 426
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_and :> MakeAnd P Q PQ.
427 428
Arguments KnownLMakeAnd {_} _%I _%I _%I.
Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
429 430
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
  knownr_make_and :> MakeAnd P Q PQ.
431 432 433 434 435 436
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.
437 438
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
  knownl_make_or :> MakeOr P Q PQ.
439 440
Arguments KnownLMakeOr {_} _%I _%I _%I.
Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
441
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
442 443 444 445
Arguments KnownRMakeOr {_} _%I _%I _%I.
Hint Mode KnownRMakeOr + - ! - : typeclass_instances.

Class MakeAffinely {PROP : bi} (P Q : PROP) :=
446
  make_affinely : bi_affinely P  Q.
447 448 449
Arguments MakeAffinely {_} _%I _%I.
Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
450
  known_make_affinely :> MakeAffinely P Q.
451 452 453 454 455 456 457 458
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) :=
459
  known_make_absorbingly :> MakeAbsorbingly P Q.
460 461 462 463 464 465 466 467
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) :=
468
  known_make_persistently :> MakePersistently P Q.
469 470 471 472 473 474 475 476
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) :=
477
  known_make_laterN :> MakeLaterN n P lP.
478 479 480 481 482 483 484 485
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) :=
486
  known_make_except_0 :> MakeExcept0 P Q.
487 488 489
Arguments KnownMakeExcept0 {_} _%I _%I.
Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.

490 491 492 493 494 495
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.

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

498 499 500 501
- 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
502

503 504 505
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
506 507 508 509

For binary connectives we have the following instances:

<<
510
IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
511
------------------------------------------
512
     IntoLaterN n (P /\ Q) (P' /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
513 514


515
      IntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
516
-------------------------------
517
IntoLaterN n (P /\ Q) (P /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
518
>>
519 520 521 522 523 524 525 526 527 528

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
529
*)
530
Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
531
  maybe_into_laterN : P  ^n Q.
532 533
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
534
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
535

536
Class IntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
537
  into_laterN :> MaybeIntoLaterN only_head n P Q.
538
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
539
Hint Mode IntoLaterN + + + ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
540

541
Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
542
  MaybeIntoLaterN only_head n P P | 1000.
Robbert Krebbers's avatar
Robbert Krebbers committed
543
Proof. apply laterN_intro. Qed.
544 545 546
(* 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. *)
547 548
Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
549
Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
550 551 552 553 554 555

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.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
556 557 558 559 560 561 562 563 564 565 566 567
(* 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.*)
568 569 570 571 572 573 574 575 576 577 578 579
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.

580 581
(* Input: [P]; Outputs: [N],
   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Joseph Tassarotti's avatar
Joseph Tassarotti committed
582 583 584 585
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Arguments IntoInv {_} _%I _.
Hint Mode IntoInv + ! - : typeclass_instances.

586 587 588 589 590
(* 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
591
   - [Pclose] is the assertion which contains an update modality to close the invariant
592 593
   - [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
594 595 596 597 598 599

   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).
*)
600 601
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
  elim_inv : φ  Pinv  Pin  (Pout  Pclose - Q')  Q.
602 603
Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I _%I.
604
Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
605

606 607 608 609 610 611 612 613 614 615 616 617
(* 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
618
- [Frame] and [MaybeFrame] used by [iFrame]
619
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
Robbert Krebbers's avatar
Robbert Krebbers committed
620
- [IntoPersistent] used by [iPersistent]
621
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
622
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
623
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
624 625
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
626
Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
627
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
628 629
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
630 631
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.
632
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
633 634 635
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) :
636
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
637
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
638
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
639
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
640
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
641
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
642
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
643
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
644
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
645
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
646
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
647
Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
648
  FromModal P Q  FromModal (tc_opaque P) Q := id.
649 650
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.
651 652
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
  IntoInv P N  IntoInv (tc_opaque P) N := id.
653 654 655
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.