phanerozoic/Coq-Iris huggingface dataset:
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_alloc_strong N E t (I : gname → Prop) :
    pred_infinite I →
    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜I γ⌝ ∗ auth_ctx γ N f φ ∗ auth_own γ (f t).
Proof.
    iIntros (??) "Hφ". rewrite /auth_own /auth_ctx.
    iMod (own_alloc_strong (● f t ⋅ ◯ f t) I) as (γ) "[% [Hγ Hγ']]";
      [done|by apply auth_both_valid_discrete|].
    iMod (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
    { iNext. rewrite /auth_inv. iExists t. by iFrame. }
    eauto.
  Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_alloc_cofinite N E t (G : gset gname) :
    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, ⌜γ ∉ G⌝ ∗ auth_ctx γ N f φ ∗ auth_own γ (f t).
Proof.
    intros ?. apply auth_alloc_strong=>//.
    apply (pred_infinite_set (C:=gset gname)) => E'.
    exists (fresh (G ∪ E')). apply not_elem_of_union, is_fresh.
  Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_alloc N E t :
    ✓ (f t) → ▷ φ t ={E}=∗ ∃ γ, auth_ctx γ N f φ ∗ auth_own γ (f t).
Proof.
    iIntros (?) "Hφ".
    iMod (auth_alloc_cofinite N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
  Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_empty γ : ⊢ |==> auth_own γ ε.
Proof. by rewrite /auth_own -own_unit. Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_inv_acc E γ a :
    ▷ auth_inv γ f φ ∗ auth_own γ a ={E}=∗ ∃ t,
      ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
      ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E}=∗ ▷ auth_inv γ f φ ∗ auth_own γ b.
Proof using Type*.
    iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
    iDestruct "Hinv" as (t) "[>Hγa Hφ]".
    iModIntro. iExists t.
    iDestruct (own_valid_2 with "Hγa Hγf") as % [? ?]%auth_both_valid_discrete.
    iSplit; first done. iFrame "Hφ". iIntros (u b) "[% Hφ]".
    iMod (own_update_2 with "Hγa Hγf") as "[Hγa Hγf]".
    { eapply auth_update; eassumption. }
    by iFrame.
  Qed.
(* iris_deprecated/base_logic/auth.v *)
Lemma auth_acc E N γ a :
    ↑N ⊆ E →
    auth_ctx γ N f φ ∗ auth_own γ a ={E,E∖↑N}=∗ ∃ t,
      ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
      ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E∖↑N,E}=∗ auth_own γ b.
Proof using Type*.
    iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
    (* The following is essentially a very trivial composition of the accessors
       [auth_inv_acc] and [inv_acc] -- but since we don't have any good support
       for that currently, this gets more tedious than it should, with us having
       to unpack and repack various proofs.
       TODO: Make this mostly automatic, by supporting "opening accessors
       around accessors". *)
    iMod (auth_inv_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
    iModIntro. iExists t. iFrame. iIntros (u b) "H".
    iMod ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
  Qed.
(* iris_deprecated/base_logic/sts.v *)
(* The CMRA we need. *)
Class stsG Σ (sts : stsT)
:= StsG {
  #[local] sts_inG :: inG Σ (sts_resR sts);
  #[global] sts_inhabited :: Inhabited (sts.state sts);
}.
(* iris_deprecated/base_logic/sts.v *)
Definition stsΣ (sts : stsT) : gFunctors
:= #[ GFunctor (sts_resR sts) ].
(* iris_deprecated/base_logic/sts.v *)
Instance subG_stsΣ Σ sts :
  subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
Proof. solve_inG. Qed.
(* iris_deprecated/base_logic/sts.v *)
Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ
:=
    own γ (sts_frag S T).
(* iris_deprecated/base_logic/sts.v *)
Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iProp Σ
:=
    own γ (sts_frag_up s T).
(* iris_deprecated/base_logic/sts.v *)
Definition sts_inv (φ : sts.state sts → iProp Σ) : iProp Σ
:=
    ∃ s, own γ (sts_auth s ∅) ∗ φ s.
(* iris_deprecated/base_logic/sts.v *)
Definition sts_ctx `{!invGS Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ
:=
    inv N (sts_inv φ).
(* iris_deprecated/base_logic/sts.v *)
Instance sts_inv_ne n :
    Proper (pointwise_relation _ (dist n) ==> dist n) sts_inv.
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_inv_proper :
    Proper (pointwise_relation _ (≡) ==> (≡)) sts_inv.
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_ownS_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) sts_ownS.
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_own_proper s : Proper ((≡) ==> (⊣⊢)) (sts_own s).
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_ctx_ne `{!invGS Σ} n N :
    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_ctx_proper `{!invGS Σ} N :
    Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_ctx_persistent `{!invGS Σ} N φ : Persistent (sts_ctx N φ).
Proof. apply _. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_own_persistent s : Persistent (sts_own s ∅).
Proof. apply _. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance sts_ownS_persistent S : Persistent (sts_ownS S ∅).
Proof. apply _. Qed.
(* iris_deprecated/base_logic/sts.v *)
Instance : Params (@sts_inv) 4
:= {}.
(* iris_deprecated/base_logic/sts.v *)
Instance : Params (@sts_ownS) 4
:= {}.
(* iris_deprecated/base_logic/sts.v *)
Instance : Params (@sts_own) 5
:= {}.
(* iris_deprecated/base_logic/sts.v *)
Instance : Params (@sts_ctx) 6
:= {}.
(* iris_deprecated/base_logic/sts.v *)
(* The same rule as implication does *not* hold, as could be shown using
     sts_frag_included. *)
Lemma sts_ownS_weaken γ S1 S2 T1 T2 :
    T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
    sts_ownS γ S1 T1 ==∗ sts_ownS γ S2 T2.
Proof. intros ???. iApply own_update. by apply sts_update_frag. Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_own_weaken γ s S T1 T2 :
    T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
    sts_own γ s T1 ==∗ sts_ownS γ S T2.
Proof. intros ???. iApply own_update. by apply sts_update_frag_up. Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_own_weaken_state γ s1 s2 T :
    sts.frame_steps T s2 s1 → sts.tok s2 ## T →
    sts_own γ s1 T ==∗ sts_own γ s2 T.
Proof.
    intros ??. iApply own_update. apply sts_update_frag_up; [|done..].
    intros Hdisj. apply sts.closed_up. done.
  Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_own_weaken_tok γ s T1 T2 :
    T2 ⊆ T1 → sts_own γ s T1 ==∗ sts_own γ s T2.
Proof.
    intros ?. iApply own_update. apply sts_update_frag_up; last done.
    - intros. apply sts.closed_up. set_solver.
    - apply sts.elem_of_up.
  Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_ownS_op γ S1 S2 T1 T2 :
    T1 ## T2 → sts.closed S1 T1 → sts.closed S2 T2 →
    sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2).
Proof. intros. by rewrite /sts_ownS -own_op sts_frag_op. Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_own_op γ s T1 T2 :
    T1 ## T2 → sts_own γ s (T1 ∪ T2) ==∗ sts_own γ s T1 ∗ sts_own γ s T2.
(* The other direction does not hold -- see sts.up_op. *)
  Proof.
    intros. rewrite /sts_own -own_op. iIntros "Hown".
    iDestruct (own_valid with "Hown") as %Hval%sts_frag_up_valid.
    rewrite -sts_frag_op.
    - iApply (sts_own_weaken with "Hown"); first done.
      + split; apply sts.elem_of_up.
      + eapply sts.closed_op; apply sts.closed_up; set_solver.
    - done.
    - apply sts.closed_up; set_solver.
    - apply sts.closed_up; set_solver.
  Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_alloc φ E N s :
    ▷ φ s ={E}=∗ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
Proof.
    iIntros "Hφ". rewrite /sts_ctx /sts_own.
    iMod (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
    { apply sts_auth_valid; set_solver. }
    iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
    iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
    rewrite /sts_inv. iNext. iExists s. by iFrame.
  Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_inv_accS φ E γ S T :
    ▷ sts_inv γ φ ∗ sts_ownS γ S T ={E}=∗ ∃ s,
      ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
Proof.
    iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
    iDestruct "Hinv" as (s) "[>Hγ Hφ]".
    iDestruct (own_valid_2 with "Hγ Hγf") as %Hvalid.
    assert (s ∈ S) by eauto using sts_auth_frag_valid_inv.
    assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r.
    iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
    iIntros (s' T') "[% Hφ]".
    iMod (own_update_2 with "Hγ Hγf") as "Hγ".
    { rewrite sts_auth_frag_op; [|done..]. by apply sts_update_auth. }
    iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
    iModIntro. iNext. iExists s'; by iFrame.
  Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_inv_acc φ E γ s0 T :
    ▷ sts_inv γ φ ∗ sts_own γ s0 T ={E}=∗ ∃ s,
      ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E}=∗ ▷ sts_inv γ φ ∗ sts_own γ s' T'.
Proof. by apply sts_inv_accS. Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_accS φ E N γ S T :
    ↑N ⊆ E →
    sts_ctx γ N φ ∗ sts_ownS γ S T ={E,E∖↑N}=∗ ∃ s,
      ⌜s ∈ S⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
Proof.
    iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
    (* The following is essentially a very trivial composition of the accessors
       [sts_inv_acc] and [inv_acc] -- but since we don't have any good support
       for that currently, this gets more tedious than it should, with us having
       to unpack and repack various proofs.
       TODO: Make this mostly automatic, by supporting "opening accessors
       around accessors". *)
    iMod (sts_inv_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame.
    iModIntro. iExists s. iFrame. iIntros (s' T') "H".
    iMod ("HclSts" $! s' T' with "H") as "(Hinv & ?)". by iMod ("Hclose" with "Hinv").
  Qed.
(* iris_deprecated/base_logic/sts.v *)
Lemma sts_acc φ E N γ s0 T :
    ↑N ⊆ E →
    sts_ctx γ N φ ∗ sts_own γ s0 T ={E,E∖↑N}=∗ ∃ s,
      ⌜sts.frame_steps T s0 s⌝ ∗ ▷ φ s ∗ ∀ s' T',
      ⌜sts.steps (s, T) (s', T')⌝ ∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
Proof. by apply sts_accS. Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Definition vs `{!invGS Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ
:=
  □ (P -∗ |={E1,E2}=> Q).
(* iris_deprecated/base_logic/viewshifts.v *)
Instance : Params (@vs) 4
:= {}.
(* iris_deprecated/base_logic/viewshifts.v *)
Notation "P ={ E }=> Q"
:= (P ={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=>  Q") : bi_scope.
(* iris_deprecated/base_logic/viewshifts.v *)
Notation "P ={ E1 , E2 }=> Q"
:= (P ={E1,E2}=> Q)%I
  (at level 99, E1,E2 at level 50, Q at level 200,
   format "P  ={ E1 , E2 }=>  Q") : stdpp_scope.
(* iris_deprecated/base_logic/viewshifts.v *)
Notation "P ={ E }=> Q"
:= (P ={E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "P  ={ E }=>  Q") : stdpp_scope.
(* iris_deprecated/base_logic/viewshifts.v *)
Instance vs_ne E1 E2 : NonExpansive2 (vs E1 E2).
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (vs E1 E2).
Proof. apply ne_proper_2, _. Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_mono E1 E2 P P' Q Q' :
  (P ⊢ P') → (Q' ⊢ Q) → (P' ={E1,E2}=> Q') ⊢ P ={E1,E2}=> Q.
Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Instance vs_mono' E1 E2 : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (vs E1 E2).
Proof. solve_proper. Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_false_elim E1 E2 P : ⊢ False ={E1,E2}=> P.
Proof. iIntros "!> []". Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_timeless E P : Timeless P → ⊢ ▷ P ={E}=> P.
Proof. by iIntros (?) "!> > ?". Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_trans E1 E2 E3 P Q R :
  (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
Proof.
  iIntros "#[HvsP HvsQ] !> HP".
  iMod ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_reflexive E P : ⊢ P ={E}=> P.
Proof. by iIntros "!> HP". Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_impl E P Q : □ (P → Q) ⊢ P ={E}=> Q.
Proof. iIntros "#HPQ !> HP". by iApply "HPQ". Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ R ∗ P ={E1,E2}=> R ∗ Q.
Proof. iIntros "#Hvs !> [$ HP]". by iApply "Hvs". Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q ∗ R.
Proof. iIntros "#Hvs !> [HP $]". by iApply "Hvs". Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_mask_frame_r E1 E2 Ef P Q :
  E1 ## Ef → (P ={E1,E2}=> Q) ⊢ P ={E1 ∪ Ef,E2 ∪ Ef}=> Q.
Proof.
  iIntros (?) "#Hvs !> HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_inv N E P Q R :
  ↑N ⊆ E → inv N R ∗ (▷ R ∗ P ={E∖↑N}=> ▷ R ∗ Q) ⊢ P ={E}=> Q.
Proof.
  iIntros (?) "#[? Hvs] !> HP". iInv N as "HR" "Hclose".
  iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
  by iApply "Hclose".
Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_inv_acc N E P :
  ↑N ⊆ E →
  ⊢ inv N P ={E,E∖↑N}=> ▷ P ∗ ∃ R, R ∗ (R ∗ ▷ P ={E∖↑N,E}=> True).
Proof.
  (* FIXME: scope printing is weird, there are [%stdpp]. *)
  iIntros (?) "!> #Hinv".
  iMod (inv_acc with "Hinv") as "[$ Hclose]"; first done.
  iModIntro. iExists (▷ P ={E ∖ ↑N,E}=∗ True)%I. iFrame.
  iIntros "!> [Hclose HP]". iMod ("Hclose" with "HP"). done.
Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma vs_alloc N P : ⊢ ▷ P ={↑N}=> inv N P.
Proof. iIntros "!> HP". by iApply inv_alloc. Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
Proof.
  rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_affinely; last apply _.
  by rewrite bi.persistently_impl_wand.
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Definition ht `{!irisGS Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
    (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ
:=
  (□ (P -∗ WP e @ s; E {{ Φ }}))%I.
(* iris_deprecated/program_logic/hoare.v *)
Instance : Params (@ht) 5
:= {}.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e @ s ; E {{ Φ } }"
:= (ht s E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  s ;  E  {{  Φ  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e @ E {{ Φ } }"
:= (ht NotStuck E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e @ E ? {{ Φ } }"
:= (ht MaybeStuck E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e {{ Φ } }"
:= (ht NotStuck ⊤ P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e ? {{ Φ } }"
:= (ht MaybeStuck ⊤ P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  ? {{  Φ  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e @ s ; E {{ v , Q } }"
:= (ht s E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  s ;  E  {{  v ,  Q  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e @ E {{ v , Q } }"
:= (ht NotStuck E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e @ E ? {{ v , Q } }"
:= (ht MaybeStuck E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e {{ v , Q } }"
:= (ht NotStuck ⊤ P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Notation "{{ P } } e ? {{ v , Q } }"
:= (ht MaybeStuck ⊤ P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  ? {{  v ,  Q  } }") : stdpp_scope.
(* iris_deprecated/program_logic/hoare.v *)
Instance ht_ne s E n :
  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht s E).
Proof. solve_proper. Qed.
(* iris_deprecated/program_logic/hoare.v *)
Instance ht_proper s E :
  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht s E).
Proof. solve_proper. Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_mono s E P P' Φ Φ' e :
  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
Proof. by intros; apply affinely_mono, persistently_mono, wand_mono, wp_mono. Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_stuck_mono s1 s2 E P Φ e :
  s1 ⊑ s2 → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
Proof. by intros; apply affinely_mono, persistently_mono, wand_mono, wp_stuck_mono. Qed.
(* iris_deprecated/program_logic/hoare.v *)
Instance ht_mono' s E :
  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
Proof. solve_proper. Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_alt s E P Φ e : (P ⊢ WP e @ s; E {{ Φ }}) → ⊢ {{ P }} e @ s; E {{ Φ }}.
Proof. iIntros (Hwp) "!> HP". by iApply Hwp. Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_val s E v : ⊢ {{ True }} of_val v @ s; E {{ v', ⌜v = v'⌝ }}.
Proof. iIntros "!> _". by iApply wp_value'. Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_vs s E P P' Φ Φ' e :
  (P ={E}=> P') ∧ {{ P' }} e @ s; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
  ⊢ {{ P }} e @ s; E {{ Φ }}.
Proof.
  iIntros "(#Hvs & #Hwp & #HΦ) !> HP". iMod ("Hvs" with "HP") as "HP".
  iApply wp_fupd. iApply (wp_wand with "(Hwp HP)").
  iIntros (v) "Hv". by iApply "HΦ".
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity s) e} :
  (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
  ⊢ {{ P }} e @ s; E1 {{ Φ }}.
Proof.
  iIntros "(#Hvs & #Hwp & #HΦ) !> HP". iApply (wp_atomic _ _ E2); auto.
  iMod ("Hvs" with "HP") as "HP". iModIntro.
  iApply (wp_wand with "(Hwp HP)").
  iIntros (v) "Hv". by iApply "HΦ".
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_bind `{!LanguageCtx K} s E P Φ Φ' e :
  {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
  ⊢ {{ P }} K e @ s; E {{ Φ' }}.
Proof.
  iIntros "[#Hwpe #HwpK] !> HP". iApply wp_bind.
  iApply (wp_wand with "(Hwpe HP)").
  iIntros (v) "Hv". by iApply "HwpK".
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_stuck_weaken s E P Φ e :
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
Proof.
  by iIntros "#Hwp !> ?"; iApply wp_stuck_weaken; iApply "Hwp".
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_mask_weaken s E1 E2 P Φ e :
  E1 ⊆ E2 → {{ P }} e @ s; E1 {{ Φ }} ⊢ {{ P }} e @ s; E2 {{ Φ }}.
Proof.
  iIntros (?) "#Hwp !> HP". iApply (wp_mask_mono _ E1 E2); try done.
  by iApply "Hwp".
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_frame_l s E P Φ R e :
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
Proof. iIntros "#Hwp !> [$ HP]". by iApply "Hwp". Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_frame_r s E P Φ R e :
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ R }} e @ s; E {{ v, Φ v ∗ R }}.
Proof. iIntros "#Hwp !> [HP $]". by iApply "Hwp". Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_frame_step_l s E1 E2 P R1 R2 e Φ :
  TCEq (to_val e) None → E2 ⊆ E1 →
  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
  ⊢ {{ R1 ∗ P }} e @ s; E1 {{ λ v, R2 ∗ Φ v }}.
Proof.
  iIntros (??) "[#Hvs #Hwp] !> [HR HP]".
  iApply (wp_frame_step_l _ E1 E2); try done.
  iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_frame_step_r s E1 E2 P R1 R2 e Φ :
  TCEq (to_val e) None → E2 ⊆ E1 →
  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
  ⊢ {{ P ∗ R1 }} e @ s; E1 {{ λ v, Φ v ∗ R2 }}.
Proof.
  iIntros (??) "[#Hvs #Hwp] !> [HP HR]".
  iApply (wp_frame_step_r _ E1 E2); try done.
  iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_frame_step_l' s E P R e Φ :
  TCEq (to_val e) None →
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
Proof.
  iIntros (?) "#Hwp !> [HR HP]".
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_frame_step_r' s E P Φ R e :
  TCEq (to_val e) None →
  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ s; E {{ v, Φ v ∗ R }}.
Proof.
  iIntros (?) "#Hwp !> [HP HR]".
  iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Qed.
(* iris_deprecated/program_logic/hoare.v *)
Lemma ht_exists (T : Type) s E (P : T → iProp Σ) Φ e :
  (∀ x, {{ P x }} e @ s; E {{ Φ }}) ⊢ {{ ∃ x, P x }} e @ s; E {{ Φ }}.
Proof. iIntros "#HT !> HP". iDestruct "HP" as (x) "HP". by iApply "HT". Qed.
(* iris_heap_lang/adequacy.v *)
Class heapGpreS Σ
:= HeapGpreS {
  #[global] heapGpreS_iris :: invGpreS Σ;
  #[global] heapGpreS_heap :: gen_heapGpreS loc (option val) Σ;
  #[global] heapGpreS_inv_heap :: inv_heapGpreS loc (option val) Σ;
  #[global] heapGpreS_proph :: proph_mapGpreS proph_id (val * val) Σ;
  #[global] heapGS_step_cnt :: mono_natG Σ;
}.
(* iris_heap_lang/adequacy.v *)
Definition heapΣ : gFunctors
:=
  #[invΣ; gen_heapΣ loc (option val); inv_heapΣ loc (option val);
    proph_mapΣ proph_id (val * val); mono_natΣ].
(* iris_heap_lang/adequacy.v *)
Instance subG_heapGpreS {Σ} : subG heapΣ Σ → heapGpreS Σ.
Proof. solve_inG. Qed.
(* iris_heap_lang/adequacy.v *)
(* TODO: The [wp_adequacy] lemma is insufficient for a state interpretation
with a non-constant step index function. We thus use the more general
[wp_strong_adequacy] lemma. The proof below replicates part of the proof of
[wp_adequacy], and it hence would make sense to see if we can prove a version
of [wp_adequacy] for a non-constant step version. *)
Lemma heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
  adequate s e σ (λ v _, φ v).
Proof.
  intros Hwp.
  apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
  eapply (wp_strong_adequacy Σ _); [|done].
  iIntros (Hinv).
  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
  iMod (inv_heap_init loc (option val)) as (?) ">Hi".
  iMod (proph_map_init κs σ.(used_proph_id)) as (?) "[Hp _]".
  iMod (mono_nat_own_alloc) as (γ) "[Hsteps _]".
  iDestruct (Hwp (HeapGS _ _ _ _ _ _ _ _) with "Hi") as "Hwp".
  iModIntro.
  iExists (λ σ ns κs nt, (gen_heap_interp σ.(heap) ∗
                          proph_map_interp κs σ.(used_proph_id) ∗
                          γ ↪●MN ns))%I.
  iExists [(λ v, ⌜φ v⌝%I)], (λ _, True)%I, _ => /=.
  iFrame.
  iIntros (es' t2' -> ? ?) " _ H _".
  iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
  iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
  iDestruct (big_sepL2_nil_inv_r with "H") as %->.
  iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
Qed.
(* iris_heap_lang/class_instances.v *)
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
(* iris_heap_lang/class_instances.v *)
Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.
(* iris_heap_lang/class_instances.v *)
Ltac solve_atomic
:=
    apply strongly_atomic_atomic, ectx_language_atomic;
      [inversion 1; naive_solver
      |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
(* iris_heap_lang/class_instances.v *)
Instance rec_atomic s f x e : Atomic s (Rec f x e).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pair_atomic s v1 v2 : Atomic s (Pair (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance injl_atomic s v : Atomic s (InjL (Val v)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance injr_atomic s v : Atomic s (InjR (Val v)).
Proof. solve_atomic. Qed.