(* iris/proofmode/classes.v *)
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
FromPure a P φ → FromPureT a P φ
FromPure a P φ → FromPure a (tc_opaque P) φ := id
FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id
FromSep P Q1 Q2 → FromSep (tc_opaque P) Q1 Q2 | 102 := id
FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 := id
FromOr P Q1 Q2 → FromOr (tc_opaque P) Q1 Q2 := id
FromExist P Φ → FromExist (tc_opaque P) Φ := id
FromForall P Φ name → FromForall (tc_opaque P) Φ name := id
FromModal φ M sel P Q → FromModal φ M sel (tc_opaque P) Q := id

Inductive pm_error(s : string) := .

Class FromAssumption{PROP : bi} (p : bool) (P Q : PROP) :=
  from_assumption : □?p P ⊢ Q.

Global ArgumentsFromAssumption {_} _ _%_I _%_I : simpl never.

Global Argumentsfrom_assumption {_} _ _%_I _%_I {_}.

Global HintMode FromAssumption + + - - : typeclass_instances.

Class KnownLFromAssumption{PROP : bi} (p : bool) (P Q : PROP) :=
  #[global] knownl_from_assumption :: FromAssumption p P Q.

Global ArgumentsKnownLFromAssumption {_} _ _%_I _%_I : simpl never.

Global Argumentsknownl_from_assumption {_} _ _%_I _%_I {_}.

Global HintMode KnownLFromAssumption + + ! - : typeclass_instances.

Class KnownRFromAssumption{PROP : bi} (p : bool) (P Q : PROP) :=
  #[global] knownr_from_assumption :: FromAssumption p P Q.

Global ArgumentsKnownRFromAssumption {_} _ _%_I _%_I : simpl never.

Global Argumentsknownr_from_assumption {_} _ _%_I _%_I {_}.

Global HintMode KnownRFromAssumption + + - ! : typeclass_instances.

Class IntoPure{PROP : bi} (P : PROP) (φ : Prop) :=
  into_pure : P ⊢ ⌜φ⌝.

Global ArgumentsIntoPure {_} _%_I _%_type_scope : simpl never.

Global Argumentsinto_pure {_} _%_I _%_type_scope {_}.

Global HintMode IntoPure + ! - : typeclass_instances.

Global Instanceinto_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. *)

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 exists φ. Qed.

Global HintExtern 0 (IntoPureT _ _) =>
  notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.

Class FromPure{PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
  from_pure : <affine>?a ⌜φ⌝ ⊢ P.

Global ArgumentsFromPure {_} _ _%_I _%_type_scope : simpl never.

Global Argumentsfrom_pure {_} _ _%_I _%_type_scope {_}.

Global HintMode 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 exists φ. Qed.

Global HintExtern 0 (FromPureT _ _ _) =>
  notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.

Class IntoInternalEq`{!Sbi PROP} {A : ofe} (P : PROP) (x y : A) :=
  into_internal_eq : P ⊢ x ≡ y.

Global ArgumentsIntoInternalEq {_ _ _} _%_I _%_type_scope _%_type_scope : simpl never.

Global Argumentsinto_internal_eq {_ _ _} _%_I _%_type_scope _%_type_scope {_}.

Global HintMode IntoInternalEq + - - ! - - : typeclass_instances.

Class IntoPersistent{PROP : bi} (p : bool) (P Q : PROP) :=
  into_persistent : <pers>?p P ⊢ <pers> Q.

Global ArgumentsIntoPersistent {_} _ _%_I _%_I : simpl never.

Global Argumentsinto_persistent {_} _ _%_I _%_I {_}.

Global HintMode IntoPersistent + + ! - : typeclass_instances.

Class FromModal{PROP1 PROP2 : bi} {A}
    (φ : Prop) (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
  from_modal : φ → M Q ⊢ P.

Global ArgumentsFromModal {_ _ _} _ _ _%_I _%_I _%_I : simpl never.

Global Argumentsfrom_modal {_ _ _} _ _ _ _%_I _%_I {_}.

Global HintMode FromModal - + - - - - ! - : typeclass_instances.

Class FromAffinely{PROP : bi} (P Q : PROP) :=
  from_affinely : <affine> Q ⊢ P.

Global ArgumentsFromAffinely {_} _%_I _%_I : simpl never.

Global Argumentsfrom_affinely {_} _%_I _%_I {_}.

Global HintMode FromAffinely + - ! : typeclass_instances.

Class IntoAbsorbingly{PROP : bi} (P Q : PROP) :=
  into_absorbingly : P ⊢ <absorb> Q.

Global ArgumentsIntoAbsorbingly {_} _%_I _%_I.

Global Argumentsinto_absorbingly {_} _%_I _%_I {_}.

Global HintMode IntoAbsorbingly + - ! : typeclass_instances.

Class IntoWand{PROP : bi} (p q : bool) (R P Q : PROP) :=
  into_wand : □?p R ⊢ □?q P -∗ Q.

Global ArgumentsIntoWand {_} _ _ _%_I _%_I _%_I : simpl never.

Global Argumentsinto_wand {_} _ _ _%_I _%_I _%_I {_}.

Global HintMode IntoWand + + + ! - - : typeclass_instances.

Class IntoWand'{PROP : bi} (p q : bool) (R P Q : PROP) :=
  into_wand' : IntoWand p q R P Q.

Global ArgumentsIntoWand' {_} _ _ _%_I _%_I _%_I : simpl never.

Global HintMode IntoWand' + + + ! ! - : typeclass_instances.

Global HintMode IntoWand' + + + ! - ! : typeclass_instances.

Class FromWand{PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.

Global ArgumentsFromWand {_} _%_I _%_I _%_I : simpl never.

Global Argumentsfrom_wand {_} _%_I _%_I _%_I {_}.

Global HintMode FromWand + ! - - : typeclass_instances.

Class FromImpl{PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.

Global ArgumentsFromImpl {_} _%_I _%_I _%_I : simpl never.

Global Argumentsfrom_impl {_} _%_I _%_I _%_I {_}.

Global HintMode FromImpl + ! - - : typeclass_instances.

Class FromSep{PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.

Global ArgumentsFromSep {_} _%_I _%_I _%_I : simpl never.

Global Argumentsfrom_sep {_} _%_I _%_I _%_I {_}.

Global HintMode FromSep + ! - - : typeclass_instances.

Class FromAnd{PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.

Global ArgumentsFromAnd {_} _%_I _%_I _%_I : simpl never.

Global Argumentsfrom_and {_} _%_I _%_I _%_I {_}.

Global HintMode FromAnd + ! - - : typeclass_instances.

Class IntoAnd{PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
  into_and : □?p P ⊢ □?p (Q1 ∧ Q2).

Global ArgumentsIntoAnd {_} _ _%_I _%_I _%_I : simpl never.

Global Argumentsinto_and {_} _ _%_I _%_I _%_I {_}.

Global HintMode IntoAnd + + ! - - : typeclass_instances.

Class IntoSep{PROP : bi} (P Q1 Q2 : PROP) :=
  into_sep : P ⊢ Q1 ∗ Q2.

Global ArgumentsIntoSep {_} _%_I _%_I _%_I : simpl never.

Global Argumentsinto_sep {_} _%_I _%_I _%_I {_}.

Global HintMode IntoSep + ! - - : typeclass_instances.

Class FromOr{PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.

Global ArgumentsFromOr {_} _%_I _%_I _%_I : simpl never.

Global Argumentsfrom_or {_} _%_I _%_I _%_I {_}.

Global HintMode FromOr + ! - - : typeclass_instances.

Class IntoOr{PROP : bi} (P Q1 Q2 : PROP) := into_or : P ⊢ Q1 ∨ Q2.

Global ArgumentsIntoOr {_} _%_I _%_I _%_I : simpl never.

Global Argumentsinto_or {_} _%_I _%_I _%_I {_}.

Global HintMode IntoOr + ! - - : typeclass_instances.

Class FromExist{PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
  from_exist : (∃ x, Φ x) ⊢ P.

Global ArgumentsFromExist {_ _} _%_I _%_I : simpl never.

Global Argumentsfrom_exist {_ _} _%_I _%_I {_}.

Global HintMode FromExist + - ! - : typeclass_instances.

Class IntoExist{PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
  into_exist : P ⊢ ∃ x, Φ x.

Global ArgumentsIntoExist {_ _} _%_I _%_I _ : simpl never.

Global Argumentsinto_exist {_ _} _%_I _%_I _ {_}.

Global HintMode IntoExist + - ! - - : typeclass_instances.

Class IntoForall{PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
  into_forall : P ⊢ ∀ x, Φ x.

Global ArgumentsIntoForall {_ _} _%_I _%_I : simpl never.

Global Argumentsinto_forall {_ _} _%_I _%_I {_}.

Global HintMode IntoForall + - ! - : typeclass_instances.

Class FromForall{PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
  from_forall : (∀ x, Φ x) ⊢ P.

Global ArgumentsFromForall {_ _} _%_I _%_I _ : simpl never.

Global Argumentsfrom_forall {_ _} _%_I _%_I _ {_}.

Global HintMode FromForall + - ! - - : typeclass_instances.

Class IsExcept0{PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.

Global ArgumentsIsExcept0 {_} _%_I : simpl never.

Global Argumentsis_except_0 {_} _%_I {_}.

Global HintMode IsExcept0 + ! : typeclass_instances.

Class CombineSepAs{PROP : bi} (P Q R : PROP) := combine_sep_as : P ∗ Q ⊢ R.

Global ArgumentsCombineSepAs {_} _%_I _%_I _%_I : simpl never.

Global Argumentscombine_sep_as {_} _%_I _%_I _%_I {_}.

Global HintMode CombineSepAs + ! ! - : typeclass_instances.

Inductive progress_indicator:= MadeProgress | NoProgress.

Class MaybeCombineSepAs{PROP : bi}
    (P Q R : PROP) (progress : progress_indicator) :=
  maybe_combine_sep_as : P ∗ Q ⊢ R.

Global ArgumentsMaybeCombineSepAs {_} _%_I _%_I _%_I _ : simpl never.

Global Argumentsmaybe_combine_sep_as {_} _%_I _%_I _%_I _ {_}.

Global HintMode MaybeCombineSepAs + ! ! - - : typeclass_instances.

Global Instancemaybe_combine_sep_as_combine_sep_as {PROP : bi} (R P Q : PROP) :
  CombineSepAs P Q R → MaybeCombineSepAs P Q R MadeProgress | 20.
Proof. done. Qed.

Global Instancemaybe_combine_sep_as_default {PROP : bi} (P Q : PROP) :
  MaybeCombineSepAs P Q (P ∗ Q) NoProgress | 100.
Proof. intros. by rewrite /MaybeCombineSepAs. Qed.

Class CombineSepGives{PROP : bi} (P Q R : PROP) :=
  combine_sep_gives : P ∗ Q ⊢ <pers> R.

Global ArgumentsCombineSepGives {_} _%_I _%_I _%_I : simpl never.

Global Argumentscombine_sep_gives {_} _%_I _%_I _%_I {_}.

Global HintMode CombineSepGives + ! ! - : typeclass_instances.

Class ElimModal{PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
  elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.

Global ArgumentsElimModal {_} _ _ _ _%_I _%_I _%_I _%_I : simpl never.

Global Argumentselim_modal {_} _ _ _ _%_I _%_I _%_I _%_I {_}.

Global HintMode ElimModal + - ! - ! - ! - : typeclass_instances.

Class AddModal{PROP : bi} (P P' : PROP) (Q : PROP) :=
  add_modal : P ∗ (P' -∗ Q) ⊢ Q.

Global ArgumentsAddModal {_} _%_I _%_I _%_I : simpl never.

Global Argumentsadd_modal {_} _%_I _%_I _%_I {_}.

Global HintMode AddModal + - ! ! : typeclass_instances.

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

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 HintMode IsCons + ! - - : typeclass_instances.

Global HintMode IsApp + ! - - : typeclass_instances.

Global Instanceis_cons_cons {A} (x : A) (l : list A) : IsCons (x :: l) x l.
Proof. done. Qed.

Global Instanceis_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
Proof. done. Qed.

Class IsDisjUnion`{DisjUnion A} (X X1 X2 : A) := is_disj_union : X = X1 ⊎ X2.

Global HintMode IsDisjUnion + + ! - - : typeclass_instances.

Global Instanceis_disj_union_disj_union `{DisjUnion A} (X1 X2 : A) :
  IsDisjUnion (X1 ⊎ X2) X1 X2.
Proof. done. Qed.

Class Frame{PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.

Global ArgumentsFrame {_} _ _%_I _%_I _%_I.

Global Argumentsframe {_} _ _%_I _%_I _%_I {_}.

Global HintMode Frame + + ! ! - : typeclass_instances.

Class MaybeFrame'{PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
  maybe_frame : □?p R ∗ Q ⊢ P.

Global ArgumentsMaybeFrame' {_} _ _%_I _%_I _%_I _.

Global Argumentsmaybe_frame {_} _ _%_I _%_I _%_I _ {_}.

Global HintMode MaybeFrame' + + ! - - - : typeclass_instances.

Global Instancemaybe_frame_frame {PROP : bi} p (R P Q : PROP) :
  Frame p R P Q → MaybeFrame' p R P Q true.
Proof. done. Qed.

Global Instancemaybe_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 Instancemaybe_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.

Notation MaybeFramep R P Q progress := (TCNoBackTrack (MaybeFrame' p R P Q progress)).

Class FrameInstantiateExistDisabled: Prop := frame_instantiate_exist_disabled {}.

Notation FrameInstantiateExistEnabled:= (TCUnless FrameInstantiateExistDisabled).

Class IntoExcept0{PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.

Global ArgumentsIntoExcept0 {_} _%_I _%_I : simpl never.

Global Argumentsinto_except_0 {_} _%_I _%_I {_}.

Global HintMode IntoExcept0 + ! - : typeclass_instances.

Global HintMode IntoExcept0 + - ! : typeclass_instances.

Lemma test_iFrame_later_1P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
Proof. iIntros "H". iFrame "H". Qed.
>>
*)

Class MaybeIntoLaterN{PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
  maybe_into_laterN : P ⊢ ▷^n Q.

Global ArgumentsMaybeIntoLaterN {_} _ _%_nat_scope _%_I _%_I.

Global Argumentsmaybe_into_laterN {_} _ _%_nat_scope _%_I _%_I {_}.

Global HintMode MaybeIntoLaterN + + + - - : typeclass_instances.

Class IntoLaterN{PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
  #[global] into_laterN :: MaybeIntoLaterN only_head n P Q.

Global ArgumentsIntoLaterN {_} _ _%_nat_scope _%_I _%_I.

Global HintMode IntoLaterN + + + ! - : typeclass_instances.

Global Instancemaybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
  MaybeIntoLaterN only_head n P P | 1000.
Proof. apply laterN_intro. Qed.

Global Instancemaybe_into_laterN_default_0 {PROP : bi} only_head (P : PROP) :
  MaybeIntoLaterN only_head 0 P P | 0.
Proof. apply _. Qed.

Class IntoEmbed{PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
  into_embed : P ⊢ ⎡Q⎤.

Global ArgumentsIntoEmbed {_ _ _} _%_I _%_I.

Global Argumentsinto_embed {_ _ _} _%_I _%_I {_}.

Global HintMode IntoEmbed + + + ! -  : typeclass_instances.

Inductive as_emp_valid_direction:=
  | DirectionIntoEmpValid
  | DirectionFromEmpValid.

Class AsEmpValid{PROP : bi} (d : as_emp_valid_direction) (φ : Prop) (P : PROP) :=
  as_emp_valid : (d = DirectionIntoEmpValid → φ → ⊢ P) ∧
                 (d = DirectionFromEmpValid → (⊢ P) → φ).

Global ArgumentsAsEmpValid {_} _ _%_type _%_I.

Class AsEmpValid0{PROP : bi} (d : as_emp_valid_direction) (φ : Prop) (P : PROP) :=
  as_emp_valid_0 : AsEmpValid d φ P.

Global ArgumentsAsEmpValid0 {_} _ _%_type _%_I.

Global ExistingInstance as_emp_valid_0 | 0.

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

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

Class IntoInv{PROP : bi} (P: PROP) (N: namespace).

Global ArgumentsIntoInv {_} _%_I _.

Global HintMode IntoInv + ! - : typeclass_instances.

Definition accessor{PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
           (α β : X → PROP) (mγ : X → option PROP) : PROP :=
  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.

Class ElimAcc{PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
      (α β : X → PROP) (mγ : X → option PROP)
      (Q : PROP) (Q' : X → PROP) :=
  elim_acc : φ → ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).

Global ArgumentsElimAcc {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I : simpl never.

Global Argumentselim_acc {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I {_}.

Global HintMode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.

Class IntoAcc{PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
      (M1 M2 : PROP → PROP) (α β : X → PROP) (mγ : X → option PROP) :=
  into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ.

Global ArgumentsIntoAcc {_} {_} _%_I _ _%_I _%_I _%_I _%_I _%_I _%_I : simpl never.

Global Argumentsinto_acc {_} {_} _%_I _ _%_I _%_I _%_I _%_I _%_I _%_I {_} : simpl never.

Global HintMode 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 ArgumentsElimInv {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I : simpl never.

Global Argumentselim_inv {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I {_}.

Global HintMode ElimInv + - - ! - - ! ! - : typeclass_instances.

Global Instanceinto_pure_tc_opaque {PROP : bi} (P : PROP) φ :
  IntoPure P φ → IntoPure (tc_opaque P) φ := id.

Global Instancefrom_pure_tc_opaque {PROP : bi} (a : bool) (P : PROP) φ :
  FromPure a P φ → FromPure a (tc_opaque P) φ := id.

Global Instancefrom_wand_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.

Global Instanceinto_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 Instancefrom_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromSep P Q1 Q2 → FromSep (tc_opaque P) Q1 Q2 | 102 := id.

Global Instancefrom_and_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 := id.

Global Instanceinto_and_tc_opaque {PROP : bi} p (P Q1 Q2 : PROP) :
  IntoAnd p P Q1 Q2 → IntoAnd p (tc_opaque P) Q1 Q2 := id.

Global Instanceinto_sep_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  IntoSep P Q1 Q2 → IntoSep (tc_opaque P) Q1 Q2 := id.

Global Instancefrom_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  FromOr P Q1 Q2 → FromOr (tc_opaque P) Q1 Q2 := id.

Global Instanceinto_or_tc_opaque {PROP : bi} (P Q1 Q2 : PROP) :
  IntoOr P Q1 Q2 → IntoOr (tc_opaque P) Q1 Q2 := id.

Global Instancefrom_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
  FromExist P Φ → FromExist (tc_opaque P) Φ := id.

Global Instanceinto_exist_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
  IntoExist P Φ name → IntoExist (tc_opaque P) Φ name := id.

Global Instancefrom_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
  FromForall P Φ name → FromForall (tc_opaque P) Φ name := id.

Global Instanceinto_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.

Global Instancefrom_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 Instanceelim_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 Instanceinto_inv_tc_opaque {PROP : bi} (P : PROP) N :
  IntoInv P N → IntoInv (tc_opaque P) N := id.

Global Instanceelim_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.