phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/environments.v *)
Lemma envs_snoc_sound Δ p i P :
  envs_lookup i Δ = None → of_envs Δ ⊢ □?p P -∗ of_envs (envs_snoc Δ p i P).
Proof.
  rewrite /envs_lookup /envs_snoc !of_envs_eq=> ?; apply pure_elim_l=> Hwf.
  destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
  apply wand_intro_l; destruct p; simpl.
  - apply and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
      intros j; destruct (ident_beq_reflect j i); naive_solver.
    + rewrite -persistently_and_intuitionistically_sep_l assoc //.
  - apply and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
      intros j; destruct (ident_beq_reflect j i); naive_solver.
    + rewrite (comm _ P) -persistent_and_sep_assoc.
      apply and_mono; first done. rewrite comm //.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_app_sound Δ Δ' p Γ :
  envs_app p Γ Δ = Some Δ' →
  of_envs Δ ⊢ (if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ'.
Proof.
  rewrite !of_envs_eq /envs_app=> ?; apply pure_elim_l=> Hwf.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_app Γ Γp) as [Γp'|] eqn:Heqo; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + apply and_intro.
      * rewrite and_elim_l. rewrite (env_app_perm _ _ Γp') //.
        rewrite affinely_elim big_opL_app sep_and. done.
      * rewrite and_elim_r. rewrite sep_elim_r. done.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_app Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_app_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      naive_solver eauto using env_app_fresh.
    + rewrite (env_app_perm _ _ Γs') // big_opL_app. apply and_intro.
      * rewrite and_elim_l. rewrite sep_elim_r. done.
      * rewrite and_elim_r. done.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_app_singleton_sound Δ Δ' p j Q :
  envs_app p (Esnoc Enil j Q) Δ = Some Δ' → of_envs Δ ⊢ □?p Q -∗ of_envs Δ'.
Proof. move=> /envs_app_sound. destruct p; by rewrite /= right_id. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
  envs_simple_replace i p Γ Δ = Some Δ' →
  of_envs (envs_delete true i p Δ) ⊢
  (if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ'.
Proof.
  rewrite /envs_simple_replace /envs_delete !of_envs_eq=> ?.
  apply pure_elim_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
  - destruct (env_app Γ Γs) eqn:Happ,
      (env_replace i Γ Γp) as [Γp'|] eqn:Heqo; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γp') //.
      rewrite big_opL_app. apply and_intro; first apply and_intro.
      * rewrite and_elim_l affinely_elim sep_elim_l. done.
      * rewrite sep_elim_r and_elim_l //.
      * rewrite and_elim_r sep_elim_r //.
  - destruct (env_app Γ Γp) eqn:Happ,
      (env_replace i Γ Γs) as [Γs'|] eqn:?; simplify_eq/=.
    apply wand_intro_l, and_intro; [apply pure_intro|].
    + destruct Hwf; constructor; simpl; eauto using env_replace_wf.
      intros j. apply (env_app_disjoint _ _ _ j) in Happ.
      destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
    + rewrite (env_replace_perm _ _ Γs') // big_opL_app.
      apply and_intro.
      * rewrite and_elim_l. rewrite sep_elim_r. done.
      * rewrite and_elim_r. done.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_simple_replace_singleton_sound' Δ Δ' i p j Q :
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
  of_envs (envs_delete true i p Δ) ⊢ □?p Q -∗ of_envs Δ'.
Proof. move=> /envs_simple_replace_sound'. destruct p; by rewrite /= right_id. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
  of_envs Δ ⊢ □?p P ∗ ((if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_simple_replace_maybe_sound Δ Δ' i p P Γ :
  envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
  of_envs Δ ⊢
  □?p P ∗ (((if p then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ') ∧
           (□?p P -∗ of_envs Δ)).
Proof.
  intros. apply pure_elim with (envs_wf Δ).
  { rewrite of_envs_eq. apply and_elim_l. }
  intros. rewrite {1}envs_lookup_sound//. apply sep_mono_r, and_intro.
  - rewrite envs_simple_replace_sound'//.
  - apply wand_intro_l, envs_lookup_sound_2; done.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_simple_replace_singleton_sound Δ Δ' i p P j Q :
  envs_lookup i Δ = Some (p,P) →
  envs_simple_replace i p (Esnoc Enil j Q) Δ = Some Δ' →
  of_envs Δ ⊢ □?p P ∗ (□?p Q -∗ of_envs Δ').
Proof.
  intros. by rewrite envs_lookup_sound// envs_simple_replace_singleton_sound'//.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_replace_sound' Δ Δ' i p q Γ :
  envs_replace i p q Γ Δ = Some Δ' →
  of_envs (envs_delete true i p Δ) ⊢
  (if q then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ'.
Proof.
  rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
  - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
  - apply envs_app_sound.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_replace_singleton_sound' Δ Δ' i p q j Q :
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
  of_envs (envs_delete true i p Δ) ⊢ □?q Q -∗ of_envs Δ'.
Proof. move=> /envs_replace_sound'. destruct q; by rewrite /= ?right_id. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_replace_sound Δ Δ' i p q P Γ :
  envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
  of_envs Δ ⊢ □?p P ∗ ((if q then <affine> env_and_persistently Γ else [∗] Γ) -∗ of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_replace_singleton_sound Δ Δ' i p q P j Q :
  envs_lookup i Δ = Some (p,P) →
  envs_replace i p q (Esnoc Enil j Q) Δ = Some Δ' →
  of_envs Δ ⊢ □?p P ∗ (□?q Q -∗ of_envs Δ').
Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_lookup_envs_clear_spatial Δ j :
  envs_lookup j (envs_clear_spatial Δ)
  = '(p,P) ← envs_lookup j Δ; if p : bool then Some (p,P) else None.
Proof.
  rewrite /envs_lookup /envs_clear_spatial.
  destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
  by destruct (Γs !! j).
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_clear_spatial_sound Δ :
  of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ.
Proof.
  rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
  rewrite -persistent_and_sep_assoc. apply and_intro.
  - apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
  - rewrite -persistent_and_sep_assoc left_id. done.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_clear_intuitionistic_sound Δ :
  of_envs Δ ⊢
  env_and_persistently (env_intuitionistic Δ) ∗ of_envs (envs_clear_intuitionistic Δ).
Proof.
  rewrite !of_envs_eq /envs_clear_spatial /=. apply pure_elim_l=> Hwf.
  rewrite persistent_and_sep_1.
  rewrite (pure_True); first by rewrite 2!left_id.
  destruct Hwf. constructor; simpl; auto using Enil_wf.
Qed.
(* iris/proofmode/environments.v *)
Lemma env_spatial_is_nil_intuitionistically Δ :
  env_spatial_is_nil Δ = true → of_envs Δ ⊢ □ of_envs Δ.
Proof.
  intros. rewrite !of_envs_eq; destruct Δ as [? []]; simplify_eq/=.
  rewrite /bi_intuitionistically !persistently_and.
  rewrite persistently_pure persistent_persistently -persistently_emp_2.
  apply and_intro; last done. rewrite !and_elim_r. done.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_lookup_envs_delete Δ i p P :
  envs_wf Δ →
  envs_lookup i Δ = Some (p,P) → envs_lookup i (envs_delete true i p Δ) = None.
Proof.
  rewrite /envs_lookup /envs_delete=> -[?? Hdisj] Hlookup.
  destruct Δ as [Γp Γs], p; simplify_eq/=.
  - rewrite env_lookup_env_delete //. revert Hlookup.
    destruct (Hdisj i) as [->| ->]; [|done]. by destruct (Γs !! _).
  - rewrite env_lookup_env_delete //. by destruct (Γp !! _).
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_lookup_envs_delete_ne Δ rp i j p :
  i ≠ j → envs_lookup i (envs_delete rp j p Δ) = envs_lookup i Δ.
Proof.
  rewrite /envs_lookup /envs_delete=> ?. destruct Δ as [Γp Γs],p; simplify_eq/=.
  - destruct rp=> //. by rewrite env_lookup_env_delete_ne.
  - destruct (Γp !! i); simplify_eq/=; by rewrite ?env_lookup_env_delete_ne.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_incr_counter_equiv Δ : envs_Forall2 (⊣⊢) Δ (envs_incr_counter Δ).
Proof. done. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_incr_counter_sound Δ : of_envs (envs_incr_counter Δ) ⊣⊢ of_envs Δ.
Proof. by f_equiv. Qed.
(* iris/proofmode/environments.v *)
Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
  (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) →
  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') →
  of_envs Δ1 ∗ of_envs Δ2 ⊢ of_envs Δ1' ∗ of_envs Δ2'.
Proof.
  revert Δ1 Δ2.
  induction js as [|j js IH]=> Δ1 Δ2 Hlookup HΔ; simplify_eq/=; [done|].
  apply pure_elim with (envs_wf Δ1)=> [|Hwf].
  { by rewrite !of_envs_eq !and_elim_l sep_elim_l. }
  destruct (envs_lookup_delete _ j Δ1)
    as [[[[] P] Δ1'']|] eqn:Hdel; simplify_eq/=; auto.
  apply envs_lookup_delete_Some in Hdel as [??]; subst.
  rewrite envs_lookup_sound //; rewrite /= (comm _ P) -assoc.
  rewrite -(IH _ _ _ HΔ); last first.
   { intros j' P'; destruct (decide (j = j')) as [->|].
     - by rewrite (envs_lookup_envs_delete _ _ _ P).
     - rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
  rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
(* iris/proofmode/environments.v *)
Lemma envs_split_sound Δ d js Δ1 Δ2 :
  envs_split d js Δ = Some (Δ1,Δ2) → of_envs Δ ⊢ of_envs Δ1 ∗ of_envs Δ2.
Proof.
  rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Δ)).
  rewrite {2}envs_clear_spatial_sound.
  rewrite (env_spatial_is_nil_intuitionistically (envs_clear_spatial _)) //.
  rewrite -persistently_and_intuitionistically_sep_l.
  rewrite (and_elim_l (<pers> _)%I)
          persistently_and_intuitionistically_sep_r intuitionistically_elim.
  destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
  apply envs_split_go_sound in HΔ as ->; last first.
  { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
  destruct d; simplify_eq/=; [|done]. by rewrite comm.
Qed.
(* iris/proofmode/environments.v *)
Lemma env_to_prop_sound Γ : env_to_prop Γ ⊣⊢ [∗] Γ.
Proof.
  destruct Γ as [|Γ i P]; simpl; first done.
  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
  - by rewrite right_id.
  - rewrite /= IH (comm _ Q _) assoc. done.
Qed.
(* iris/proofmode/environments.v *)
Lemma env_to_prop_and_pers_sound Γ i P :
  □ env_to_prop_and (Esnoc Γ i P) ⊣⊢ <affine> env_and_persistently (Esnoc Γ i P).
Proof.
  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
  - by rewrite right_id.
  - rewrite /= IH. clear IH. f_equiv. simpl.
    rewrite assoc. f_equiv.
    rewrite persistently_and comm. done.
Qed.
(* iris/proofmode/ident_name.v *)
(* [ident_name] is a way to remember an identifier within the binder of a
(trivial) function, which can be constructed and retrieved with Ltac but is easy
to forward around opaquely in Gallina (through typeclasses, for example) *)
Definition ident_name
:= unit → unit.
(* iris/proofmode/ident_name.v *)
(* [to_ident_name id] returns a constr of type [ident_name] that holds [id] in
the binder name *)
Ltac to_ident_name id
:=
  eval cbv in (ltac:(clear; intros id; assumption) : unit → unit).
(* iris/proofmode/ident_name.v *)
(* to_ident_name is a Gallina-level version of [to_ident_name] for constructing
    [ident_name] literals. *)
Notation to_ident_name id
:= (λ id:unit, id) (only parsing).
(* iris/proofmode/ident_name.v *)
(* The idea of [AsIdentName] is to convert the binder in [f] to an [ident_name]
representing the name of the binder. If [f] is not a lambda, this typeclass can
produce the fallback identifier [__unknown]. For example, if the user writes
[bi_exist Φ], there is no binder anywhere to extract.

This class has only one instance, a [Hint Extern] which implements that
conversion to resolve [name] in Ltac (see [solve_as_ident_name]). *)
Class AsIdentName {A B} (f : A → B) (name : ident_name)
:= as_ident_name {}.
(* iris/proofmode/ident_name.v *)
Ltac solve_as_ident_name
:=
  lazymatch goal with
  (* The [H] here becomes the default name if the binder is anonymous. We use
     [H] with the idea that an unnamed and unused binder is likely to be a
     proposition. *)
  | |- AsIdentName (λ H, _) _ =>
    let name := to_ident_name H in
    notypeclasses refine (as_ident_name name)
  | |- AsIdentName _ _ =>
     let name := to_ident_name ident:(__unknown) in
     notypeclasses refine (as_ident_name name)
  | |- _ => fail "solve_as_ident_name: goal should be `AsIdentName`"
  end.
(* iris/proofmode/intro_patterns.v *)
Inductive gallina_ident
:=
  | IGallinaNamed : string → gallina_ident
  | IGallinaAnon : gallina_ident.
(* iris/proofmode/intro_patterns.v *)
Inductive intro_pat
:=
  | IIdent : ident → intro_pat
  | IFresh : intro_pat
  | IDrop : intro_pat
  | IFrame : intro_pat
  | IList : list (list intro_pat) → intro_pat
  | IPure : gallina_ident → intro_pat
  | IIntuitionistic : intro_pat → intro_pat
  | ISpatial : intro_pat → intro_pat
  | IModalElim : intro_pat → intro_pat
  | IRewrite : direction → intro_pat
  | IPureIntro : intro_pat
  | IModalIntro : intro_pat
  | ISimpl : intro_pat
  | IDone : intro_pat
  | IForall : intro_pat
  | IAll : intro_pat
  | IClear : sel_pat → intro_pat
  | IClearFrame : sel_pat → intro_pat.
(* iris/proofmode/intro_patterns.v *)
Inductive stack_item
:=
  | StPat : intro_pat → stack_item
  | StList : stack_item
  | StConjList : stack_item
  | StBar : stack_item
  | StAmp : stack_item
  | StIntuitionistic : stack_item
  | StSpatial : stack_item
  | StModalElim : stack_item.
(* iris/proofmode/intro_patterns.v *)
Notation stack
:= (list stack_item).
(* iris/proofmode/intro_patterns.v *)
Fixpoint close_list (k : stack)
    (ps : list intro_pat) (pss : list (list intro_pat)) : option stack
:=
  match k with
  | StList :: k => Some (StPat (IList (ps :: pss)) :: k)
  | StPat pat :: k => close_list k (pat :: ps) pss
  | StIntuitionistic :: k =>
     '(p,ps) ← maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
  | StModalElim :: k =>
     '(p,ps) ← maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
  | StBar :: k => close_list k [] (ps :: pss)
  | _ => None
  end.
(* iris/proofmode/intro_patterns.v *)
Fixpoint big_conj (ps : list intro_pat) : intro_pat
:=
  match ps with
  | [] => IList [[]]
  | [p] => IList [[ p ]]
  | [p1;p2] => IList [[ p1 ; p2 ]]
  | p :: ps => IList [[ p ; big_conj ps ]]
  end.
(* iris/proofmode/intro_patterns.v *)
Fixpoint close_conj_list (k : stack)
    (cur : option intro_pat) (ps : list intro_pat) : option stack
:=
  match k with
  | StConjList :: k =>
     ps ← match cur with
          | None => guard (ps = []);; Some [] | Some p => Some (p :: ps)
          end;
     Some (StPat (big_conj ps) :: k)
  | StPat pat :: k => guard (cur = None);; close_conj_list k (Some pat) ps
  | StIntuitionistic :: k => p ← cur; close_conj_list k (Some (IIntuitionistic p)) ps
  | StSpatial :: k => p ← cur; close_conj_list k (Some (ISpatial p)) ps
  | StModalElim :: k => p ← cur; close_conj_list k (Some (IModalElim p)) ps
  | StAmp :: k => p ← cur; close_conj_list k None (p :: ps)
  | _ => None
  end.
(* iris/proofmode/intro_patterns.v *)
Fixpoint parse_go (ts : list token) (k : stack) : option stack
:=
  match ts with
  | [] => Some k
  | TName "_" :: ts => parse_go ts (StPat IDrop :: k)
  | TName s :: ts => parse_go ts (StPat (IIdent s) :: k)
  | TAnon :: ts => parse_go ts (StPat IFresh :: k)
  | TFrame :: ts => parse_go ts (StPat IFrame :: k)
  | TBracketL :: ts => parse_go ts (StList :: k)
  | TBar :: ts => parse_go ts (StBar :: k)
  | TBracketR :: ts => close_list k [] [] ≫= parse_go ts
  | TParenL :: ts => parse_go ts (StConjList :: k)
  | TAmp :: ts => parse_go ts (StAmp :: k)
  | TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
  | TPure (Some s) :: ts => parse_go ts (StPat (IPure (IGallinaNamed s)) :: k)
  | TPure None :: ts => parse_go ts (StPat (IPure IGallinaAnon) :: k)
  | TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
  | TMinus :: TIntuitionistic :: ts => parse_go ts (StSpatial :: k)
  | TModal :: ts => parse_go ts (StModalElim :: k)
  | TArrow d :: ts => parse_go ts (StPat (IRewrite d) :: k)
  | TPureIntro :: ts => parse_go ts (StPat IPureIntro :: k)
  | (TModalIntro | TIntuitionisticIntro) :: ts => parse_go ts (StPat IModalIntro :: k)
  | TSimpl :: ts => parse_go ts (StPat ISimpl :: k)
  | TDone :: ts => parse_go ts (StPat IDone :: k)
  | TAll :: ts => parse_go ts (StPat IAll :: k)
  | TForall :: ts => parse_go ts (StPat IForall :: k)
  | TBraceL :: ts => parse_clear ts k
  | _ => None
  end
with parse_clear (ts : list token) (k : stack) : option stack :=
  match ts with
  | TFrame :: TName s :: ts => parse_clear ts (StPat (IClearFrame (SelIdent s)) :: k)
  | TFrame :: TPure None :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
  | TFrame :: TIntuitionistic :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: k)
  | TFrame :: TSep :: ts => parse_clear ts (StPat (IClearFrame SelSpatial) :: k)
  | TName s :: ts => parse_clear ts (StPat (IClear (SelIdent s)) :: k)
  | TPure None :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
  | TIntuitionistic :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
  | TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
  | TBraceR :: ts => parse_go ts k
  | _ => None
  end.
(* iris/proofmode/intro_patterns.v *)
Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat)
:=
  match k with
  | [] => Some ps
  | StPat pat :: k => close k (pat :: ps)
  | StIntuitionistic :: k => '(p,ps) ← maybe2 (::) ps; close k (IIntuitionistic p :: ps)
  | StSpatial :: k => '(p,ps) ← maybe2 (::) ps; close k (ISpatial p :: ps)
  | StModalElim :: k => '(p,ps) ← maybe2 (::) ps; close k (IModalElim p :: ps)
  | _ => None
  end.
(* iris/proofmode/intro_patterns.v *)
Definition parse (s : string) : option (list intro_pat)
:=
  k ← parse_go (tokenize s) []; close k [].
(* iris/proofmode/intro_patterns.v *)
Ltac parse s
:=
  lazymatch type of s with
  | list intro_pat => s
  | intro_pat => constr:([s])
  | list string =>
     lazymatch eval vm_compute in (mjoin <$> mapM parse s) with
     | Some ?pats => pats
     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
     end
  | string =>
     lazymatch eval vm_compute in (parse s) with
     | Some ?pats => pats
     | _ => fail "intro_pat.parse: cannot parse" s "as an introduction pattern"
     end
  | ident => constr:([IIdent s])
  | ?X => fail "intro_pat.parse: the term" s
     "is expected to be an introduction pattern"
     "(usually a string),"
     "but has unexpected type" X
  end.
(* iris/proofmode/intro_patterns.v *)
Ltac parse_one s
:=
  lazymatch type of s with
  | intro_pat => s
  | string =>
     lazymatch eval vm_compute in (parse s) with
     | Some [?pat] => pat
     | _ => fail "intro_pat.parse_one: cannot parse" s "as an introduction pattern"
     end
  | ?X => fail "intro_pat.parse_one: the term" s
     "is expected to be an introduction pattern"
     "(usually a string),"
     "but has unexpected type" X
  end.
(* iris/proofmode/intro_patterns.v *)
Fixpoint intro_pat_intuitionistic (p : intro_pat)
:=
  match p with
  | IPure _ => true
  | IRewrite _ => true
  | IIntuitionistic _ => true
  | IList pps => forallb (forallb intro_pat_intuitionistic) pps
  | ISimpl => true
  | IClear _ => true
  | IClearFrame _ => true
  | _ => false
  end.
(* iris/proofmode/intro_patterns.v *)
Ltac intro_pat_intuitionistic p
:=
  lazymatch type of p with
  | intro_pat => eval cbv in (intro_pat_intuitionistic p)
  | list intro_pat => eval cbv in (forallb intro_pat_intuitionistic p)
  | string =>
     let pat := intro_pat.parse p in
     eval cbv in (forallb intro_pat_intuitionistic pat)
  | ident => false
  | bool => p
  | ?X => fail "intro_pat_intuitionistic: the term" p
     "is expected to be an introduction pattern"
     "(usually a string),"
     "but has unexpected type" X
  end.
(* iris/proofmode/ltac_tactics.v *)
(* Tactic used for solving side-conditions arising from TC resolution in [iMod]
and [iInv]. *)
Ltac iSolveSideCondition
:=
  lazymatch goal with
  | |- pm_error ?err => fail "" err
  | _ => split_and?; try solve [ fast_done | solve_ndisj | tc_solve ]
  end.
(* iris/proofmode/ltac_tactics.v *)
(* Used for printing [string]s and [ident]s. *)
Ltac pretty_ident H
:=
  lazymatch H with
  | INamed ?H => H
  | ?H => H
  end.
(* iris/proofmode/ltac_tactics.v *)
(* * Misc *)
Ltac iGetCtx
:=
  lazymatch goal with
  | |- envs_entails ?Δ _ => Δ
  | |- context[ envs_split _ _ ?Δ ] => Δ
  end.
(* iris/proofmode/ltac_tactics.v *)
Ltac iMissingHypsCore Δ Hs
:=
  let Hhyps := pm_eval (envs_dom Δ) in
  eval vm_compute in (list_difference Hs Hhyps).
(* iris/proofmode/ltac_tactics.v *)
Ltac iMissingHyps Hs
:=
  let Δ := iGetCtx in
  iMissingHypsCore Δ Hs.
(* iris/proofmode/ltac_tactics.v *)
Ltac iTypeOf H
:=
  let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
  pm_eval (envs_lookup H Δ).
(* iris/proofmode/ltac_tactics.v *)
Ltac iBiOfGoal
:=
  match goal with |- @envs_entails ?PROP _ _ => PROP end.
(* iris/proofmode/ltac_tactics.v *)
(* The tactic [iFresh] bumps the fresh name counter in the proof mode
environment and returns the old value.

Note that we use [Ltac] instead of [Tactic Notation] since [Tactic Notation]
tactics can only have side-effects, but cannot return terms. *)
Ltac iFresh
:=
  (* We make use of an Ltac hack to allow the [iFresh] tactic to both have a
  side-effect (i.e. to bump the counter) and to return a value (the fresh name).
  We do this by wrapped the side-effect under a [match] in a let-binding. See
  https://stackoverflow.com/a/46178884 *)
  let start :=
    lazymatch goal with
    | _ => iStartProof
    end in
  let c :=
    lazymatch goal with
    | |- envs_entails (Envs _ _ ?c) _ => c
    end in
  let inc :=
    lazymatch goal with
    | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
      let c' := eval vm_compute in (Pos.succ c) in
      change_no_check (envs_entails (Envs Δp Δs c') Q)
    end in
  constr:(IAnon c).
(* iris/proofmode/ltac_tactics.v *)
(* Elaborated selection patterns, unlike the type [sel_pat], contains
only specific identifiers, and no wildcards like `#` (with the
exception of the pure selection pattern `%`) *)
Inductive esel_pat
:=
  | ESelPure
  | ESelIdent : (* whether the ident is intuitionistic *) bool → ident → esel_pat.
(* iris/proofmode/ltac_tactics.v *)
Ltac iElaborateSelPat_go pat Δ Hs
:=
  lazymatch pat with
  | [] => eval cbv in Hs
  | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)
  | SelIntuitionistic :: ?pat =>
    let Hs' := pm_eval (env_dom (env_intuitionistic Δ)) in
    let Δ' := pm_eval (envs_clear_intuitionistic Δ) in
    iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
  | SelSpatial :: ?pat =>
    let Hs' := pm_eval (env_dom (env_spatial Δ)) in
    let Δ' := pm_eval (envs_clear_spatial Δ) in
    iElaborateSelPat_go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
  | SelIdent ?H :: ?pat =>
    lazymatch pm_eval (envs_lookup_delete false H Δ) with
    | Some (?p,_,?Δ') =>  iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs)
    | None =>
      let H := pretty_ident H in
      fail "iElaborateSelPat:" H "not found"
    end
  end.