phanerozoic/Coq-Iris huggingface dataset:
(* iris/proofmode/class_instances_make.v *)
Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100.
Proof. by rewrite /MakeExcept0. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_assumption_plainly_l_true P Q :
  FromAssumption true P Q → KnownLFromAssumption true (■ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  rewrite intuitionistically_plainly_elim //.
Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_assumption_plainly_l_false `{!BiAffine PROP} P Q :
  FromAssumption true P Q → KnownLFromAssumption false (■ P) Q.
Proof.
  rewrite /KnownLFromAssumption /FromAssumption /= =><-.
  rewrite plainly_elim_persistently intuitionistically_into_persistently //.
Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_pure_plainly P φ :
  FromPure false P φ → FromPure false (■ P) φ.
Proof. rewrite /FromPure=> <-. by rewrite plainly_pure. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_pure_plainly P φ :
  IntoPure P φ → IntoPure (■ P) φ.
Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_wand_plainly_true q R P Q :
  IntoWand true q R P Q → IntoWand true q (■ R) P Q.
Proof. rewrite /IntoWand /= intuitionistically_plainly_elim //. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_wand_plainly_false q R P Q :
  Absorbing R → IntoWand false q R P Q → IntoWand false q (■ R) P Q.
Proof. intros ?. by rewrite /IntoWand plainly_elim. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_and_plainly P Q1 Q2 :
  FromAnd P Q1 Q2 → FromAnd (■ P) (■ Q1) (■ Q2).
Proof. rewrite /FromAnd=> <-. by rewrite plainly_and. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_sep_plainly P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (■ P) (■ Q1) (■ Q2).
Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_and_plainly p P Q1 Q2 :
  IntoAnd p P Q1 Q2 → IntoAnd p (■ P) (■ Q1) (■ Q2).
Proof.
  rewrite /IntoAnd /=. destruct p; simpl.
  - rewrite -plainly_and -[(□ ■ P)%I]intuitionistically_idemp intuitionistically_plainly =>->.
    rewrite [(□ (_ ∧ _))%I]intuitionistically_elim //.
  - intros ->. by rewrite plainly_and.
Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_sep_plainly `{!BiPositive PROP} P Q1 Q2 :
  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_sep_plainly_affine P Q1 Q2 :
  IntoSep P Q1 Q2 →
  TCOr (Affine Q1) (Absorbing Q2) → TCOr (Affine Q2) (Absorbing Q1) →
  IntoSep (■ P) (■ Q1) (■ Q2).
Proof.
  rewrite /IntoSep /= => -> ??. by rewrite sep_and plainly_and plainly_and_sep_l_1.
Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_or_plainly P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (■ P) (■ Q1) (■ Q2).
Proof. rewrite /FromOr=> <-. by rewrite -plainly_or_2. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_or_plainly `{!SbiEmpValidExist PROP} P Q1 Q2 :
  IntoOr P Q1 Q2 → IntoOr (■ P) (■ Q1) (■ Q2).
Proof. rewrite /IntoOr=>->. by rewrite plainly_or. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_exist_plainly {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (■ P) (λ a, ■ (Φ a))%I.
Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_exist_plainly `{!SbiEmpValidExist PROP}
    {A} P (Φ : A → PROP) name :
  IntoExist P Φ name → IntoExist (■ P) (λ a, ■ (Φ a))%I name.
Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_forall_plainly {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (■ P) (λ a, ■ (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_forall_plainly {A} P (Φ : A → PROP) name :
  FromForall P Φ name → FromForall (■ P) (λ a, ■ (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance from_modal_plainly P :
  FromModal True modality_plainly (■ P) (■ P) P | 2.
Proof. by rewrite /FromModal. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_except_0_plainly `{!BiPlainlyExist PROP} P Q :
  IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
(* iris/proofmode/class_instances_plainly.v *)
Instance into_later_plainly n P Q :
  IntoLaterN false n P Q → IntoLaterN false n (■ P) (■ Q).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_assumption_bupd `{!BiBUpd PROP} p P Q :
  FromAssumption p P Q → KnownRFromAssumption p P (|==> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_assumption_fupd
    `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} E p P Q :
  FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_fupd. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
  FromPure a P φ → FromPure a (|==> P) φ.
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_pure_fupd `{!BiFUpd PROP} a E P φ :
  FromPure a P φ → FromPure a (|={E}=> P) φ.
Proof. rewrite /FromPure=> <-. apply fupd_intro. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_wand_bupd `{!BiBUpd PROP} p q R P Q :
  IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_wand_fupd `{!BiFUpd PROP} E p q R P Q :
  IntoWand false false R P Q →
  IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_wand_bupd_persistent `{!BiBUpd PROP} p q R P Q :
  IntoWand false q R P Q → IntoWand p q (|==> R) P (|==> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_wand_fupd_persistent `{!BiFUpd PROP} E1 E2 p q R P Q :
  IntoWand false q R P Q → IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
Proof.
  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
  apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_wand_bupd_args `{!BiBUpd PROP} p q R P Q :
  IntoWand p false R P Q → IntoWand' p q R (|==> P) (|==> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => ->.
  apply wand_intro_l. by rewrite intuitionistically_if_elim bupd_wand_r.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_wand_fupd_args `{!BiFUpd PROP} E1 E2 p q R P Q :
  IntoWand p false R P Q → IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof.
  rewrite /IntoWand' /IntoWand /= => ->.
  apply wand_intro_l. by rewrite intuitionistically_if_elim fupd_wand_r.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_sep_bupd `{!BiBUpd PROP} P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_sep_fupd `{!BiFUpd PROP} E P Q1 Q2 :
  FromSep P Q1 Q2 → FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_or_bupd `{!BiBUpd PROP} P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /FromOr=><-. apply bupd_or. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_or_fupd `{!BiFUpd PROP} E1 E2 P Q1 Q2 :
  FromOr P Q1 Q2 → FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /FromOr=><-. apply fupd_or. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_and_bupd `{!BiBUpd PROP} P Q1 Q2 :
  IntoAnd false P Q1 Q2 → IntoAnd false (|==> P) (|==> Q1) (|==> Q2).
Proof. rewrite /IntoAnd/==>->. apply bupd_and. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_and_fupd `{!BiFUpd PROP} E1 E2 P Q1 Q2 :
  IntoAnd false P Q1 Q2 → IntoAnd false (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
Proof. rewrite /IntoAnd/==>->. apply fupd_and. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_exist_bupd `{!BiBUpd PROP} {A} P (Φ : A → PROP) :
  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
Proof. rewrite /FromExist=><-. apply bupd_exist. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_exist_fupd `{!BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
  FromExist P Φ → FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof. rewrite /FromExist=><-. apply fupd_exist. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_forall_bupd `{!BiBUpd PROP} {A} P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (|==> P) (λ a, |==> Φ a)%I.
Proof. rewrite /IntoForall=>->. apply bupd_forall. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance into_forall_fupd `{!BiFUpd PROP} {A} E1 E2 P (Φ : A → PROP) :
  IntoForall P Φ → IntoForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
Proof. rewrite /IntoForall=>->. apply fupd_forall. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_forall_fupd
    `{!BiFUpd PROP, !Sbi PROP, !BiFUpdSbi PROP, !BiAffine PROP}
    E1 E2 {A} P (Φ : A → PROP) name :
  (* Some cases in which [E2 ⊆ E1] holds *)
  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
  FromForall P Φ name → (∀ x, Plain (Φ x)) →
  FromForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> (Φ a))%I name.
Proof.
  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_forall_step_fupd
    `{!BiFUpd PROP, !Sbi PROP, !BiFUpdSbi PROP, !BiAffine PROP}
    E1 E2 {A} P (Φ : A → PROP) name :
  (* Some cases in which [E2 ⊆ E1] holds *)
  TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
  FromForall P Φ name → (∀ x, Plain (Φ x)) →
  FromForall (|={E1}[E2]▷=> P) (λ a, |={E1}[E2]▷=> (Φ a))%I name.
Proof.
  rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance is_except_0_bupd `{!BiBUpd PROP} P : IsExcept0 P → IsExcept0 (|==> P).
Proof.
  rewrite /IsExcept0=> HP.
  by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance is_except_0_fupd `{!BiFUpd PROP} E1 E2 P :
  IsExcept0 (|={E1,E2}=> P).
Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_modal_bupd `{!BiBUpd PROP} P :
  FromModal True modality_id (|==> P) (|==> P) P.
Proof. by rewrite /FromModal /= -bupd_intro. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_modal_fupd E P `{!BiFUpd PROP} :
  FromModal True modality_id (|={E}=> P) (|={E}=> P) P.
Proof. by rewrite /FromModal /= -fupd_intro. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance from_modal_fupd_wrong_mask E1 E2 P `{!BiFUpd PROP} :
  FromModal
        (pm_error "Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities")
    modality_id (|={E1,E2}=> P) (|={E1,E2}=> P) P | 100.
Proof. by intros []. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_modal_bupd `{!BiBUpd PROP} p P Q :
  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
Proof.
  by rewrite /ElimModal
    intuitionistically_if_elim bupd_frame_r wand_elim_r bupd_trans.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_modal_bupd_plain_goal
    `{!BiBUpd PROP, !Sbi PROP, !BiBUpdSbi PROP, !BiAffine PROP} p P Q :
  Plain Q → ElimModal True p false (|==> P) P Q Q.
Proof.
  intros. by rewrite /ElimModal intuitionistically_if_elim
    bupd_frame_r wand_elim_r bupd_elim.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_modal_bupd_plain
    `{!BiBUpd PROP, !Sbi PROP, !BiBUpdSbi PROP, !BiAffine PROP} p P Q :
  Plain P → ElimModal True p p (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_elim wand_elim_r. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_modal_bupd_fupd
    `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} p E1 E2 P Q :
  ElimModal True p false (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Proof.
  by rewrite /ElimModal intuitionistically_if_elim
    (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_modal_fupd_fupd `{!BiFUpd PROP} p E1 E2 E3 P Q :
  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof.
  by rewrite /ElimModal intuitionistically_if_elim
    fupd_frame_r wand_elim_r fupd_trans.
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_modal_fupd_fupd_wrong_mask `{!BiFUpd PROP} p E0 E1 E2 E3 P Q :
  ElimModal
    (pm_error "Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
    p false
    (|={E1,E2}=> P) False (|={E0,E3}=> Q) False | 100.
Proof. intros []. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance add_modal_bupd `{!BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance add_modal_fupd `{!BiFUpd PROP} E1 E2 P Q :
  AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_acc_bupd `{!BiBUpd PROP} {X} α β mγ Q :
  ElimAcc (X:=X) True bupd bupd α β mγ
          (|==> Q)
          (λ x, |==> β x ∗ (mγ x -∗? |==> Q))%I.
Proof.
  iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
Qed.
(* iris/proofmode/class_instances_updates.v *)
Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
  ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α β mγ
          (|={E1,E}=> Q)
          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))%I.
Proof.
  iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
  iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
  iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Starting and stopping the proof mode *)
Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → ⊢ P.
Proof.
  rewrite envs_entails_unseal !of_envs_eq /=.
  rewrite left_id=><-.
  apply and_intro=> //. apply pure_intro; repeat constructor.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_stop Δ P :
  (match env_intuitionistic Δ, env_spatial Δ with
   | Enil, Γs => env_to_prop Γs
   | Γp, Enil => □ env_to_prop_and Γp
   | Γp, Γs => □ env_to_prop_and Γp ∗ env_to_prop Γs
   end ⊢ P) →
  envs_entails Δ P.
Proof.
  rewrite envs_entails_unseal !of_envs_eq. intros <-. rewrite and_elim_r.
  destruct (env_intuitionistic Δ).
  { rewrite env_to_prop_sound and_elim_r //. }
  cbv zeta. destruct (env_spatial Δ).
  - rewrite env_to_prop_and_pers_sound. rewrite comm. done.
  - rewrite env_to_prop_and_pers_sound env_to_prop_sound.
    rewrite /bi_affinely [(emp ∧ _)%I]comm -persistent_and_sep_assoc left_id //.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Basic rules *)
Lemma tac_eval Δ Q Q' :
  (∀ (Q'':=Q'), Q'' ⊢ Q) → (* We introduce [Q''] as a let binding so that
    tactics like `reflexivity` as called by [rewrite //] do not eagerly unify
    it with [Q]. See [test_iEval] in [tests/proofmode]. *)
  envs_entails Δ Q' → envs_entails Δ Q.
Proof. by intros <-. Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_eval_in Δ i p P P' Q :
  envs_lookup i Δ = Some (p, P) →
  (∀ (P'':=P'), P ⊢ P') →
  match envs_simple_replace i p (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_unseal /=. intros ? HP ?.
  rewrite envs_simple_replace_singleton_sound //; simpl.
  by rewrite HP wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Class AffineEnv (Γ : env PROP)
:= affine_env : Forall Affine Γ.
(* iris/proofmode/coq_tactics.v *)
Instance affine_env_nil : AffineEnv Enil.
Proof. constructor. Qed.
(* iris/proofmode/coq_tactics.v *)
Instance affine_env_snoc Γ i P :
  Affine P → AffineEnv Γ → AffineEnv (Esnoc Γ i P).
Proof. by constructor. Qed.
(* iris/proofmode/coq_tactics.v *)
(* If the BI is affine, no need to walk on the whole environment. *)
Instance affine_env_bi `(!BiAffine PROP) Γ : AffineEnv Γ | 0.
Proof. induction Γ; apply _. Qed.
(* iris/proofmode/coq_tactics.v *)
Instance affine_env_spatial Δ :
  AffineEnv (env_spatial Δ) → Affine ([∗] env_spatial Δ).
Proof. intros H. induction H; simpl; apply _. Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_unseal (affine (of_envs Δ)). Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_assumption Δ i p P Q :
  envs_lookup i Δ = Some (p,P) →
  FromAssumption p P Q →
  (let Δ' := envs_delete true i p Δ in
   if env_spatial_is_nil Δ' then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
  envs_entails Δ Q.
Proof.
  intros ?? H. rewrite envs_entails_unseal envs_lookup_sound //.
  simpl in *. destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
  - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_assumption_coq Δ P Q :
  (⊢ P) →
  FromAssumption false P Q →
  (if env_spatial_is_nil Δ then TCTrue
   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ))) →
  envs_entails Δ Q.
Proof.
  rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
  rewrite envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
  rewrite HP HPQ.
  destruct (env_spatial_is_nil _) eqn:?.
  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
  - destruct H; by rewrite sep_elim_l.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_rename Δ i j p P Q :
  envs_lookup i Δ = Some (p,P) →
  match envs_simple_replace i p (Esnoc Enil j P) Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_unseal=> ??. rewrite envs_simple_replace_singleton_sound //.
  by rewrite wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_clear Δ i p P Q :
  envs_lookup i Δ = Some (p,P) →
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
  envs_entails (envs_delete true i p Δ) Q →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
  by destruct p; rewrite /= sep_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * False *)
Lemma tac_ex_falso Δ Q : envs_entails Δ False → envs_entails Δ Q.
Proof. by rewrite envs_entails_unseal -(False_elim Q). Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_false_destruct Δ i p P Q :
  envs_lookup i Δ = Some (p,P) →
  P = False%I →
  envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal => ??. subst. rewrite envs_lookup_sound //; simpl.
  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Pure *)
Lemma tac_pure_intro Δ Q φ a :
  FromPure a Q φ →
  (if a then AffineEnv (env_spatial Δ) else TCTrue) →
  φ →
  envs_entails Δ Q.
Proof.
  intros ???. rewrite envs_entails_unseal -(from_pure a Q). destruct a; simpl.
  - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp.
  - by apply pure_intro.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_pure Δ i p P φ Q :
  envs_lookup i Δ = Some (p, P) →
  IntoPure P φ →
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
  (φ → envs_entails (envs_delete true i p Δ) Q) → envs_entails Δ Q.
Proof.
  rewrite envs_entails_unseal=> ?? HPQ HQ.
  rewrite envs_lookup_sound //; simpl. destruct p; simpl.
  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
    by apply pure_elim_l.
  - destruct HPQ.
    + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
      by apply pure_elim_l.
    + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝) absorbingly_sep_lr.
      rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_pure_revert Δ φ P Q :
  MakeAffinely ⌜ φ ⌝ P →
  envs_entails Δ (P -∗ Q) →
  (φ → envs_entails Δ Q).
Proof.
  rewrite /MakeAffinely envs_entails_unseal. intros <- -> ?.
  by rewrite pure_True // affinely_True_emp left_id.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Intuitionistic *)
Lemma tac_intuitionistic Δ i j p P P' Q :
  envs_lookup i Δ = Some (p, P) →
  IntoPersistent p P P' →
  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
  match envs_replace i p true (Esnoc Enil j P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_unseal=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
  destruct p; simpl; rewrite /bi_intuitionistically.
  - by rewrite -(into_persistent true P) /= wand_elim_r.
  - destruct HPQ.
    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
              (into_persistent _ P) wand_elim_r //.
    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
      by rewrite -{1}absorbingly_intuitionistically_into_persistently
        absorbingly_sep_l wand_elim_r HQ.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_spatial Δ i j p P P' Q :
  envs_lookup i Δ = Some (p, P) →
  (if p then FromAffinely P' P else TCEq P' P) →
  match envs_replace i p false (Esnoc Enil j P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ Q.
Proof.
  intros ? HP. destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
  rewrite envs_entails_unseal=> <-. rewrite envs_replace_singleton_sound //; simpl.
  destruct p; simpl; last destruct HP.
  - by rewrite intuitionistically_affinely (from_affinely P' P) wand_elim_r.
  - by rewrite wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
(* * Implication and wand *)
Lemma tac_impl_intro Δ i P P' Q R :
  FromImpl R P Q →
  (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
  FromAffinely P' P →
  match envs_app false (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ R.
Proof.
  destruct (envs_app _ _ _) eqn:?; last done.
  rewrite /FromImpl envs_entails_unseal => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
  - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
    rewrite envs_app_singleton_sound //; simpl.
    rewrite -(from_affinely P' P) -affinely_and_lr.
    by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
  - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
    by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
Qed.
(* iris/proofmode/coq_tactics.v *)
Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
  FromImpl R P Q →
  IntoPersistent false P P' →
  match envs_app true (Esnoc Enil i P') Δ with
  | None => False
  | Some Δ' => envs_entails Δ' Q
  end →
  envs_entails Δ R.
Proof.
  destruct (envs_app _ _ _) eqn:?; last done.
  rewrite /FromImpl envs_entails_unseal => <- ??.
  rewrite envs_app_singleton_sound //=. apply impl_intro_l.
  rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
  by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
Qed.