ReactorJet/Coq-Iris huggingface dataset:
(* iris/base_logic/bupd_alt.v *)
From iris.proofmode Require Import proofmode
From iris.base_logic Require Export base_logic
From iris.prelude Require Import options

Definition bupd_alt{PROP : bi} `{!Sbi PROP} (P : PROP) : PROP :=
  ∀ R, (P -∗ ■ R) -∗ ■ R.

Local CoercionuPred_holds : uPred >-> Funclass.

Notation bupd_alt:= (@bupd_alt PROP _).

Global Instancebupd_alt_ne : NonExpansive bupd_alt.
  Proof. solve_proper. Qed.

Global Instancebupd_alt_proper : Proper ((≡) ==> (≡)) bupd_alt.
  Proof. solve_proper. Qed.

Global Instancebupd_alt_mono' : Proper ((⊢) ==> (⊢)) bupd_alt.
  Proof. solve_proper. Qed.

Global Instancebupd_alt_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) bupd_alt.
  Proof. solve_proper. Qed.

Lemma bupd_alt_introP : P ⊢ bupd_alt P.
  Proof. iIntros "HP" (R) "H". by iApply "H". Qed.

Lemma bupd_alt_monoP Q : (P ⊢ Q) → bupd_alt P ⊢ bupd_alt Q.
  Proof. by intros ->. Qed.

Lemma bupd_alt_transP : bupd_alt (bupd_alt P) ⊢ bupd_alt P.
  Proof. iIntros "HP" (R) "H". iApply "HP". iIntros "HP". by iApply "HP". Qed.

Lemma bupd_alt_frame_rP Q : bupd_alt P ∗ Q ⊢ bupd_alt (P ∗ Q).
  Proof.
    iIntros "[HP HQ]" (R) "H". iApply "HP". iIntros "HP". iApply ("H" with "[$]").
  Qed.

Lemma bupd_alt_plainlyP : bupd_alt (■ P) ⊢ ■ P.
  Proof. iIntros "H". iApply ("H" $! P with "[]"); auto. Qed.

Lemma bupd_bupd_alt`{!BiBUpd PROP, !BiBUpdSbi PROP, !BiAffine PROP} P :
    (|==> P) ⊢ bupd_alt P.
  Proof. iIntros "HP" (R) "H". by iMod ("H" with "HP") as "?". Qed.

Lemma own_updatePx (Φ : M → Prop) :
    x ~~>: Φ → own x ⊢ bupd_alt (∃ y, ⌜Φ y⌝ ∧ own y).
  Proof.
    iIntros (Hup) "Hx"; iIntros (R) "H".
    iApply (own_updateP_plainly with "[$Hx H]"); first done.
    iIntros (y ?) "Hy". iApply "H"; auto.
  Qed.

Lemma bupd_alt_bupd{M} (P : uPred M) : bupd_alt P ⊢ |==> P.
Proof.
  rewrite /bupd_alt /plainly. uPred.unseal; split=> n x Hx H k y ? Hxy.
  unshelve refine (H {| uPred_holds k _ :=
    ∃ x' : M, ✓{k} (x' ⋅ y) ∧ P k x' |} k y _ _ _).
  - intros n1 n2 x1 x2 (z&?&?) _ ?.
    eauto using cmra_validN_le, uPred_mono.
  - done.
  - done.
  - intros k' z ?? HP. exists z. by rewrite (comm op).
Qed.

Lemma bupd_alt_bupd_iff{M} (P : uPred M) : bupd_alt P ⊣⊢ |==> P.
Proof.
  apply (anti_symm _).
  - apply bupd_alt_bupd.
  - apply bupd_bupd_alt.
Qed.

Lemma ownM_updateP{M : ucmra} x (Φ : M → Prop) (R : uPred M) :
  x ~~>: Φ →
  uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.
Proof.
  intros Hup. rewrite /plainly. uPred.unseal.
  split. intros n z Hv (?&z2&?&[z1 ?]&HR); ofe_subst.
  destruct (Hup n (Some (z1 ⋅ z2))) as (y&?&?); simpl in *.
  { by rewrite assoc. }
  refine (HR y n z1 _ _ _ n y _ _ _); auto.
  - rewrite comm. by eapply cmra_validN_op_r.
  - by rewrite (comm _ _ y) (comm _ z2).
  - apply (reflexivity (R:=includedN _)).
Qed.
(* iris/base_logic/derived.v *)
From iris.algebra Require Import frac
From iris.bi Require Export bi
From iris.base_logic Require Export bi
From iris.prelude Require Import options

Global InstanceownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.

Lemma intuitionistically_ownM(a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
  Proof.
    rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
      [by rewrite persistently_elim|].
    by rewrite {1}persistently_ownM_core core_id_core.
  Qed.

Lemma ownM_invalid(a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
  Proof.
    intros. rewrite ownM_valid internal_cmra_valid_elim. by apply pure_elim'.
  Qed.

Global InstanceownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
  Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.

Lemma ownM_unit': uPred_ownM ε ⊣⊢ True.
  Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.

Lemma bupd_ownM_updatex y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
  Proof.
    intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
    by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
  Qed.

Global InstanceownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
  Proof.
    intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
    rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
    apply except_0_mono. rewrite internal_eq_sym.
    apply (internal_eq_rewrite' b a (uPred_ownM) _);
      [solve_proper|auto using and_elim_l, and_elim_r..].
  Qed.

Global InstanceownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
  Proof.
    intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
  Qed.

Global InstanceuPred_ownM_sep_homomorphism :
    MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
  Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.

Lemma bupd_soundnessP `{!Plain P} : (⊢ |==> P) → ⊢ P.
  Proof. rewrite bupd_elim. done. Qed.

Inductive modality:= MBUpd | MLater | MPersistently | MPlainly.

Definition denote_modality(m : modality) : uPred M → uPred M :=
    match m with
    | MBUpd => bupd
    | MLater => bi_later
    | MPersistently => bi_persistently
    | MPlainly => plainly
    end.

Definition denote_modalities(ms : list modality) : uPred M → uPred M :=
    λ P, foldr denote_modality P ms.
(* iris/base_logic/proofmode.v *)
From iris.algebra Require Import proofmode_classes
From iris.proofmode Require Import classes
From iris.base_logic Require Export derived
From iris.prelude Require Import options
FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2)
FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2)

Global Instancefrom_sep_ownM (a b1 b2 : M) :
    IsOp a b1 b2 →
    FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
  Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.

Global Instancecombine_sep_as_ownM (a b1 b2 : M) :
    IsOp a b1 b2 →
    CombineSepAs (uPred_ownM b1) (uPred_ownM b2) (uPred_ownM a) | 60.
  Proof. intros. by rewrite /CombineSepAs -ownM_op -is_op. Qed.

Global Instancecombine_sep_gives_ownM (b1 b2 : M) :
    CombineSepGives (uPred_ownM b1) (uPred_ownM b2) (✓ (b1 ⋅ b2)).
  Proof.
    intros. rewrite /CombineSepGives -ownM_op ownM_valid.
    by apply: bi.persistently_intro.
  Qed.

Global Instancefrom_sep_ownM_core_id (a b1 b2 : M) :
    IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
    FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
  Proof.
    intros ? H. rewrite /FromAnd (is_op a) ownM_op.
    destruct H; by rewrite bi.persistent_and_sep.
  Qed.

Global Instanceinto_and_ownM p (a b1 b2 : M) :
    IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
  Proof.
    intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
  Qed.

Global Instanceinto_sep_ownM (a b1 b2 : M) :
    IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
  Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
(* iris/bi/extensions.v *)
From iris.bi Require Export derived_connectives
From iris.prelude Require Import options

Class BiAffine(PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.

Global HintMode BiAffine ! : typeclass_instances.

Global ExistingInstance absorbing_bi | 0.

Class BiPositive(PROP : bi) :=
  bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.

Global HintMode BiPositive ! : typeclass_instances.

Class BiLöb(PROP : bi) :=
  löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).

Global HintMode BiLöb ! : typeclass_instances.

Global Argumentslöb_weak {_ _} _ _.

Class BiLaterContractive(PROP : bi) :=
  #[global] later_contractive :: Contractive (bi_later (PROP:=PROP)).

Class BiPersistentlyForall(PROP : bi) :=
  persistently_forall_2 : ∀ {A} (Ψ : A → PROP), (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).

Global HintMode BiPersistentlyForall ! : typeclass_instances.

Class BiPureForall(PROP : bi) :=
  pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.

Global HintMode BiPureForall ! : typeclass_instances.
(* iris/bi/weakestpre.v *)
From stdpp Require Export coPset
From iris.bi Require Import interface derived_connectives
From iris.prelude Require Import options

Inductive stuckness:= NotStuck | MaybeStuck.

Global Instancestuckness_le : SqSubsetEq stuckness := λ s1 s2,
  match s1, s2 with
  | MaybeStuck, NotStuck => False
  | _, _ => True
  end.

Global Instancestuckness_le_po : PreOrder (⊑@{stuckness}).
Proof. split; by repeat intros []. Qed.

Class Wp(PROP EXPR VAL A : Type) :=
  wp : A → coPset → EXPR → (VAL → PROP) → PROP.

Global Argumentswp {_ _ _ _ _} _ _ _%_E _%_I.

Global Instance: Params (@wp) 8 := {}.

Class Twp(PROP EXPR VAL A : Type) :=
  twp : A → coPset → EXPR → (VAL → PROP) → PROP.

Global Argumentstwp {_ _ _ _ _} _ _ _%_E _%_I.

Global Instance: Params (@twp) 8 := {}.
(* iris/prelude/prelude.v *)
From stdpp Require Export ssreflect
From iris.prelude Require Import options

Coercion Z.of_nat : nat >-> Z.
(* iris/program_logic/total_ectx_lifting.v *)
From iris.proofmode Require Import proofmode
From iris.program_logic Require Export ectx_language total_weakestpre total_lifting
From iris.prelude Require Import options

Local HintResolve base_prim_reducible_no_obs base_reducible_prim_step
  base_reducible_no_obs_reducible : core.

Lemma twp_lift_base_step{s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E,∅}=∗
    ⌜base_reducible_no_obs e1 σ1⌝ ∗
    ∀ κ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
      ⌜κ = []⌝ ∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E [{ Φ }] ∗
      [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H".
  iApply (twp_lift_step _ E)=>//. iIntros (σ1 ns κs nt) "Hσ".
  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
  iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs Hstep).
  iApply "H". by eauto.
Qed.

Lemma twp_lift_pure_base_step_no_fork{s E Φ} e1 :
  (∀ σ1, base_reducible_no_obs e1 σ1) →
  (∀ σ1 κ e2 σ2 efs, base_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
  (|={E}=> ∀ κ e2 efs σ, ⌜base_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }] )
  ⊢ WP e1 @ s; E [{ Φ }].
Proof using Hinh.
  iIntros (??) ">H". iApply twp_lift_pure_step_no_fork; eauto.
  iIntros "!>" (?????). iApply "H"; eauto.
Qed.

Lemma twp_lift_atomic_base_step{s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
    ⌜base_reducible_no_obs e1 σ1⌝ ∗
    ∀ κ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
      ⌜κ = []⌝ ∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      from_option Φ False (to_val e2) ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
  iIntros (σ1 ns κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs Hstep). iApply "H"; eauto.
Qed.

Lemma twp_lift_atomic_base_step_no_fork{s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
    ⌜base_reducible_no_obs e1 σ1⌝ ∗
    ∀ κ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
      ⌜κ = []⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt
                            ∗ from_option Φ False (to_val e2))
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H". iApply twp_lift_atomic_base_step; eauto.
  iIntros (σ1 ns κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iIntros (κ v2 σ2 efs Hstep).
  iMod ("H" with "[# //]") as "(-> & -> & ? & $) /=". by iFrame.
Qed.

Lemma twp_lift_pure_det_base_step_no_fork{s E Φ} e1 e2 :
  to_val e1 = None →
  (∀ σ1, base_reducible_no_obs e1 σ1) →
  (∀ σ1 κ e2' σ2 efs',
    base_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
  WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
Proof using Hinh.
  intros. rewrite -(twp_lift_pure_det_step_no_fork e1 e2); eauto.
Qed.
(* iris/program_logic/total_lifting.v *)
From iris.bi Require Export big_op
From iris.proofmode Require Import proofmode
From iris.program_logic Require Export total_weakestpre
From iris.prelude Require Import options

Local HintResolve reducible_no_obs_reducible : core.

Lemma twp_lift_steps E Φ e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E,∅}=∗
    ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
      ⌜κ = []⌝ ∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E [{ Φ }] ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
  ⊢ WP e1 @ s; E [{ Φ }].
Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.

Lemma twp_lift_pure_step_no_fork`{!Inhabited (state Λ)} s E Φ e1 :
  (∀ σ1, reducible_no_obs e1 σ1) →
  (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
  (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }])
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (Hsafe Hstep) ">H". iApply twp_lift_step.
  { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
  iIntros (σ1 ns κs n) "Hσ".
  iApply fupd_mask_intro; first by set_solver. iIntros "Hclose". iSplit.
  { iPureIntro. destruct s; auto. }
  iIntros (κ e2 σ2 efs ?). destruct (Hstep σ1 κ e2 σ2 efs) as (->&<-&->); auto.
  iMod (state_interp_mono with "Hσ"). iMod "Hclose" as "_".
  iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
Qed.

Lemma twp_lift_atomic_step{s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
    ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
      ⌜κ = []⌝ ∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      from_option Φ False (to_val e2) ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H".
  iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 ns κs nt) "Hσ1".
  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
  iApply fupd_mask_intro; first set_solver.
  iIntros "Hclose" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
  iMod ("H" $! κ e2 σ2 efs with "[#]") as "($ & $ & HΦ & $)"; first by eauto.
  destruct (to_val e2) eqn:?; last by iExFalso.
  iApply twp_value; last done. by apply of_to_val.
Qed.

Lemma twp_lift_pure_det_step_no_fork`{!Inhabited (state Λ)} {s E Φ} e1 e2 :
  (∀ σ1, reducible_no_obs e1 σ1) →
  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
    κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
  (|={E}=> WP e2 @ s; E [{ Φ }]) ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step_no_fork s E); try done.
  { naive_solver. }
  iIntros "!>" (κ' e' efs' σ (_&_&->&->)%Hpuredet); auto.
Qed.

Lemma twp_pure_step`{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
  PureExec φ n e1 e2 →
  φ →
  WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?] ? IH]; simpl; first done.
  iApply twp_lift_pure_det_step_no_fork; [done|naive_solver|].
  iModIntro. by iApply "IH".
Qed.
(* iris/proofmode/class_instances_cmra.v *)
From iris.proofmode Require Import modality_instances classes
From iris.prelude Require Import options
FromExist (PROP:=PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I

Global Instanceinto_pure_internal_cmra_valid `{!CmraDiscrete A} (a : A) :
    @IntoPure PROP (✓ a) (✓ a).
  Proof. by rewrite /IntoPure internal_cmra_valid_discrete. Qed.

Global Instancefrom_pure_internal_cmra_valid {A : cmra} (a : A) :
    @FromPure PROP false (✓ a) (✓ a).
  Proof.
    rewrite /FromPure /=. apply bi.pure_elim'=> ?.
    rewrite -internal_cmra_valid_intro //.
  Qed.

Global Instanceinto_pure_internal_included {A : cmra} (a b : A) `{!Discrete b} :
    @IntoPure PROP (a ≼ b) (a ≼ b).
  Proof. by rewrite /IntoPure internal_included_discrete. Qed.

Global Instancefrom_pure_internal_included {A : cmra} (a b : A) :
    @FromPure PROP false (a ≼ b) (a ≼ b).
  Proof.
    rewrite /FromPure /=. apply bi.pure_elim'=> ?.
    rewrite -internal_included_intro //.
  Qed.

Global Instanceinto_exist_internal_included {A : cmra} (a b : A) :
    IntoExist (PROP:=PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I (λ x, x).
  Proof. by rewrite /IntoExist. Qed.

Global Instancefrom_exist_internal_included {A : cmra} (a b : A) :
    FromExist (PROP:=PROP) (a ≼ b) (λ c, b ≡ a ⋅ c)%I.
  Proof. by rewrite /FromExist. Qed.
(* iris/proofmode/class_instances_internal_eq.v *)
From stdpp Require Import nat_cancel
From iris.proofmode Require Import modality_instances classes
From iris.prelude Require Import options
FromModal (PROP1:=PROP) (PROP2:=PROP) True (modality_laterN 1)

Global Instancefrom_pure_internal_eq {A : ofe} (a b : A) :
  @FromPure PROP false (a ≡ b) (a ≡ b).
Proof. by rewrite /FromPure pure_internal_eq. Qed.

Global Instanceinto_pure_eq {A : ofe} (a b : A) (P : Prop) :
  TCOr (Discrete a) (Discrete b) →
  TCOr (TCAnd (LeibnizEquiv A) (TCEq P (a = b)))
       (TCEq P (a ≡ b)) →
  @IntoPure PROP (a ≡ b) P.
Proof.
  move=> ? [[? ->]|->]; rewrite /IntoPure discrete_eq; last done.
  by rewrite leibniz_equiv_iff.
Qed.

Global Instancefrom_modal_Next {A : ofe} (x y : A) :
  FromModal (PROP1:=PROP) (PROP2:=PROP) True (modality_laterN 1)
    (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
Proof. by rewrite /FromModal /= later_equivI. Qed.

Global Instanceinto_laterN_Next {A : ofe} only_head n n' (x y : A) :
  NatCancel n 1 n' 0 →
  IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
Proof.
  rewrite /IntoLaterN /MaybeIntoLaterN /NatCancel Nat.add_0_r.
  move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
Qed.

Global Instanceinto_internal_eq_internal_eq {A : ofe} (x y : A) :
  @IntoInternalEq PROP _ A (x ≡ y) x y.
Proof. by rewrite /IntoInternalEq. Qed.

Global Instanceinto_internal_eq_affinely {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.

Global Instanceinto_internal_eq_intuitionistically {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (□ P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.

Global Instanceinto_internal_eq_absorbingly {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.

Global Instanceinto_internal_eq_plainly `{!BiPlainly PROP} {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (■ P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.

Global Instanceinto_internal_eq_persistently {A : ofe} (x y : A) P :
  IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
(* iris/proofmode/ident_name.v *)
From stdpp Require Import base
From iris.prelude Require Import options

Definition ident_name:= unit → unit.

Ltac to_ident_nameid :=
  eval cbv in (ltac:(clear; intros id; assumption) : unit → unit).

Notation to_ident_nameid := (λ id:unit, id) (only parsing).

Class AsIdentName{A B} (f : A → B) (name : ident_name) := as_ident_name {}.

Global Argumentsas_ident_name {A B f} name : assert.

Ltac solve_as_ident_name:=
  lazymatch goal with

Global HintExtern 1 (AsIdentName _ _) => solve_as_ident_name : typeclass_instances.
(* iris/proofmode/modality_instances.v *)
From iris.bi Require Import bi
From iris.proofmode Require Export classes
From iris.prelude Require Import options

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.

Definition modality_persistently:=
    Modality _ modality_persistently_mixin.

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.

Definition modality_affinely:=
    Modality _ modality_affinely_mixin.

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.

Definition modality_intuitionistically:=
    Modality _ modality_intuitionistically_mixin.

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.

Definition modality_embed`{!BiEmbed PROP PROP'} :=
    Modality _ modality_embed_mixin.

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.

Definition modality_plainly`{!Sbi PROP} :=
    Modality _ modality_plainly_mixin.

Lemma modality_laterN_mixinn :
    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.

Definition modality_laterNn :=
    Modality _ (modality_laterN_mixin n).
(* iris/proofmode/notation.v *)
From stdpp Require Export strings
From iris.proofmode Require Import coq_tactics environments
From iris.prelude Require Import options

Global ArgumentsEnvs _ _%_proof_scope _%_proof_scope _.

Global ArgumentsEnil {_}.

Global ArgumentsEsnoc {_} _%_proof_scope _%_string _%_I.
(* iris/proofmode/reduction.v *)
From iris.bi Require Import bi telescopes
From iris.proofmode Require Import base environments
From iris.prelude Require Import options

Ltac pm_evalt :=
  eval pm_eval in t.

Ltac pm_reduce:=

Ltac pm_reflexivity:= pm_reduce; exact eq_refl.

Ltac pm_prettify:=
(* iris/proofmode/sel_patterns.v *)
From stdpp Require Export strings
From iris.proofmode Require Import base tokens
From iris.prelude Require Import options

Inductive sel_pat:=
  | SelPure
  | SelIntuitionistic
  | SelSpatial
  | SelIdent : ident → sel_pat.

Fixpoint sel_pat_pure(ps : list sel_pat) : bool :=
  match ps with
  | [] => false
  | SelPure :: ps => true
  | _ :: ps => sel_pat_pure ps
  end.

Fixpoint parse_go(ts : list token) (k : list sel_pat) : option (list sel_pat) :=
  match ts with
  | [] => Some (reverse k)
  | TName s :: ts => parse_go ts (SelIdent s :: k)
  | TPure None :: ts => parse_go ts (SelPure :: k)
  | TIntuitionistic :: ts => parse_go ts (SelIntuitionistic :: k)
  | TSep :: ts => parse_go ts (SelSpatial :: k)
  | _ => None
  end.

Definition parse(s : string) : option (list sel_pat) :=
  parse_go (tokenize s) [].

Ltac parses :=
  lazymatch type of s with
  | sel_pat => constr:([s])
  | list sel_pat => s
  | ident => constr:([SelIdent s])
  | list ident => eval vm_compute in (SelIdent <$> s)
  | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
  | string =>
     lazymatch eval vm_compute in (parse s) with
     | Some ?pats => pats
     | _ => fail "sel_pat.parse: cannot parse" s "as a selection pattern"
     end
  | ?X => fail "sel_pat.parse: the term" s
     "is expected to be a selection pattern"
     "(usually a string),"
     "but has unexpected type" X
  end.