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

Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
6
  from_assumption : ?p P  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9
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
10 11
be used in case of evars *)
Hint Mode FromAssumption + + - - : typeclass_instances.
12

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

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

46 47 48 49 50 51 52 53 54 55
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
56
Proof. by exists φ. Qed.
57 58
Hint Extern 0 (FromPureT _ _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
59

60
Class IntoInternalEq {PROP : sbi} {A : ofeT} (P : PROP) (x y : A) :=
61
  into_internal_eq : P  x  y.
62 63
Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.
Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
64 65
Hint Mode IntoInternalEq + - ! - - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
66
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
67
  into_persistent : bi_persistently_if p P  bi_persistently Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69
Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
70
Hint Mode IntoPersistent + + ! - : typeclass_instances.
71

72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
(* 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
88 89 90 91 92 93 94 95 96 97 98 99
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 {_}.

100 101
(* 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
102 103 104 105 106 107 108 109 110 111 112 113 114 115 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
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
204

205 206 207 208 209 210
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
211

212 213
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
  into_absorbingly : P  bi_absorbingly Q.
214 215 216 217
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
218

Robbert Krebbers's avatar
Robbert Krebbers committed
219 220 221 222 223 224 225 226 227
(*
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.
228
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
230
  into_wand : ?p R  ?q P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
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.
247

248 249 250 251 252 253 254 255 256 257
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
258 259 260 261 262 263 264 265 266 267 268 269 270
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) :=
271
  into_and : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
272 273
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
274
Hint Mode IntoAnd + + ! - - : typeclass_instances.
275

276 277 278 279 280
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
281

Robbert Krebbers's avatar
Robbert Krebbers committed
282 283 284
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 {_}.
285
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
286

Robbert Krebbers's avatar
Robbert Krebbers committed
287 288 289
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 {_}.
290
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
291

Robbert Krebbers's avatar
Robbert Krebbers committed
292
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
293
  from_exist : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
296
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
297

Robbert Krebbers's avatar
Robbert Krebbers committed
298
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
299
  into_exist : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
300 301
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
302
Hint Mode IntoExist + - ! - : typeclass_instances.
303

Robbert Krebbers's avatar
Robbert Krebbers committed
304
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
305
  into_forall : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
306 307
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
308 309
Hint Mode IntoForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
310
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
311 312 313 314
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
315 316 317 318 319 320 321 322
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 {_}.
323
Hint Mode FromModal + ! - : typeclass_instances.
324

Robbert Krebbers's avatar
Robbert Krebbers committed
325
Class ElimModal {PROP : bi} (P P' : PROP) (Q Q' : PROP) :=
326
  elim_modal : P  (P' - Q')  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
327 328
Arguments ElimModal {_} _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _%I _%I _%I _%I {_}.
329
Hint Mode ElimModal + ! - ! - : typeclass_instances.
330

331 332
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
333
Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
334
  add_modal : P  (P' - Q)  Q.
335 336
Arguments AddModal {_} _%I _%I _%I : simpl never.
Arguments add_modal {_} _%I _%I _%I {_}.
337 338
Hint Mode AddModal + - ! ! : typeclass_instances.

339
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
340
Proof. by rewrite /AddModal wand_elim_r. Qed.
341

342 343 344 345 346 347 348 349 350
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.
351

352
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
353 354 355 356 357
Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.

Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
358
  maybe_frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
359 360 361 362 363 364 365 366 367 368 369 370 371 372
Arguments MaybeFrame {_} _ _%I _%I _%I.
Arguments maybe_frame {_} _%I _%I _%I {_}.
Hint Mode MaybeFrame + + ! ! - : typeclass_instances.

Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
  Frame p R P Q  MaybeFrame p R P Q.
Proof. done. Qed.
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
  MaybeFrame true R P P | 100.
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
  TCOr (Affine R) (Absorbing P)  MaybeFrame false R P P | 100.
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
379 380 381 382 383 384 385 386
(* The class [IntoLaterN] has only two instances:

- The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN' n P Q → IntoLaterN n P Q], where [IntoLaterN']
  is identical to [IntoLaterN], but computationally is supposed to make
  progress, i.e. its instances should actually strip a later.

The point of using the auxilary class [IntoLaterN'] is to ensure that the
387
default instance is not applied deeply in the term, which may result in too many
Robbert Krebbers's avatar
Robbert Krebbers committed
388 389 390 391 392 393 394 395 396 397 398 399
definitions being unfolded (see issue #55).

For binary connectives we have the following instances:

<<
IntoLaterN' n P P'       IntoLaterN n Q Q'
------------------------------------------
     IntoLaterN' n (P /\ Q) (P' /\ Q')


      IntoLaterN' n Q Q'
-------------------------------
400
IntoLaterN' n (P /\ Q) (P /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420
>>
*)
Class IntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) := into_laterN : P  ^n Q.
Arguments IntoLaterN {_} _%nat_scope _%I _%I.
Arguments into_laterN {_} _%nat_scope _%I _%I {_}.
Hint Mode IntoLaterN + - - - : typeclass_instances.

Class IntoLaterN' {PROP : sbi} (n : nat) (P Q : PROP) :=
  into_laterN' :> IntoLaterN n P Q.
Arguments IntoLaterN' {_} _%nat_scope _%I _%I.
Hint Mode IntoLaterN' + - ! - : typeclass_instances.

Instance into_laterN_default {PROP : sbi} n (P : PROP) : IntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.

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.

421 422 423 424 425 426 427 428 429 430 431 432 433
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.

434 435 436 437 438 439 440 441 442 443 444 445
(* 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
446
- [Frame] and [MaybeFrame] used by [iFrame]
447
- [IntoLaterN] and [FromLaterN] used by [iNext]
Robbert Krebbers's avatar
Robbert Krebbers committed
448
- [IntoPersistent] used by [iPersistent]
449
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
450
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
451
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
452 453
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
454
Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
455
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
456 457
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
458 459
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.
460
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
461 462 463
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) :
464
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
465
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
466
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
468
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
469
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
470
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
472
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
473
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
474
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
475
Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
476
  FromModal P Q  FromModal (tc_opaque P) Q := id.
477 478
(* Higher precedence than [elim_modal_timeless], so that [iAssert] does not
   loop (see test [test_iAssert_modality] in proofmode.v). *)
Robbert Krebbers's avatar
Robbert Krebbers committed
479
Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
480
  ElimModal P P' Q Q'  ElimModal (tc_opaque P) P' Q Q' | 100 := id.