Library iris.proofmode.classes

From stdpp Require Import namespaces.
From iris.bi Require Export bi.
From iris.proofmode Require Import base.
From iris.proofmode Require Export ident_name modalities.
From iris.prelude Require Import options.
Import bi.

Use this as precondition on "failing" instances of typeclasses that have pure preconditions (such as ElimModal), if you want a nice error to be shown when this instances is picked as part of some proof mode tactic.
Inductive pm_error (s : string) := .

Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
  from_assumption : □?p P Q.
Global Arguments FromAssumption {_} _ _%I _%I : simpl never.
Global Arguments from_assumption {_} _ _%I _%I {_}.
Global Hint Mode FromAssumption + + - - : typeclass_instances.

Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
  knownl_from_assumption :> FromAssumption p P Q.
Global Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
Global Arguments knownl_from_assumption {_} _ _%I _%I {_}.
Global Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.

Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
  knownr_from_assumption :> FromAssumption p P Q.
Global Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
Global Arguments knownr_from_assumption {_} _ _%I _%I {_}.
Global Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.

Class IntoPure {PROP : bi} (P : PROP) (φ : Prop) :=
  into_pure : P φ.
Global Arguments IntoPure {_} _%I _%type_scope : simpl never.
Global Arguments into_pure {_} _%I _%type_scope {_}.
Global Hint Mode IntoPure + ! - : typeclass_instances.

Class IntoPureT {PROP : bi} (P : PROP) (φ : Type) :=
  into_pureT : ψ : Prop, φ = ψ IntoPure P ψ.
Lemma into_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ IntoPureT P φ.
Proof. by φ. Qed.
Global Hint Extern 0 (IntoPureT _ _) ⇒
  notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.

FromPure a P φ is used when introducing a pure assertion. It is used by iPureIntro and the [%] specialization pattern.
The Boolean a specifies whether introduction of P needs emp in addition to φ. Concretely, for the iPureIntro tactic, this means it specifies whether the spatial context should be empty or not.
Note that the Boolean a is not needed for the (dual) IntoPure class, because there we can just ask that P is Affine.
Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
  from_pure : <affine>?a φ P.
Global Arguments FromPure {_} _ _%I _%type_scope : simpl never.
Global Arguments from_pure {_} _ _%I _%type_scope {_}.
Global 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 φ.
Proof. by φ. Qed.
Global Hint Extern 0 (FromPureT _ _ _) ⇒
  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.

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

Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
  into_persistent : <pers>?p P <pers> Q.
Global Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Global Arguments into_persistent {_} _ _%I _%I {_}.
Global Hint Mode IntoPersistent + + ! - : typeclass_instances.

The FromModal φ M sel P Q class is used by the iModIntro tactic to transform a goal P into a modality M and proposition Q, under additional pure assumptions φ.
The inputs are P and sel and the outputs are M and Q.
The input sel can be used to specify which modality to introduce in case there are multiple choices to turn P into a modality. For example, given ⎡|==> R, sel can be either |==> ?e or ?e , which turn it into an update modality or embedding, respectively. In case there is no need to specify the modality to introduce, sel should be an evar.
For modalities N that do not need to augment the proof mode environment, one can define an instance FromModal True modality_id (N P) P. Defining such an instance only imposes the proof obligation P N P. Examples of such modalities N are bupd, fupd, except_0, monPred_subjectively and bi_absorbingly.
Class FromModal {PROP1 PROP2 : bi} {A}
    (φ : Prop) (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
  from_modal : φ M Q P.
Global Arguments FromModal {_ _ _} _ _ _%I _%I _%I : simpl never.
Global Arguments from_modal {_ _ _} _ _ _ _%I _%I {_}.
Global Hint Mode FromModal - + - - - - ! - : typeclass_instances.

The FromAffinely P Q class is used to add an <affine> modality to the proposition Q.
The input is Q and the output is P.
Class FromAffinely {PROP : bi} (P Q : PROP) :=
  from_affinely : <affine> Q P.
Global Arguments FromAffinely {_} _%I _%I : simpl never.
Global Arguments from_affinely {_} _%I _%I {_}.
Global Hint Mode FromAffinely + - ! : typeclass_instances.

The IntoAbsorbingly P Q class is used to add an <absorb> modality to the proposition Q.
The input is Q and the output is P.
Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
  into_absorbingly : P <absorb> Q.
Global Arguments IntoAbsorbingly {_} _%I _%I.
Global Arguments into_absorbingly {_} _%I _%I {_}.
Global Hint Mode IntoAbsorbingly + - ! : 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.
Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
  into_wand : □?p R □?q P -∗ Q.
Global Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
Global Arguments into_wand {_} _ _ _%I _%I _%I {_}.
Global Hint Mode IntoWand + + + ! - - : typeclass_instances.

Class IntoWand' {PROP : bi} (p q : bool) (R P Q : PROP) :=
  into_wand' : IntoWand p q R P Q.
Global Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
Global Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
Global Hint Mode IntoWand' + + + ! - ! : typeclass_instances.

Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) P.
Global Arguments FromWand {_} _%I _%I _%I : simpl never.
Global Arguments from_wand {_} _%I _%I _%I {_}.
Global Hint Mode FromWand + ! - - : typeclass_instances.

Class FromImpl {PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1 Q2) P.
Global Arguments FromImpl {_} _%I _%I _%I : simpl never.
Global Arguments from_impl {_} _%I _%I _%I {_}.
Global Hint Mode FromImpl + ! - - : typeclass_instances.

Class FromSep {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 Q2 P.
Global Arguments FromSep {_} _%I _%I _%I : simpl never.
Global Arguments from_sep {_} _%I _%I _%I {_}.
Global Hint Mode FromSep + ! - - : typeclass_instances.
Global Hint Mode FromSep + - ! ! : typeclass_instances.
Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 Q2 P.
Global Arguments FromAnd {_} _%I _%I _%I : simpl never.
Global Arguments from_and {_} _%I _%I _%I {_}.
Global Hint Mode FromAnd + ! - - : typeclass_instances.
Global Hint Mode FromAnd + - ! ! : typeclass_instances.
The IntoAnd p P Q1 Q2 class is used to handle some [H1 H2] intro patterns:
  • IntoAnd true is used for such patterns in the intuitionistic context
  • IntoAnd false is used for such patterns where one of the two sides is discarded (e.g. [_ H]) or where the left-hand side is pure as in [% H] (via an IntoExist fallback).
The inputs are p P and the outputs are Q1 Q2.
Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
  into_and : □?p P □?p (Q1 Q2).
Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
Global Arguments into_and {_} _ _%I _%I _%I {_}.
Global Hint Mode IntoAnd + + ! - - : typeclass_instances.

The IntoSep P Q1 Q2 class is used to handle [H1 H2] intro patterns in the spatial context, except:
  • when one side is _, then IntoAnd is tried first (but IntoSep is used as fallback)
  • when the left-hand side is %, then IntoExist is used)
The input is P and the outputs are Q1 Q2.
Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
  into_sep : P Q1 Q2.
Global Arguments IntoSep {_} _%I _%I _%I : simpl never.
Global Arguments into_sep {_} _%I _%I _%I {_}.
Global Hint Mode IntoSep + ! - - : typeclass_instances.

Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 Q2 P.
Global Arguments FromOr {_} _%I _%I _%I : simpl never.
Global Arguments from_or {_} _%I _%I _%I {_}.
Global Hint Mode FromOr + ! - - : typeclass_instances.

Class IntoOr {PROP : bi} (P Q1 Q2 : PROP) := into_or : P Q1 Q2.
Global Arguments IntoOr {_} _%I _%I _%I : simpl never.
Global Arguments into_or {_} _%I _%I _%I {_}.
Global Hint Mode IntoOr + ! - - : typeclass_instances.

Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A PROP) :=
  from_exist : ( x, Φ x) P.
Global Arguments FromExist {_ _} _%I _%I : simpl never.
Global Arguments from_exist {_ _} _%I _%I {_}.
Global Hint Mode FromExist + - ! - : typeclass_instances.

Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name: ident_name) :=
  into_exist : P x, Φ x.
Global Arguments IntoExist {_ _} _%I _%I _ : simpl never.
Global Arguments into_exist {_ _} _%I _%I _ {_}.
Global Hint Mode IntoExist + - ! - - : typeclass_instances.

Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A PROP) :=
  into_forall : P x, Φ x.
Global Arguments IntoForall {_ _} _%I _%I : simpl never.
Global Arguments into_forall {_ _} _%I _%I {_}.
Global Hint Mode IntoForall + - ! - : typeclass_instances.

Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name : ident_name) :=
  from_forall : ( x, Φ x) P.
Global Arguments FromForall {_ _} _%I _%I _ : simpl never.
Global Arguments from_forall {_ _} _%I _%I _ {_}.
Global Hint Mode FromForall + - ! - - : typeclass_instances.

Class IsExcept0 {PROP : bi} (Q : PROP) := is_except_0 : Q Q.
Global Arguments IsExcept0 {_} _%I : simpl never.
Global Arguments is_except_0 {_} _%I {_}.
Global Hint Mode IsExcept0 + ! : typeclass_instances.

The ElimModal φ p p' P P' Q Q' class is used by the iMod tactic.
The inputs are p, P and Q, and the outputs are φ, p', P' and Q'.
The class is used to transform a hypothesis P into a hypothesis P', given a goal Q, which is simultaneously transformed into Q'. The Booleans p and p' indicate whether the original, respectively, updated hypothesis reside in the persistent context (iff true). The proposition φ can be used to express a side-condition that iMod will generate (if not True).
An example instance is:
ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
This instance expresses that to eliminate |={E1,E2}=> P the goal is transformed from |={E1,E3}=> Q into |={E2,E3}=> Q, and the resulting hypothesis is moved into the spatial context (regardless of where it was originally). A corresponding ElimModal instance for the Iris 1/2-style update modality, would have a side-condition φ on the masks.
Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
  elim_modal : φ □?p P (□?p' P' -∗ Q') Q.
Global Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
Global Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
Global Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.

Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
  add_modal : P (P' -∗ Q) Q.
Global Arguments AddModal {_} _%I _%I _%I : simpl never.
Global Arguments add_modal {_} _%I _%I _%I {_}.
Global Hint Mode AddModal + - ! ! : typeclass_instances.

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

We use the classes IsCons and IsApp to make sure that instances such as frame_big_sepL_cons and frame_big_sepL_app cannot be applied repeatedly often when having [∗ list] k x ?e, Φ k x with ?e an evar.
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.

Global Instance is_cons_cons {A} (x : A) (l : list A) : IsCons (x :: l) x l.
Proof. done. Qed.
Global Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.

Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R Q P.
Global Arguments Frame {_} _ _%I _%I _%I.
Global Arguments frame {_} _ _%I _%I _%I {_}.
Global Hint Mode Frame + + ! ! - : typeclass_instances.

Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
  maybe_frame : □?p R Q P.
Global Arguments MaybeFrame {_} _ _%I _%I _%I _.
Global Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
Global Hint Mode MaybeFrame + + ! - - - : typeclass_instances.

Global Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
  Frame p R P Q MaybeFrame p R P Q true.
Proof. done. Qed.

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

Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
  make_embed : P ⊣⊢ Q.
Global Arguments MakeEmbed {_ _ _} _%I _%I.
Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
  known_make_embed :> MakeEmbed P Q.
Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.

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

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

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

Class MakeAffinely {PROP : bi} (P Q : PROP) :=
  make_affinely : <affine> P ⊣⊢ Q.
Global Arguments MakeAffinely {_} _%I _%I.
Global Hint Mode MakeAffinely + - - : typeclass_instances.
Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
  known_make_affinely :> MakeAffinely P Q.
Global Arguments KnownMakeAffinely {_} _%I _%I.
Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.

Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
  make_intuitionistically : P ⊣⊢ Q.
Global Arguments MakeIntuitionistically {_} _%I _%I.
Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
  known_make_intuitionistically :> MakeIntuitionistically P Q.
Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.

Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
  make_absorbingly : <absorb> P ⊣⊢ Q.
Global Arguments MakeAbsorbingly {_} _%I _%I.
Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
  known_make_absorbingly :> MakeAbsorbingly P Q.
Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.

Class MakePersistently {PROP : bi} (P Q : PROP) :=
  make_persistently : <pers> P ⊣⊢ Q.
Global Arguments MakePersistently {_} _%I _%I.
Global Hint Mode MakePersistently + - - : typeclass_instances.
Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
  known_make_persistently :> MakePersistently P Q.
Global Arguments KnownMakePersistently {_} _%I _%I.
Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.

Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
  make_laterN : ▷^n P ⊣⊢ lP.
Global Arguments MakeLaterN {_} _%nat _%I _%I.
Global Hint Mode MakeLaterN + + - - : typeclass_instances.
Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
  known_make_laterN :> MakeLaterN n P lP.
Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.

Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
  make_except_0 : P ⊣⊢ Q.
Global Arguments MakeExcept0 {_} _%I _%I.
Global Hint Mode MakeExcept0 + - - : typeclass_instances.
Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
  known_make_except_0 :> MakeExcept0 P Q.
Global Arguments KnownMakeExcept0 {_} _%I _%I.
Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.

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

Class MaybeIntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
  maybe_into_laterN : P ▷^n Q.
Global Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
Global Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
Global Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.

Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
  into_laterN :> MaybeIntoLaterN only_head n P Q.
Global Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
Global Hint Mode IntoLaterN + + + ! - : typeclass_instances.

Global Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
  MaybeIntoLaterN only_head n P P | 1000.
Proof. apply laterN_intro. Qed.
Global Instance maybe_into_laterN_default_0 {PROP : bi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
Proof. apply _. Qed.

The class IntoEmbed P Q is used to transform hypotheses while introducing embeddings using iModIntro.
Input: the proposition P, output: the proposition Q so that P Q.
Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
  into_embed : P Q.
Global Arguments IntoEmbed {_ _ _} _%I _%I.
Global Arguments into_embed {_ _ _} _%I _%I {_}.
Global Hint Mode IntoEmbed + + + ! - : typeclass_instances.

Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
  as_emp_valid : φ P.
Global Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
  as_emp_valid_0 : AsEmpValid φ P.
Global Arguments AsEmpValid0 {_} _%type _%I.
Global Existing Instance as_emp_valid_0 | 0.

Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
  φ P.
Proof. by apply as_emp_valid. Qed.
Lemma as_emp_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
  ( P) φ.
Proof. by apply as_emp_valid. Qed.

Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Global Arguments IntoInv {_} _%I _.
Global Hint Mode IntoInv + ! - : typeclass_instances.

Accessors. This definition only exists for the purpose of the proof mode; a truly usable and general form would use telescopes and also allow binders for the closing view shift. γ is an option to make it easy for ElimAcc instances to recognize the emp case and make it look nicer.
Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP PROP)
           (α β : X PROP) ( : X option PROP) : PROP :=
  M1 ( x, α x (β x -∗ M2 (default emp ( x))))%I.

Class ElimAcc {PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP PROP)
      (α β : X PROP) ( : X option PROP)
      (Q : PROP) (Q' : X PROP) :=
  elim_acc : φ (( x, α x -∗ Q' x) -∗ accessor M1 M2 α β -∗ Q).
Global Arguments ElimAcc {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Global Arguments elim_acc {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Global Hint Mode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.

Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
      (M1 M2 : PROP PROP) (α β : X PROP) ( : X option PROP) :=
  into_acc : φ Pacc -∗ Pin -∗ accessor M1 M2 α β .
Global Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
Global Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.

Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
      (Pinv Pin : PROP) (Pout : X PROP) (mPclose : option (X PROP))
      (Q : PROP) (Q' : X PROP) :=
  elim_inv : φ Pinv Pin ( x, Pout x (default (λ _, emp) mPclose) x -∗ Q' x) Q.
Global Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Global Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Global Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.

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:
Global Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
  IntoPure P φ IntoPure (tc_opaque P) φ := id.
Global Instance from_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
  FromPure a P φ FromPure a (tc_opaque P) φ := id.
Global Instance from_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromWand P Q1 Q2 FromWand (tc_opaque P) Q1 Q2 := id.
Global 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.
Global Instance from_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromAnd P Q1 Q2 FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
Global Instance into_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
  IntoAnd p P Q1 Q2 IntoAnd p (tc_opaque P) Q1 Q2 := id.
Global Instance into_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  IntoSep P Q1 Q2 IntoSep (tc_opaque P) Q1 Q2 := id.
Global Instance from_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromOr P Q1 Q2 FromOr (tc_opaque P) Q1 Q2 := id.
Global Instance into_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  IntoOr P Q1 Q2 IntoOr (tc_opaque P) Q1 Q2 := id.
Global Instance from_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
  FromExist P Φ FromExist (tc_opaque P) Φ := id.
Global Instance into_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name: ident_name) :
  IntoExist P Φ name IntoExist (tc_opaque P) Φ name := id.
Global Instance from_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) (name : ident_name) :
  FromForall P Φ name FromForall (tc_opaque P) Φ name := id.
Global Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A PROP) :
  IntoForall P Φ IntoForall (tc_opaque P) Φ := id.
Global Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
    φ M (sel : A) (P : PROP2) (Q : PROP1) :
  FromModal φ M sel P Q FromModal φ M sel (tc_opaque P) Q := id.
Global Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
  ElimModal φ p p' P P' Q Q' ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
Global Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
  IntoInv P N IntoInv (tc_opaque P) N := id.
Global Instance elim_inv_tc_opaque {PROP : bi} {X} φ Pinv Pin Pout Pclose Q Q' :
  ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q'
  ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.