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

Robbert Krebbers's avatar
Robbert Krebbers committed
46 47 48 49
Class FromPure {PROP : bi} (P : PROP) (φ : Prop) :=
  from_pure : ⌜φ⌝  P.
Arguments FromPure {_} _%I _%type_scope : simpl never.
Arguments from_pure {_} _%I _%type_scope {_}.
50 51
Hint Mode FromPure + ! - : typeclass_instances.

52
Class FromPureT {PROP : bi} (P : PROP) (φ : Type) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  from_pureT :  ψ : Prop, φ = ψ  FromPure P ψ.
54
Lemma from_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : FromPure P φ  FromPureT P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56 57 58
Proof. by exists φ. Qed.
Hint Extern 0 (FromPureT _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.

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

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

71 72 73 74 75
Class FromAlways {PROP : bi} (a pe pl : bool) (P Q : PROP) :=
  from_always : bi_affinely_if a (bi_persistently_if pe (bi_plainly_if pl 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
76

77 78 79 80 81 82
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
83

84 85
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
  into_absorbingly : P  bi_absorbingly Q.
86 87 88 89
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
90

Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93 94 95 96 97 98 99
(*
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.
100
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
102
  into_wand : ?p R  ?q P - Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
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.
119

120 121 122 123 124 125 126 127 128 129
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
130 131 132 133 134 135 136 137 138 139 140 141 142
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) :=
143
  into_and : ?p P  ?p (Q1  Q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
146
Hint Mode IntoAnd + + ! - - : typeclass_instances.
147

148 149 150 151 152
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
153

Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156
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 {_}.
157
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
158

Robbert Krebbers's avatar
Robbert Krebbers committed
159 160 161
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 {_}.
162
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
163

Robbert Krebbers's avatar
Robbert Krebbers committed
164
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
165
  from_exist : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
168
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
169

Robbert Krebbers's avatar
Robbert Krebbers committed
170
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
171
  into_exist : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
172 173
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
174
Hint Mode IntoExist + - ! - : typeclass_instances.
175

Robbert Krebbers's avatar
Robbert Krebbers committed
176
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
177
  into_forall : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
180 181
Hint Mode IntoForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
182
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
183 184 185 186
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
187 188 189 190 191 192 193 194
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 {_}.
195
Hint Mode FromModal + ! - : typeclass_instances.
196

Robbert Krebbers's avatar
Robbert Krebbers committed
197
Class ElimModal {PROP : bi} (P P' : PROP) (Q Q' : PROP) :=
198
  elim_modal : P  (P' - Q')  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200
Arguments ElimModal {_} _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _%I _%I _%I _%I {_}.
201
Hint Mode ElimModal + ! - ! - : typeclass_instances.
202

203 204
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
205
Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
206
  add_modal : P  (P' - Q)  Q.
207 208
Arguments AddModal {_} _%I _%I _%I : simpl never.
Arguments add_modal {_} _%I _%I _%I {_}.
209 210
Hint Mode AddModal + - ! ! : typeclass_instances.

211
Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
212
Proof. by rewrite /AddModal wand_elim_r. Qed.
213

214 215 216 217 218 219 220 221 222
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.
223

224
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
225 226 227 228 229
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) :=
230
  maybe_frame : ?p R  Q  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
231 232 233 234 235 236 237 238 239 240 241 242 243 244
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.

245 246 247 248 249 250
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
251 252 253 254 255 256 257 258
(* 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
259
default instance is not applied deeply in the term, which may result in too many
Robbert Krebbers's avatar
Robbert Krebbers committed
260 261 262 263 264 265 266 267 268 269 270 271
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'
-------------------------------
272
IntoLaterN' n (P /\ Q) (P /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
>>
*)
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.

293 294 295 296 297 298 299 300 301 302 303 304 305
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.

306 307 308 309 310 311 312 313 314 315 316 317
(* 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
318
- [Frame] and [MaybeFrame] used by [iFrame]
319
- [IntoLaterN] and [FromLaterN] used by [iNext]
Robbert Krebbers's avatar
Robbert Krebbers committed
320
- [IntoPersistent] used by [iPersistent]
321
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
322
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
323
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
Instance from_pure_tc_opaque {PROP : bi} (P : PROP) φ :
325
  FromPure P φ  FromPure (tc_opaque P) φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
326
Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
327
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
328 329
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
330 331
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.
332
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
333 334 335
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) :
336
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
338
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
340
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
342
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
344
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
346
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
347
Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
348
  FromModal P Q  FromModal (tc_opaque P) Q := id.
349 350
(* 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
351
Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
352
  ElimModal P P' Q Q'  ElimModal (tc_opaque P) P' Q Q' | 100 := id.