classes.v 13.2 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 6 7 8 9
Import bi.

Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
  from_assumption : ?p P  Q.
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
52
Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
53
  into_persistent : ?p P   Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55
Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}.
56
Hint Mode IntoPersistent + + ! - : typeclass_instances.
57

58 59 60 61 62
Class FromPersistent {PROP : bi} (a p : bool) (P Q : PROP) :=
  from_persistent : ?a ?p Q  P.
Arguments FromPersistent {_} _ _ _%I _%I : simpl never.
Arguments from_persistent {_} _ _ _%I _%I {_}.
Hint Mode FromPersistent + - - ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85

Class FromBare {PROP : bi} (P Q : PROP) :=
  from_bare :  Q  P.
Arguments FromBare {_} _%I _%type_scope : simpl never.
Arguments from_bare {_} _%I _%type_scope {_}.
Hint Mode FromBare + ! - : typeclass_instances.
Hint Mode FromBare + - ! : typeclass_instances.

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

(*
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.
86
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
  into_wand : ?p R  ?q P - Q.
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.
105

Robbert Krebbers's avatar
Robbert Krebbers committed
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
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) :=
  into_and : ?p P  ?p (Q1  Q2).
Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Arguments into_and {_} _ _%I _%I _%I {_}.
122
Hint Mode IntoAnd + + ! - - : typeclass_instances.
123

124 125 126 127 128
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
129

Robbert Krebbers's avatar
Robbert Krebbers committed
130 131 132
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 {_}.
133
Hint Mode FromOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
134

Robbert Krebbers's avatar
Robbert Krebbers committed
135 136 137
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 {_}.
138
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
139

Robbert Krebbers's avatar
Robbert Krebbers committed
140
Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
141
  from_exist : ( x, Φ x)  P.
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143
Arguments FromExist {_ _} _%I _%I : simpl never.
Arguments from_exist {_ _} _%I _%I {_}.
144
Hint Mode FromExist + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
145

Robbert Krebbers's avatar
Robbert Krebbers committed
146
Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
147
  into_exist : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
148 149
Arguments IntoExist {_ _} _%I _%I : simpl never.
Arguments into_exist {_ _} _%I _%I {_}.
150
Hint Mode IntoExist + - ! - : typeclass_instances.
151

Robbert Krebbers's avatar
Robbert Krebbers committed
152
Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
153
  into_forall : P   x, Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155
Arguments IntoForall {_ _} _%I _%I : simpl never.
Arguments into_forall {_ _} _%I _%I {_}.
156 157
Hint Mode IntoForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
158
Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :=
159 160 161 162
  from_forall : ( x, Φ x)  P.
Arguments from_forall {_ _} _ _ {_}.
Hint Mode FromForall + - ! - : typeclass_instances.

Robbert Krebbers's avatar
Robbert Krebbers committed
163 164 165 166 167 168 169 170
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 {_}.
171
Hint Mode FromModal + ! - : typeclass_instances.
172

Robbert Krebbers's avatar
Robbert Krebbers committed
173
Class ElimModal {PROP : bi} (P P' : PROP) (Q Q' : PROP) :=
174
  elim_modal : P  (P' - Q')  Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
175 176
Arguments ElimModal {_} _%I _%I _%I _%I : simpl never.
Arguments elim_modal {_} _%I _%I _%I _%I {_}.
177 178
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
179

Robbert Krebbers's avatar
Robbert Krebbers committed
180
Lemma elim_modal_dummy {PROP : bi} (P Q : PROP) : ElimModal P P Q Q.
181
Proof. by rewrite /ElimModal wand_elim_r. Qed.
182

183 184 185 186 187 188 189 190 191
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.
192

Robbert Krebbers's avatar
Robbert Krebbers committed
193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : ?p R  Q  P.
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) :=
  maybe_frame : ?p R  Q  P.
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.

214 215 216 217 218 219
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
220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261
(* 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
default instance is not applied deeply in the term, which may cause in too many
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'
-------------------------------
IntoLaterN n (P /\ Q) (P /\ Q')
>>
*)
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.

262 263 264 265 266 267 268 269 270 271 272 273
(* 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
274
- [Frame] and [MaybeFrame] used by [iFrame]
275
- [IntoLaterN] and [FromLaterN] used by [iNext]
Robbert Krebbers's avatar
Robbert Krebbers committed
276
- [IntoPersistent] used by [iPersistent]
277
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
278
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
279
  IntoPure P φ  IntoPure (tc_opaque P) φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
Instance from_pure_tc_opaque {PROP : bi} (P : PROP) φ :
281
  FromPure P φ  FromPure (tc_opaque P) φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
Instance from_laterN_tc_opaque {PROP : sbi} n (P Q : PROP) :
283
  FromLaterN n P Q  FromLaterN n (tc_opaque P) Q := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
284 285
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.
286
(* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288 289
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) :
290
  IntoAnd p P Q1 Q2  IntoAnd p (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
292
  FromOr P Q1 Q2  FromOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
294
  IntoOr P Q1 Q2  IntoOr (tc_opaque P) Q1 Q2 := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
296
  FromExist P Φ  FromExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
298
  IntoExist P Φ  IntoExist (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A  PROP) :
300
  IntoForall P Φ  IntoForall (tc_opaque P) Φ := id.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
302
  FromModal P Q  FromModal (tc_opaque P) Q := id.
303 304
(* 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
305
Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
306
  ElimModal P P' Q Q'  ElimModal (tc_opaque P) P' Q Q' | 100 := id.