phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/ltac_tactics.v *)
(* [pat0] is the unparsed pattern, and is only used in error messages *)
Ltac _iDestructHypGo Hz pat0 pat
:=
  lazymatch pat with
  | IFresh =>
     lazymatch Hz with
     | IAnon _ => idtac
     | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
     end
  | IDrop => _iClearHyp Hz
  | IFrame => iFrame Hz
  | IIdent Hz => idtac
  | IIdent ?y => iRename Hz into y
  | IList [[]] => iExFalso; iExact Hz

  (* conjunctive patterns like [H1 H2] *)
  | IList [[?pat1; IDrop]] =>
     let x := _ident_for_pat_default pat1 Hz in
     _iAndDestructChoice Hz Left x;
     _iDestructHypGo x pat0 pat1
  | IList [[IDrop; ?pat2]] =>
     let x := _ident_for_pat_default pat2 Hz in
     _iAndDestructChoice Hz Right x;
     _iDestructHypGo x pat0 pat2
  (* [% ...] is always interpreted as an existential; there are [IntoExist]
  instances in place to handle conjunctions with a pure left-hand side this way
  as well. *)
  | IList [[IPure IGallinaAnon; ?pat2]] =>
     let x := _ident_for_pat_default pat2 Hz in
     _iExistDestruct Hz as ? x; _iDestructHypGo x pat0 pat2
  | IList [[IPure (IGallinaNamed ?s); ?pat2]] =>
     let x := fresh in
     let y := _ident_for_pat_default pat2 Hz in
     _iExistDestruct Hz as x y;
     rename_by_string x s;
     _iDestructHypGo y pat0 pat2
  | IList [[?pat1; ?pat2]] =>
     (* We have to take care of not using the same name for the two hypotheses:
        [_ident_for_pat_default] will thus only reuse [Hz] (which could in principle
        clash with a name from [pat2]) if it is an anonymous name. *)
     let x1 := _ident_for_pat_default pat1 Hz in
     let x2 := _ident_for_pat pat2 in
     _iAndDestruct Hz x1 x2;
     _iDestructHypGo x1 pat0 pat1; _iDestructHypGo x2 pat0 pat2
  | IList [_ :: _ :: _] => fail "iDestruct:" pat0 "has too many conjuncts"
  | IList [[_]] => fail "iDestruct:" pat0 "has just a single conjunct"

  (* disjunctive patterns like [H1|H2] *)
  | IList [[?pat1];[?pat2]] =>
     let x1 := _ident_for_pat_default pat1 Hz in
     let x2 := _ident_for_pat_default pat2 Hz in
     iOrDestruct Hz as x1 x2;
     [_iDestructHypGo x1 pat0 pat1|_iDestructHypGo x2 pat0 pat2]
  (* this matches a list of three or more disjunctions [H1|H2|H3] *)
  | IList (_ :: _ :: _ :: _) => fail "iDestruct:" pat0 "has too many disjuncts"
  (* the above patterns don't match [H1 H2|H3] *)
  | IList [_;_] => fail "iDestruct: in" pat0 "a disjunct has multiple patterns"

  | IPure IGallinaAnon => iPure Hz as ?
  | IPure (IGallinaNamed ?s) =>
     let x := fresh in
     iPure Hz as x;
     rename_by_string x s
  | IRewrite Right => iPure Hz as ->
  | IRewrite Left => iPure Hz as <-
  | IIntuitionistic ?pat =>
    let x := _ident_for_pat_default pat Hz in
    _iIntuitionistic Hz x; _iDestructHypGo x pat0 pat
  | ISpatial ?pat =>
    let x := _ident_for_pat_default pat Hz in
    _iSpatial Hz x; _iDestructHypGo x pat0 pat
  | IModalElim ?pat =>
    let x := _ident_for_pat_default pat Hz in
    iModCore Hz as x; _iDestructHypGo x pat0 pat
  | _ => fail "iDestruct:" pat0 "is not supported due to" pat
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iDestructHypFindPat Hgo pat found pats
:=
  lazymatch pats with
  | [] =>
    lazymatch found with
    | true => pm_prettify (* post-tactic prettification *)
    | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
    end
  | ISimpl :: ?pats => simpl; _iDestructHypFindPat Hgo pat found pats
  | IClear ?H :: ?pats => iClear H; _iDestructHypFindPat Hgo pat found pats
  | IClearFrame ?H :: ?pats => iFrame H; _iDestructHypFindPat Hgo pat found pats
  | ?pat1 :: ?pats =>
     lazymatch found with
     | false => _iDestructHypGo Hgo pat pat1; _iDestructHypFindPat Hgo pat true pats
     | true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
     end
  end.
(* iris/proofmode/ltac_tactics.v *)
(* This is the core implementation of [iDestruct]. *)
Ltac _iDestructHyp0 H pat
:=
  let pats := intro_pat.parse pat in
  _iDestructHypFindPat H pat false pats.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iDestructHyp H xs pat
:=
  ltac1_list_iter ltac:(fun x => _iExistDestruct H as x H) xs;
  _iDestructHyp0 H pat.
(* iris/proofmode/ltac_tactics.v *)
(* * Introduction tactic *)
Ltac _iIntros_go pats startproof
:=
  lazymatch pats with
  | [] =>
    lazymatch startproof with
    | true => iStartProof
    | false => idtac
    end
  (* Optimizations to avoid generating fresh names *)
  | IPure (IGallinaNamed ?s) :: ?pats =>
     let i := fresh in
     _iIntro (i);
     rename_by_string i s;
     _iIntros_go pats startproof
  | IPure IGallinaAnon :: ?pats => _iIntro (?); _iIntros_go pats startproof
  | IIntuitionistic (IIdent ?H) :: ?pats => _iIntroPersistent H; _iIntros_go pats false
  | IDrop :: ?pats => _iIntroDrop; _iIntros_go pats startproof
  | IIdent ?H :: ?pats => _iIntroSpatial H; _iIntros_go pats startproof
  (* Introduction patterns that can only occur at the top-level *)
  | IPureIntro :: ?pats => iPureIntro; _iIntros_go pats false
  | IModalIntro :: ?pats => iModIntro; _iIntros_go pats false
  | IForall :: ?pats => repeat _iIntroForall; _iIntros_go pats startproof
  | IAll :: ?pats => repeat (_iIntroForall || _iIntro); _iIntros_go pats startproof
  (* Clearing and simplifying introduction patterns *)
  | ISimpl :: ?pats => simpl; _iIntros_go pats startproof
  | IClear ?H :: ?pats => iClear H; _iIntros_go pats false
  | IClearFrame ?H :: ?pats => iFrame H; _iIntros_go pats false
  | IDone :: ?pats => try done; _iIntros_go pats startproof
  (* Introduction + destruct *)
  | IIntuitionistic ?pat :: ?pats =>
     let H := iFresh in _iIntroPersistent H; iDestructHyp H as pat; _iIntros_go pats false
  | ?pat :: ?pats =>
     let H := iFresh in _iIntroSpatial H; iDestructHyp H as pat; _iIntros_go pats false
  end.
(* iris/proofmode/ltac_tactics.v *)
(* This is the core implementation of [iIntros]. *)
Ltac _iIntros0 pat
:=
  let pats := intro_pat.parse pat in
  (* HACK to avoid calling [iStartProof] on side-conditions opened by [iIntros (?%lemma)]. *)
  lazymatch pats with
  | [] => idtac
  | _ => _iIntros_go pats true
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iIntros xs pat
:=
  ltac1_list_iter ltac:(fun x => _iIntro (x)) xs;
  _iIntros0 pat.
(* iris/proofmode/ltac_tactics.v *)
(* Used for generalization in [iInduction] and [iLöb] *)
Ltac _iRevertIntros_go Hs tac
:=
  lazymatch Hs with
  | [] => tac ()
  | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
  | ESelIdent ?p ?H :: ?Hs =>
    iRevertHyp H; _iRevertIntros_go Hs tac; _iIntroMaybePersistent H p
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iRevertIntros0 Hs tac
:=
  try iStartProof;
  let Hs := iElaborateSelPat Hs in
  _iRevertIntros_go Hs tac.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iRevertIntros xs Hs tac
:=
  _iRevertIntros0 Hs ltac:(fun _ => _iRevert xs ""; tac (); _iIntros xs "").
(* iris/proofmode/ltac_tactics.v *)
Ltac _iDestruct0 lem pat
:=
  iDestructCore lem as pat (fun H => iDestructHyp H as pat).
(* iris/proofmode/ltac_tactics.v *)
Ltac _iDestruct lem xs pat
:=
  iDestructCore lem as pat (fun H => _iDestructHyp H xs pat).
(* iris/proofmode/ltac_tactics.v *)
Ltac iHypsContaining x
:=
  let rec go Γ x Hs :=
    lazymatch Γ with
    | Enil => constr:(Hs)
    | Esnoc ?Γ ?H ?Q =>
       match Q with
       | context [x] => go Γ x (H :: Hs)
       | _ => go Γ x Hs
       end
     end in
  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _ _) _ => Γp end in
  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs _) _ => Γs end in
  let Hs := go Γp x (@nil ident) in go Γs x Hs.
(* iris/proofmode/ltac_tactics.v *)
Ltac _iInduction x xs Hs tac IH
:=
  (* FIXME: We should be able to do this in a more sane way, by concatenating
  the spec patterns instead of calling [iRevertIntros] multiple times. *)
  _iRevertIntros0 Hs ltac:(fun _ =>
    _iRevertIntros0 "∗" ltac:(fun _ =>
      let Hsx := iHypsContaining x in
      _iRevertIntros xs Hsx ltac:(fun _ =>
        iInductionCore tac as IH
      )
    )
  ).
(* iris/proofmode/ltac_tactics.v *)
Ltac _iInduction0 x Hs tac IH
:=
  with_ltac1_nil ltac:(fun xs => _iInduction x xs Hs tac IH).
(* iris/proofmode/ltac_tactics.v *)
Ltac _iLöb xs Hs IH
:=
  (* FIXME: We should be able to do this in a more sane way, by concatenating
  the spec patterns instead of calling [iRevertIntros] multiple times. *)
  _iRevertIntros0 Hs ltac:(fun _ =>
    _iRevertIntros xs "∗" ltac:(fun _ =>
      iLöbCore as IH
    )
  ).
(* iris/proofmode/ltac_tactics.v *)
Ltac _iLöb0 Hs IH
:=
  with_ltac1_nil ltac:(fun xs => _iLöb xs Hs IH).
(* iris/proofmode/ltac_tactics.v *)
(* * Rewrite *)
Ltac iRewriteFindPred
:=
  match goal with
  | |- _ ⊣⊢ ?Φ ?x =>
     generalize x;
     match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac iSimplifyEq
:= repeat (
  iMatchHyp (fun H P => match P with ⌜_ = _⌝%I => iDestruct H as %? end)
  || simplify_eq/=).
(* iris/proofmode/ltac_tactics.v *)
Ltac _iDestructAccAndHyp0 pat x H
:=
  lazymatch type of x with
  | unit => destruct x as []; _iDestructHyp0 H pat
  | _ => fail "Missing intro pattern for accessor variable"
  end.
(* iris/proofmode/ltac_tactics.v *)
(* [_iDestructAccAndHyp xs pat x H] expects [x] to be a variable in the context.
Then it behaves as follows:
- If [x] has type [unit], it destructs [x] and continues as
  [_iDestructHyp H xs pat]. That is, it is basically as if [x] did not exist.
- Otherwise, [xs] must be a non-empty list of patterns, and the first pattern is
  applied to [x]. Then we continue as [_iDestructHyp H (tail xs) pat].
  Basically it is as if "H" (the hypothesis being destructed) actually was
  [∃ x, H], so that the first pattern in the [xs] destructs this existential. *)
Ltac _iDestructAccAndHyp xs pat x H
:=
  let go := ltac2:(tac xs |-
    match of_ltac1_list xs with
    | [] =>
      Control.throw_invalid_argument "iDestructAccAndHyp: List should be non-empty"
    | x1 :: xs' =>
      ltac1:(x1 |- intros x1) x1;
      ltac1:(tac xs' |- tac xs') tac (Ltac1.of_list xs')
    end) in
  lazymatch type of x with
  | unit => destruct x as []; _iDestructHyp H xs pat
  | _ => revert x; go ltac:(fun xs' => _iDestructHyp H xs' pat) xs
  end.
(* iris/proofmode/modalities.v *)
(* The `iModIntro` tactic is not tied the Iris modalities, but can be
instantiated with a variety of modalities.

For the purpose of MoSeL, a modality is a mapping of propositions
`M : PROP1 → PROP2` (where `PROP1` and `PROP2` are BI-algebras, although usually
it is the same algebra) that is monotone and distributes over separating
conjunction. Specifically, the following rules have to be satisfied:

      P ⊢ Q        emp ⊢ M emp
    ----------
    M P ⊢ M Q      M P ∗ M Q ⊢ M (P ∗ Q)

Together those conditions allow one to introduce the modality in the
goal, while stripping away the modalities in the context.

Additionally, upon introducing a modality one can perform a number of
associated actions on the intuitionistic and spatial contexts.
Such an action can be one of the following:

- 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).
- 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.
- Introduction will clear the context.
- Introduction will keep the context as-is.

Formally, these actions correspond to the inductive type [modality_action].
For each of those actions you have to prove that the transformation is valid.

To instantiate the modality you have to define: 1) a mixin `modality_mixin`,
2) a record `modality`, 3) a `FromModal` type class instance from `classes.v`.

For examples consult `modality_id` at the end of this file, or the instances
in the `modality_instances.v` file.

Note that in MoSeL modalities can map the propositions between two different
BI-algebras. Most of the modalities in Iris operate on the same type of
assertions. For example, the <affine> modality can potentially maps propositions
of an arbitrary BI-algebra into the sub-BI-algebra of affine propositions, but
it is implemented as an endomapping. On the other hand, the embedding modality
⎡-⎤ is a mapping between propositions of different BI-algebras. *)
Inductive modality_action (PROP1 : bi) : bi → Type
:=
  | MIEnvIsEmpty {PROP2 : bi} : modality_action PROP1 PROP2
  | MIEnvForall (C : PROP1 → Prop) : modality_action PROP1 PROP1
  | MIEnvTransform {PROP2 : bi} (C : PROP2 → PROP1 → Prop) : modality_action PROP1 PROP2
  | MIEnvClear {PROP2} : modality_action PROP1 PROP2
  | MIEnvId : modality_action PROP1 PROP1.
(* iris/proofmode/modalities.v *)
Notation MIEnvFilter C
:= (MIEnvTransform (TCDiag C)).
(* iris/proofmode/modalities.v *)
Definition modality_intuitionistic_action_spec {PROP1 PROP2}
    (s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop
:=
  match s with
  | MIEnvIsEmpty => λ M, True
  | MIEnvForall C => λ M,
     (∀ P, C P → □ P ⊢ M (□ P)) ∧
     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
  | MIEnvTransform C => λ M,
     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) ∧
     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q))
  | MIEnvClear => λ M, True
  | MIEnvId => λ M, ∀ P, □ P ⊢ M (□ P)
  end.
(* iris/proofmode/modalities.v *)
Definition modality_spatial_action_spec {PROP1 PROP2}
    (s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop
:=
  match s with
  | MIEnvIsEmpty => λ M, True
  | MIEnvForall C => λ M, ∀ P, C P → P ⊢ M P
  | MIEnvTransform C => λ M, ∀ P Q, C P Q → P ⊢ M Q
  | MIEnvClear => λ M, ∀ P, Absorbing (M P)
  | MIEnvId => λ M, ∀ P, P ⊢ M P
  end.
(* iris/proofmode/modalities.v *)
(* 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 {PROP1 PROP2 : bi} (M : PROP1 → PROP2)
    (iaction saction : modality_action PROP1 PROP2)
:= {
  modality_mixin_intuitionistic : modality_intuitionistic_action_spec iaction M;
  modality_mixin_spatial : modality_spatial_action_spec saction M;
  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)
}.
(* iris/proofmode/modalities.v *)
Record modality (PROP1 PROP2 : bi)
:= Modality {
  modality_car :> PROP1 → PROP2;
  modality_intuitionistic_action : modality_action PROP1 PROP2;
  modality_spatial_action : modality_action PROP1 PROP2;
  modality_mixin_of :
    modality_mixin modality_car modality_intuitionistic_action modality_spatial_action
}.
(* iris/proofmode/modalities.v *)
Lemma modality_intuitionistic_transform C P Q :
    modality_intuitionistic_action M = MIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_and_transform C P Q :
    modality_intuitionistic_action M = MIEnvTransform C → M P ∧ M Q ⊢ M (P ∧ Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_spatial_transform C P Q :
    modality_spatial_action M = MIEnvTransform C → C P Q → P ⊢ M Q.
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_spatial_clear P :
    modality_spatial_action M = MIEnvClear → Absorbing (M P).
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_emp : emp ⊢ M emp.
Proof. eapply modality_mixin_emp, modality_mixin_of. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
Proof. eapply modality_mixin_mono, modality_mixin_of. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
Proof. eapply modality_mixin_sep, modality_mixin_of. Qed.
(* iris/proofmode/modalities.v *)
Instance modality_mono' : Proper ((⊢) ==> (⊢)) M.
Proof. intros P Q. apply modality_mono. Qed.
(* iris/proofmode/modalities.v *)
Instance modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
Proof. intros P Q. apply modality_mono. Qed.
(* iris/proofmode/modalities.v *)
Instance modality_proper : Proper ((≡) ==> (≡)) M.
Proof. intros P Q. rewrite !equiv_entails=> -[??]; eauto using modality_mono. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_intuitionistic_forall C P :
    modality_intuitionistic_action M = MIEnvForall C → C P → □ P ⊢ M (□ P).
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_and_forall C P Q :
    modality_intuitionistic_action M = MIEnvForall C → M P ∧ M Q ⊢ M (P ∧ Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_intuitionistic_id P :
    modality_intuitionistic_action M = MIEnvId → □ P ⊢ M (□ P).
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_spatial_forall C P :
    modality_spatial_action M = MIEnvForall C → C P → P ⊢ M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_spatial_id P :
    modality_spatial_action M = MIEnvId → P ⊢ M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_intuitionistic_forall_big_and C Ps :
    modality_intuitionistic_action M = MIEnvForall C →
    Forall C Ps →
    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
    { rewrite affinely_True_emp. apply modality_emp. }
    rewrite affinely_and -modality_and_forall //. apply and_mono, IH.
    by eapply modality_intuitionistic_forall.
  Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_intuitionistic_id_big_and Ps :
    modality_intuitionistic_action M = MIEnvId →
    (<affine> [∧ list] P ∈ Ps, <pers> P) ⊢ M (<affine> [∧ list] P ∈ Ps, <pers> P).
Proof.
    intros. induction Ps as [|P Ps IH]; simpl.
    { rewrite affinely_True_emp. apply modality_emp. }
    rewrite -affinely_and_r. rewrite {1}IH {IH}.
    rewrite !persistently_and_intuitionistically_sep_l.
    by rewrite {1}(modality_intuitionistic_id P) // modality_sep.
  Qed.
(* iris/proofmode/modalities.v *)
Lemma modality_spatial_forall_big_sep C Ps :
    modality_spatial_action M = MIEnvForall C →
    Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
Proof.
    induction 2 as [|P Ps ? _ IH]; simpl.
    - by rewrite -modality_emp.
    - by rewrite -modality_sep -IH {1}(modality_spatial_forall _ P).
  Qed.
(* iris/proofmode/modalities.v *)
(* The identity modality [modality_id] can be used in combination with
[FromModal True modality_id] to support introduction for modalities that enjoy
[P ⊢ M P]. This is done by defining an instance [FromModal True modality_id (M P) P],
which will instruct [iModIntro] to introduce the modality without modifying the
proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
[monPred_subjectively] and [bi_absorbingly]. *)
Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
Proof. split; simpl; eauto. Qed.
(* iris/proofmode/modalities.v *)
Definition modality_id {PROP : bi}
:= Modality (@id PROP) modality_id_mixin.
(* iris/proofmode/modality_instances.v *)
Lemma modality_persistently_mixin :
    modality_mixin (@bi_persistently PROP) MIEnvId MIEnvClear.
Proof.
    split; simpl; eauto using equiv_entails_1_2, persistently_intro,
      persistently_mono, persistently_sep_2 with typeclass_instances.
  Qed.
(* iris/proofmode/modality_instances.v *)
Definition modality_persistently
:=
    Modality _ modality_persistently_mixin.
(* iris/proofmode/modality_instances.v *)
Lemma modality_affinely_mixin :
    modality_mixin (@bi_affinely PROP) MIEnvId (MIEnvForall Affine).
Proof.
    split; simpl; eauto using equiv_entails_1_2, affinely_intro, affinely_mono,
      affinely_sep_2 with typeclass_instances.
  Qed.
(* iris/proofmode/modality_instances.v *)
Definition modality_affinely
:=
    Modality _ modality_affinely_mixin.
(* iris/proofmode/modality_instances.v *)
Lemma modality_intuitionistically_mixin :
    modality_mixin (@bi_intuitionistically PROP) MIEnvId MIEnvIsEmpty.
Proof.
    split; simpl; eauto using equiv_entails_1_2, intuitionistically_emp,
      affinely_mono, persistently_mono, intuitionistically_idemp,
      intuitionistically_sep_2 with typeclass_instances.
  Qed.
(* iris/proofmode/modality_instances.v *)
Definition modality_intuitionistically
:=
    Modality _ modality_intuitionistically_mixin.
(* iris/proofmode/modality_instances.v *)
Lemma modality_embed_mixin `{!BiEmbed PROP PROP'} :
    modality_mixin (@embed PROP PROP' _)
      (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
Proof.
    split; simpl; split_and?;
      eauto using equiv_entails_1_2, embed_emp_2, embed_sep, embed_and.
    - intros P Q. rewrite /IntoEmbed=> ->. by rewrite embed_intuitionistically_2.
    - by intros P Q ->.
  Qed.
(* iris/proofmode/modality_instances.v *)
Definition modality_embed `{!BiEmbed PROP PROP'}
:=
    Modality _ modality_embed_mixin.
(* iris/proofmode/modality_instances.v *)
Lemma modality_plainly_mixin `{!Sbi PROP} :
    modality_mixin (@plainly PROP _) (MIEnvForall Plain) MIEnvClear.
Proof.
    split; simpl; split_and?; eauto using equiv_entails_1_2, plainly_intro,
      plainly_mono, plainly_and, plainly_sep_2 with typeclass_instances.
  Qed.
(* iris/proofmode/modality_instances.v *)
Definition modality_plainly `{!Sbi PROP}
:=
    Modality _ modality_plainly_mixin.
(* iris/proofmode/modality_instances.v *)
Lemma modality_laterN_mixin n :
    modality_mixin (@bi_laterN PROP n)
      (MIEnvTransform (MaybeIntoLaterN false n)) (MIEnvTransform (MaybeIntoLaterN false n)).
Proof.
    split; simpl; split_and?; eauto using equiv_entails_1_2, laterN_intro,
      laterN_mono, laterN_and, laterN_sep with typeclass_instances.
    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_intuitionistically_2.
  Qed.
(* iris/proofmode/modality_instances.v *)
Definition modality_laterN n
:=
    Modality _ (modality_laterN_mixin n).
(* iris/proofmode/monpred.v *)
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
      (P : monPred I PROP) (𝓟 : PROP)
:=
  make_monPred_at : P i ⊣⊢ 𝓟.
(* iris/proofmode/monpred.v *)
Class IsBiIndexRel {I : biIndex} (i j : I)
:= is_bi_index_rel : i ⊑ j.
(* iris/proofmode/monpred.v *)
Instance is_bi_index_rel_refl {I : biIndex} (i : I) : IsBiIndexRel i i | 0.
Proof. by rewrite /IsBiIndexRel. Qed.
(* iris/proofmode/monpred.v *)
(* Frame [𝓡] into the goal [monPred_at P i] and determine the remainder [𝓠].
    Used when framing encounters a monPred_at in the goal. *)
Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
      (𝓡 : PROP) (P : monPred I PROP) (𝓠 : PROP)
:=
  frame_monPred_at : □?p 𝓡 ∗ 𝓠 ⊢ P i.
(* iris/proofmode/monpred.v *)
Lemma modality_objectively_mixin :
    modality_mixin (@monPred_objectively I PROP)
      (MIEnvFilter Objective) (MIEnvFilter Objective).
Proof.
    split; simpl; split_and?; intros;
      try select (TCDiag _ _ _) (fun H => destruct H);
      eauto using bi.equiv_entails_1_2, objective_objectively,
        monPred_objectively_mono, monPred_objectively_and,
        monPred_objectively_sep_2 with typeclass_instances.
  Qed.
(* iris/proofmode/monpred.v *)
Definition modality_objectively
:=
    Modality _ modality_objectively_mixin.
(* iris/proofmode/monpred.v *)
Notation MakeMonPredAt
:= (@MakeMonPredAt I PROP).
(* iris/proofmode/monpred.v *)
Instance from_modal_objectively P :
  FromModal True modality_objectively (<obj> P) (<obj> P) P | 1.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/monpred.v *)
Instance from_modal_subjectively P :
  FromModal True modality_id (<subj> P) (<subj> P) P | 1.
Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
(* iris/proofmode/monpred.v *)
Instance from_modal_affinely_monPred_at φ `(sel : A) P Q 𝓠 i :
  FromModal φ modality_affinely sel P Q →
  MakeMonPredAt i Q 𝓠 →
  FromModal φ modality_affinely sel (P i) 𝓠 | 0.
Proof.
  rewrite /FromModal /MakeMonPredAt /==> HPQ <- ?.
  by rewrite -HPQ // monPred_at_affinely.
Qed.