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

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

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

20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
(* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
some shortcoming of unification in Coq's type class search. An example where we
use this workaround is to repair the following instance:

  Global Instance into_exist_and_pure P Q (φ : Prop) :
    IntoPure P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).

Coq is unable to use this instance: [class_apply] -- which is used by type class
search -- fails with the error that it cannot unify [Prop] and [Type]. This is
probably caused because [class_apply] uses an ancient unification algorith. The
[refine] tactic -- which uses a better unification algorithm -- succeeds to
apply the above instance.

Since we do not want to define [Hint Extern] declarations using [refine] for
any instance like [into_exist_and_pure], we factor this out in the class
[IntoPureT]. This way, we only have to declare a [Hint Extern] using [refine]
once, and use [IntoPureT] in any instance like [into_exist_and_pure].

TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
to be finished and merged someday. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Class IntoPureT {PROP : bi} (P : PROP) (φ : Type) :=
41
  into_pureT :  ψ : Prop, φ = ψ  IntoPure P ψ.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Lemma into_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ  IntoPureT P φ.
43 44 45 46
Proof. by exists φ. Qed.
Hint Extern 0 (IntoPureT _ _) =>
  notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
47 48
(** [FromPure] is used when introducing a pure assertion. It is used
    by iPure, the "[%]" specialization pattern, and the [with "[%]"]
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
49
    pattern when using [iAssert].
50

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
51 52 53
    The [a] Boolean asserts whether we introduce the pure assertion in
    an affine way or in an absorbing way. When [FromPure true P φ] is
    derived, then [FromPure false P φ] can always be derived too. We
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
54 55
    use [true] for specialization patterns and [false] for the
    [iPureIntro] tactic.
56

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
57 58 59
    This Boolean is not needed for [IntoPure], because in the case of
    [IntoPure], we can have the same behavior by asking that [P] be
    [Affine]. *)
60 61 62 63 64 65 66 67 68 69
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
  from_pure : bi_affinely_if a ⌜φ⌝  P.
Arguments FromPure {_} _ _%I _%type_scope : simpl never.
Arguments from_pure {_} _ _%I _%type_scope {_}.
Hint Mode FromPure + + ! - : typeclass_instances.

Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
  from_pureT :  ψ : Prop, φ = ψ  FromPure a P ψ.
Lemma from_pureT_hint {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
  FromPure a P φ  FromPureT a P φ.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof. by exists φ. Qed.
71 72
Hint Extern 0 (FromPureT _ _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
73

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

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

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

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

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

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

104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
Inductive modality_intro_spec (PROP : bi) :=
  | MIEnvIsEmpty
  | MIEnvForall (C : PROP  Prop)
  | MIEnvTransform (C : PROP  PROP  Prop)
  | MIEnvClear
  | MIEnvId.
Arguments MIEnvIsEmpty {_}.
Arguments MIEnvForall {_} _.
Arguments MIEnvTransform {_} _.
Arguments MIEnvClear {_}.
Arguments MIEnvId {_}.

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

(* A modality is then a record packing together the modality with the laws it
should satisfy to justify the given actions for both contexts: *)
Record modality_mixin {PROP : bi} (M : PROP  PROP)
    (pspec sspec : modality_intro_spec PROP) := {
  modality_mixin_persistent :
Robbert Krebbers's avatar
Robbert Krebbers committed
123
    match pspec with
124 125 126 127 128
    | MIEnvIsEmpty => True
    | MIEnvForall C => ( P, C P   P  M ( P))  ( P Q, M P  M Q  M (P  Q))
    | MIEnvTransform C => ( P Q, C P Q   P  M ( Q))  ( P Q, M P  M Q  M (P  Q))
    | MIEnvClear => True
    | MIEnvId =>  P,  P  M ( P)
Robbert Krebbers's avatar
Robbert Krebbers committed
129
    end;
130
  modality_mixin_spatial :
Robbert Krebbers's avatar
Robbert Krebbers committed
131
    match sspec with
132 133 134 135 136
    | MIEnvIsEmpty => True
    | MIEnvForall C =>  P, C P  P  M P
    | MIEnvTransform C => ( P Q, C P Q  P  M Q)
    | MIEnvClear =>  P, Absorbing (M P)
    | MIEnvId =>  P, P  M P
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    end;
138 139 140
  modality_mixin_emp : emp  M emp;
  modality_mixin_mono P Q : (P  Q)  M P  M Q;
  modality_mixin_sep P Q : M P  M Q  M (P  Q)
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142
}.

143 144 145 146 147 148
Record modality (PROP : bi) := Modality {
  modality_car :> PROP  PROP;
  modality_persistent_spec : modality_intro_spec PROP;
  modality_spatial_spec : modality_intro_spec PROP;
  modality_mixin_of :
    modality_mixin modality_car modality_persistent_spec modality_spatial_spec
Robbert Krebbers's avatar
Robbert Krebbers committed
149
}.
150 151 152
Arguments Modality {_} _ {_ _} _.
Arguments modality_persistent_spec {_} _.
Arguments modality_spatial_spec {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
153

154 155
Section modality.
  Context {PROP} (M : modality PROP).
Robbert Krebbers's avatar
Robbert Krebbers committed
156

157 158
  Lemma modality_persistent_forall C P :
    modality_persistent_spec M = MIEnvForall C  C P   P  M ( P).
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  Proof. destruct M as [??? []]; naive_solver. Qed.
160 161
  Lemma modality_and_forall C P Q :
    modality_persistent_spec M = MIEnvForall C  M P  M Q  M (P  Q).
162
  Proof. destruct M as [??? []]; naive_solver. Qed.
163 164
  Lemma modality_persistent_transform C P Q :
    modality_persistent_spec M = MIEnvTransform C  C P Q   P  M ( Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  Proof. destruct M as [??? []]; naive_solver. Qed.
166 167
  Lemma modality_and_transform C P Q :
    modality_persistent_spec M = MIEnvTransform C  M P  M Q  M (P  Q).
168
  Proof. destruct M as [??? []]; naive_solver. Qed.
169 170
  Lemma modality_persistent_id P :
    modality_persistent_spec M = MIEnvId   P  M ( P).
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  Proof. destruct M as [??? []]; naive_solver. Qed.
172 173
  Lemma modality_spatial_forall C P :
    modality_spatial_spec M = MIEnvForall C  C P  P  M P.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  Proof. destruct M as [??? []]; naive_solver. Qed.
175 176
  Lemma modality_spatial_transform C P Q :
    modality_spatial_spec M = MIEnvTransform C  C P Q  P  M Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  Proof. destruct M as [??? []]; naive_solver. Qed.
178 179
  Lemma modality_spatial_clear P :
    modality_spatial_spec M = MIEnvClear  Absorbing (M P).
Robbert Krebbers's avatar
Robbert Krebbers committed
180
  Proof. destruct M as [??? []]; naive_solver. Qed.
181 182
  Lemma modality_spatial_id P :
    modality_spatial_spec M = MIEnvId  P  M P.
Robbert Krebbers's avatar
Robbert Krebbers committed
183 184
  Proof. destruct M as [??? []]; naive_solver. Qed.

185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
  Lemma modality_emp : emp  M emp.
  Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
  Lemma modality_mono P Q : (P  Q)  M P  M Q.
  Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
  Lemma modality_sep P Q : M P  M Q  M (P  Q).
  Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
  Global Instance modality_mono' : Proper (() ==> ()) M.
  Proof. intros P Q. apply modality_mono. Qed.
  Global Instance modality_flip_mono' : Proper (flip () ==> flip ()) M.
  Proof. intros P Q. apply modality_mono. Qed.
  Global Instance modality_proper : Proper (() ==> ()) M.
  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using modality_mono. Qed.

  Lemma modality_persistent_forall_big_and C Ps :
    modality_persistent_spec M = MIEnvForall C 
Robbert Krebbers's avatar
Robbert Krebbers committed
200 201 202
    Forall C Ps   [] Ps  M ( [] Ps).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
203 204 205
    - by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
    - rewrite affinely_persistently_and -modality_and_forall // -IH.
      by rewrite {1}(modality_persistent_forall _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  Qed.
207 208
  Lemma modality_spatial_forall_big_sep C Ps :
    modality_spatial_spec M = MIEnvForall C 
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210 211
    Forall C Ps  [] Ps  M ([] Ps).
  Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
212 213
    - by rewrite -modality_emp.
    - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
Robbert Krebbers's avatar
Robbert Krebbers committed
214
  Qed.
215
End modality.
Robbert Krebbers's avatar
Robbert Krebbers committed
216

217 218 219 220 221
Class FromModal {PROP : bi} (M : modality PROP) (P Q : PROP) :=
  from_modal : M Q  P.
Arguments FromModal {_} _ _%I _%I : simpl never.
Arguments from_modal {_} _ _%I _%I {_}.
Hint Mode FromModal + - ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
222

223 224 225 226 227 228
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
229

230 231
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
  into_absorbingly : P  bi_absorbingly Q.
232 233 234 235
Arguments IntoAbsorbingly {_} _%I _%I.
Arguments into_absorbingly {_} _%I _%I {_}.
Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
236

Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239 240 241 242 243 244 245
(*
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.
246
*)
247

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

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

295 296 297 298 299
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
300

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

Robbert Krebbers's avatar
Robbert Krebbers committed
306 307 308
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 {_}.
309
Hint Mode IntoOr + ! - - : typeclass_instances.
Robbert Krebbers's avatar
Oops!  
Robbert Krebbers committed
310

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
334 335 336 337 338
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.

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

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

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

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

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

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

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

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

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
391 392 393 394 395 396 397 398 399
(* 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. *)
400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483
Class MakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
  make_embed : P  Q.
Arguments MakeEmbed {_ _ _ _} _%I _%I.
Hint Mode MakeEmbed + + + + - - : typeclass_instances.
Class KnownMakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
  go_make_embed :> MakeEmbed P Q.
Arguments KnownMakeEmbed {_ _ _ _} _%I _%I.
Hint Mode KnownMakeEmbed + + + + ! - : typeclass_instances.

Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P  Q  PQ .
Arguments MakeSep {_} _%I _%I _%I.
Hint Mode MakeSep + - - - : typeclass_instances.
Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) := gol_make_sep :> MakeSep P Q PQ.
Arguments KnownLMakeSep {_} _%I _%I _%I.
Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) := gor_make_sep :> MakeSep P Q PQ.
Arguments KnownRMakeSep {_} _%I _%I _%I.
Hint Mode KnownRMakeSep + - ! - : typeclass_instances.

Class MakeAnd {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P  Q  PQ.
Arguments MakeAnd {_} _%I _%I _%I.
Hint Mode MakeAnd + - - - : typeclass_instances.
Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) := gol_make_and :> MakeAnd P Q PQ.
Arguments KnownLMakeAnd {_} _%I _%I _%I.
Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) := gor_make_and :> MakeAnd P Q PQ.
Arguments KnownRMakeAnd {_} _%I _%I _%I.
Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.

Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P  Q  PQ.
Arguments MakeOr {_} _%I _%I _%I.
Hint Mode MakeOr + - - - : typeclass_instances.
Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) := gol_make_or :> MakeOr P Q PQ.
Arguments KnownLMakeOr {_} _%I _%I _%I.
Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := gor_make_or :> MakeOr P Q PQ.
Arguments KnownRMakeOr {_} _%I _%I _%I.
Hint Mode KnownRMakeOr + - ! - : typeclass_instances.

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

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

Class MakePersistently {PROP : bi} (P Q : PROP) :=
  make_persistently : bi_persistently P  Q.
Arguments MakePersistently {_} _%I _%I.
Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
  go_make_persistently :> MakePersistently P Q.
Arguments KnownMakePersistently {_} _%I _%I.
Hint Mode KnownMakePersistently + ! - : typeclass_instances.

Class MakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
  make_laterN : ^n P  lP.
Arguments MakeLaterN {_} _%nat _%I _%I.
Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : sbi} (n : nat) (P lP : PROP) :=
  go_make_laterN :> MakeLaterN n P lP.
Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.

Class MakeExcept0 {PROP : sbi} (P Q : PROP) :=
  make_except_0 : sbi_except_0 P  Q.
Arguments MakeExcept0 {_} _%I _%I.
Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : sbi} (P Q : PROP) :=
  go_make_except_0 :> MakeExcept0 P Q.
Arguments KnownMakeExcept0 {_} _%I _%I.
Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.

484 485 486 487 488 489
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.

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

492 493 494 495
- 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
496

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

For binary connectives we have the following instances:

<<
504
IntoLaterN n P P'       MaybeIntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
505
------------------------------------------
506
     IntoLaterN n (P /\ Q) (P' /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
507 508


509
      IntoLaterN n Q Q'
Robbert Krebbers's avatar
Robbert Krebbers committed
510
-------------------------------
511
IntoLaterN n (P /\ Q) (P /\ Q')
Robbert Krebbers's avatar
Robbert Krebbers committed
512
>>
513 514 515 516 517 518 519 520 521 522

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
523
*)
524
Class MaybeIntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
525
  maybe_into_laterN : P  ^n Q.
526 527
Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
528
Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
529

530
Class IntoLaterN {PROP : sbi} (only_head : bool) (n : nat) (P Q : PROP) :=
531
  into_laterN :> MaybeIntoLaterN only_head n P Q.
532
Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
533
Hint Mode IntoLaterN + + + ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
534

535
Instance maybe_into_laterN_default {PROP : sbi} only_head n (P : PROP) :
536
  MaybeIntoLaterN only_head n P P | 1000.
Robbert Krebbers's avatar
Robbert Krebbers committed
537
Proof. apply laterN_intro. Qed.
538 539 540
(* 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. *)
541 542
Instance maybe_into_laterN_default_0 {PROP : sbi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
543
Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
544 545 546 547 548 549

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
550 551 552 553 554 555 556 557 558 559 560 561
(* 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.*)
562 563 564 565 566 567 568 569 570 571 572 573
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.

574 575
(* Input: [P]; Outputs: [N],
   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Joseph Tassarotti's avatar
Joseph Tassarotti committed
576 577 578 579
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Arguments IntoInv {_} _%I _.
Hint Mode IntoInv + ! - : typeclass_instances.

580 581 582 583 584
(* 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
585
   - [Pclose] is the assertion which contains an update modality to close the invariant
586 587
   - [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
588 589 590 591 592 593

   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).
*)
594 595
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
  elim_inv : φ  Pinv  Pin  (Pout  Pclose - Q')  Q.
596 597
Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I _%I.
598
Hint Mode ElimInv + - ! - - - ! - : typeclass_instances.
Joseph Tassarotti's avatar
Joseph Tassarotti committed
599

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