phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/primitive_laws.v *)
Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
  v' ≠ v1 → vals_compare_safe v' v1 →
  [[{ l ↦{dq} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  [[{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }]].
Proof.
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
  iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto with base_step.
  iIntros (κ v2' σ2 efs Hstep); inv_base_step.
  rewrite bool_decide_false //.
  iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
  iModIntro; iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_cmpxchg_fail s E l dq v' v1 v2 :
  v' ≠ v1 → vals_compare_safe v' v1 →
  {{{ ▷ l ↦{dq} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' }}}.
Proof.
  iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_fail with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_cmpxchg_fail_lc s E l dq v' v1 v2 n :
  v' ≠ v1 → vals_compare_safe v' v1 →
  {{{ steps_lb n ∗ ▷ l ↦{dq} v' }}}
    CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET PairV v' (LitV $ LitBool false); l ↦{dq} v' ∗ £ (S n) }}}.
Proof.
  iIntros (?? Φ) "[#? >H] HΦ". iApply (twp_wp_step_lc_texan with "[$] HΦ").
  iApply (twp_cmpxchg_fail with "H"); [by auto..|]; iIntros "H HΦ ? !>".
  iApply "HΦ"; iFrame.
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma twp_cmpxchg_suc s E l v1 v2 v' :
  v' = v1 → vals_compare_safe v' v1 →
  [[{ l ↦ v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  [[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]].
Proof.
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
  iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto with base_step.
  iIntros (κ v2' σ2 efs Hstep); inv_base_step.
  rewrite bool_decide_true //.
  iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
  iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_cmpxchg_suc s E l v1 v2 v' :
  v' = v1 → vals_compare_safe v' v1 →
  {{{ ▷ l ↦ v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }}}.
Proof.
  iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_suc with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_cmpxchg_suc_lc s E l v1 v2 v' n :
  v' = v1 → vals_compare_safe v' v1 →
  {{{ steps_lb n ∗ ▷ l ↦ v' }}}
    CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
  {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 ∗ £ (S n) }}}.
Proof.
  iIntros (?? Φ) "[#? >H] HΦ". iApply (twp_wp_step_lc_texan with "[$] HΦ").
  iApply (twp_cmpxchg_suc with "H"); [by auto..|]; iIntros "H HΦ ? !>".
  iApply "HΦ"; iFrame.
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma twp_faa s E l i1 i2 :
  [[{ l ↦ LitV (LitInt i1) }]]
    FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
  [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
  iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto with base_step.
  iIntros (κ e2 σ2 efs Hstep); inv_base_step.
  iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
  iModIntro. do 2 (iSplit; first done). iFrame. by iApply "HΦ".
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_faa s E l i1 i2 :
  {{{ ▷ l ↦ LitV (LitInt i1) }}}
    FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
  {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }}}.
Proof.
  iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_faa with "H"); [by auto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_faa_lc s E l i1 i2 n :
  {{{ steps_lb n ∗ ▷ l ↦ LitV (LitInt i1) }}}
    FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
  {{{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) ∗ £ (S n) }}}.
Proof.
  iIntros (Φ) "[#? >H] HΦ". iApply (twp_wp_step_lc_texan with "[$] HΦ").
  iApply (twp_faa with "H"); [by auto..|]; iIntros "H HΦ ? !>".
  iApply "HΦ"; iFrame.
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_new_proph s E :
  {{{ True }}}
    NewProph @ s; E
  {{{ pvs p, RET (LitV (LitProphecy p)); proph p pvs }}}.
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_base_step_no_fork; first done.
  iIntros (σ1 ns κ κs nt) "(Hσ & HR & Hsteps) !>". iSplit; first by eauto with base_step.
  iIntros "!>" (v2 σ2 efs Hstep) "_". inv_base_step.
  rename select proph_id into p.
  iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit; first done. iFrame. by iApply "HΦ".
Qed.
(* iris_heap_lang/primitive_laws.v *)
(* In the following, strong atomicity is required due to the fact that [e] must
be able to make a base step for [Resolve e _ _] not to be (base) stuck. *)
Lemma resolve_reducible e σ (p : proph_id) v :
  Atomic StronglyAtomic e → reducible e σ →
  p ∈ σ.(used_proph_id) →
  reducible (Resolve e (Val (LitV (LitProphecy p))) (Val v)) σ.
Proof.
  intros A (κ & e' & σ' & efs & H) Hin.
  exists (κ ++ [(p, (default v (to_val e'), v))]), e', σ', efs.
  eapply (Ectx_step []); try done.
  assert (∃w, Val w = e') as [w <-].
  { unfold Atomic in A. apply (A σ e' κ σ' efs) in H. unfold is_Some in H.
    destruct H as [w H]. exists w. simpl in H. by apply (of_to_val _ _ H). }
  simpl. constructor; last done. by apply prim_step_to_val_is_base_step.
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma step_resolve e vp vt σ1 κ e2 σ2 efs :
  Atomic StronglyAtomic e →
  prim_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs →
  base_step (Resolve e (Val vp) (Val vt)) σ1 κ e2 σ2 efs.
Proof.
  intros A [Ks e1' e2' Hfill -> step]. simpl in *.
  induction Ks as [|K Ks _] using rev_ind.
  + simpl in *. subst. inv_base_step. by constructor.
  + rewrite fill_app /= in Hfill. destruct K; inversion Hfill; subst; clear Hfill.
    - rename select ectx_item into Ki.
      assert (fill_item Ki (fill Ks e1') = fill (Ks ++ [Ki]) e1') as Eq1;
        first by rewrite fill_app.
      assert (fill_item Ki (fill Ks e2') = fill (Ks ++ [Ki]) e2') as Eq2;
        first by rewrite fill_app.
      rewrite fill_app /=. rewrite Eq1 in A.
      assert (is_Some (to_val (fill (Ks ++ [Ki]) e2'))) as H.
      { apply (A σ1 _ κ σ2 efs). eapply (Ectx_step (Ks ++ [Ki])); done. }
      destruct H as [v H]. apply to_val_fill_some in H. by destruct H, Ks.
    - rename select (of_val vp = _) into Hvp.
      assert (to_val (fill Ks e1') = Some vp) as Hfillvp by rewrite -Hvp //.
      apply to_val_fill_some in Hfillvp as [-> ->]. inv_base_step.
    - rename select (of_val vt = _) into Hvt.
      assert (to_val (fill Ks e1') = Some vt) as Hfillvt by rewrite -Hvt //.
      apply to_val_fill_some in Hfillvt as [-> ->]. inv_base_step.
Qed.
(* iris_heap_lang/primitive_laws.v *)
Lemma wp_resolve_strong s E e Φ (p : proph_id) v (pvs : list (val * val)) :
  Atomic StronglyAtomic e →
  to_val e = None →
  proph p pvs -∗
  (proph p pvs -∗ WP e @ s; E {{ r, ∃ pvs', proph p pvs' ∗
      ∀ pvs'', ⌜pvs' = (r, v)::pvs''⌝ -∗ proph p pvs'' -∗ Φ r }}) -∗
  WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
Proof.
  (* TODO we should try to use a generic lifting lemma (and avoid [wp_unfold])
     here, since this breaks the WP abstraction. *)
  iIntros (A He) "Hp WPe". rewrite !wp_unfold /wp_pre /= He. simpl in *.
  iIntros (σ1 ns κ κs nt) "(Hσ & Hκ & Hsteps)".
  iPoseProof (proph_map_agree with "Hκ Hp") as "[%Hin #_]".
  iSpecialize ("WPe" with "Hp").
  destruct κ as [|[p' [w' v']] κ' _] using rev_ind.
  - iMod ("WPe" $! σ1 ns [] κs nt with "[$Hσ $Hκ $Hsteps]") as "[Hs WPe]".
    iModIntro. iSplit.
    { iDestruct "Hs" as "%". iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
    iIntros (e2 σ2 efs step). exfalso. apply step_resolve in step; last done.
    inv_base_step. match goal with H: ?κs ++ [_] = [] |- _ => by destruct κs end.
  - rewrite -assoc.
    iMod ("WPe" $! σ1 ns _ _ nt with "[$Hσ $Hκ $Hsteps]") as "[Hs WPe]". iModIntro. iSplit.
    { iDestruct "Hs" as %?. iPureIntro. destruct s; [ by apply resolve_reducible | done]. }
    iIntros (e2 σ2 efs step) "Hcred". apply step_resolve in step; last done.
    inv_base_step; simplify_list_eq.
    iMod ("WPe" $! (Val w') σ2 efs with "[%] Hcred") as "WPe".
    { by eexists [] _ _. }
    iModIntro. iNext. iMod "WPe" as "WPe". iModIntro.
    iApply (step_fupdN_wand with "WPe"); iIntros "> [($ & Hκ & $) WPe]".
    rewrite !wp_unfold /wp_pre /=. iDestruct "WPe" as "[>(%pvs' & Hp & HΦ) $]".
    iMod (proph_map_resolve_proph p' (w',v') κs with "[$Hκ $Hp]") as (vs' ->) "[$ Hp]".
    do 2 iModIntro. iApply ("HΦ" with "[//] Hp").
Qed.
(* iris_heap_lang/primitive_laws.v *)
(* A variant of [wp_resolve_strong] where [proph] ownership is not available
   inside [e]. Almost all the time, this is sufficient. *)
Lemma wp_resolve s E e Φ (p : proph_id) v (pvs : list (val * val)) :
  Atomic StronglyAtomic e →
  to_val e = None →
  proph p pvs -∗
  WP e @ s; E {{ r, ∀ pvs', ⌜pvs = (r, v)::pvs'⌝ -∗ proph p pvs' -∗ Φ r }} -∗
  WP Resolve e (Val $ LitV $ LitProphecy p) (Val v) @ s; E {{ Φ }}.
Proof.
  iIntros (??) "Hp WPe".
  iApply (wp_resolve_strong with "Hp"); first done.
  iIntros "Hp". iApply (wp_wand with "WPe").
  iIntros (?) "$ //".
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_expr_eval `{!heapGS_gen hlc Σ} Δ s E Φ e e' :
  (∀ (e'':=e'), e = e'') →
  envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_expr_eval `{!heapGS_gen hlc Σ} Δ s E Φ e e' :
  (∀ (e'':=e'), e = e'') →
  envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. by intros ->. Qed.
(* iris_heap_lang/proofmode.v *)
Ltac wp_expr_simpl
:= wp_expr_eval simpl.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_pure `{!heapGS_gen hlc Σ} Δ Δ' s E K e1 e2 φ n Φ :
  PureExec φ n e1 e2 →
  φ →
  MaybeIntoLaterNEnvs n Δ Δ' →
  envs_entails Δ' (WP (fill K e2) @ s; E {{ Φ }}) →
  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ??? HΔ'. rewrite into_laterN_env_sound /=.
  (* We want [pure_exec_fill] to be available to TC search locally. *)
  pose proof @pure_exec_fill.
  rewrite HΔ' -lifting.wp_pure_step_later //.
  iIntros "Hwp !> _" => //.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_pure `{!heapGS_gen hlc Σ} Δ s E K e1 e2 φ n Φ :
  PureExec φ n e1 e2 →
  φ →
  envs_entails Δ (WP (fill K e2) @ s; E [{ Φ }]) →
  envs_entails Δ (WP (fill K e1) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=> ?? ->.
  (* We want [pure_exec_fill] to be available to TC search locally. *)
  pose proof @pure_exec_fill.
  rewrite -total_lifting.twp_pure_step //.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_pure_credit `{!heapGS_gen hlc Σ} Δ Δ' s E j K e1 e2 ϕ Φ :
  PureExec ϕ 1 e1 e2 →
  ϕ →
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  match envs_lookup j Δ' with
  | Some (false, P) =>
    ∃ n,
      P = (£ n) ∧
      match envs_simple_replace j false (Esnoc Enil j (£ (S n))) Δ' with
      | Some Δ'' => envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
      | None => False
      end
  | None =>
     match envs_app false (Esnoc Enil j (£ 1)) Δ' with
     | Some Δ'' => envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
     | None => False
     end
  | _ => False
  end →
  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ??? HΔ.
  pose proof @pure_exec_fill.
  rewrite -lifting.wp_pure_step_later; last done.
  rewrite into_laterN_env_sound /=. apply later_mono.
  destruct (envs_lookup j Δ') as [[[] P]|] eqn:Hj; first done.
  - destruct HΔ as (n & -> & HΔ).
    destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ'; last done.
    rewrite envs_simple_replace_sound //; simpl.
    rewrite right_id. apply wand_intro_r.
    rewrite sep_comm assoc -lc_succ wand_elim_r.
    apply HΔ.
  - destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; last done.
    rewrite envs_app_sound //; simpl.
    rewrite right_id. apply wand_intro_r. by rewrite wand_elim_l.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_value_nofupd `{!heapGS_gen hlc Σ} Δ s E Φ v :
  envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_unseal=> ->. by apply wp_value. Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_value_nofupd `{!heapGS_gen hlc Σ} Δ s E Φ v :
  envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_unseal=> ->. by apply twp_value. Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_value `{!heapGS_gen hlc Σ} Δ s E (Φ : val → iPropI Σ) v :
  envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_unseal=> ->. by rewrite wp_value_fupd. Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_value `{!heapGS_gen hlc Σ} Δ s E (Φ : val → iPropI Σ) v :
  envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_unseal=> ->. by rewrite twp_value_fupd. Qed.
(* iris_heap_lang/proofmode.v *)
(* Simplify the goal if it is [WP] of a value.
  If the postcondition already allows a fupd, do not add a second one.
  But otherwise, *do* add a fupd. This ensures that all the lemmas applied
  here are bidirectional, so we never will make a goal unprovable. *)
Ltac wp_value_head
:=
  lazymatch goal with
  | |- envs_entails _ (wp ?s ?E (Val _) (λ _, fupd ?E _ _)) =>
      eapply tac_wp_value_nofupd
  | |- envs_entails _ (wp ?s ?E (Val _) (λ _, wp _ ?E _ _)) =>
      eapply tac_wp_value_nofupd
  | |- envs_entails _ (wp ?s ?E (Val _) _) =>
      eapply tac_wp_value
  | |- envs_entails _ (twp ?s ?E (Val _) (λ _, fupd ?E _ _)) =>
      eapply tac_twp_value_nofupd
  | |- envs_entails _ (twp ?s ?E (Val _) (λ _, twp _ ?E _ _)) =>
      eapply tac_twp_value_nofupd
  | |- envs_entails _ (twp ?s ?E (Val _) _) =>
      eapply tac_twp_value
  end.
(* iris_heap_lang/proofmode.v *)
Ltac wp_finish
:=
  wp_expr_simpl;      (* simplify occurrences of subst/fill *)
  try wp_value_head;  (* in case we have reached a value, get rid of the WP *)
  pm_prettify.
(* iris_heap_lang/proofmode.v *)
(* prettify ▷s caused by [MaybeIntoLaterNEnvs] and
                         λs caused by wp_value *)
Ltac solve_vals_compare_safe
:=
  (* The first branch is for when we have [vals_compare_safe] in the context.
     The other two branches are for when either one of the branches reduces to
     [True] or we have it in the context. *)
  fast_done || (left; fast_done) || (right; fast_done).
(* iris_heap_lang/proofmode.v *)
(* TODO: do this in one go, without [repeat]. *)
Ltac wp_pures
:=
  iStartProof;
  first [ (* The `;[]` makes sure that no side-condition magically spawns. *)
          progress repeat (wp_pure _; [])
        | wp_finish (* In case wp_pure never ran, make sure we do the usual cleanup. *)
        ].
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_bind `{!heapGS_gen hlc Σ} K Δ s E Φ e f :
  f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
  envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
Proof. rewrite envs_entails_unseal=> -> ->. by apply: wp_bind. Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_bind `{!heapGS_gen hlc Σ} K Δ s E Φ e f :
  f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
  envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
  envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
Proof. rewrite envs_entails_unseal=> -> ->. by apply: twp_bind. Qed.
(* iris_heap_lang/proofmode.v *)
Ltac wp_bind_core K
:=
  lazymatch eval hnf in K with
  | [] => idtac
  | _ => eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify]
  end.
(* iris_heap_lang/proofmode.v *)
Ltac twp_bind_core K
:=
  lazymatch eval hnf in K with
  | [] => idtac
  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|reduction.pm_prettify]
  end.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
  (0 < n)%Z →
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  (∀ l,
    match envs_app false (Esnoc Enil j (array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ' with
    | Some Δ'' =>
       envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Φ }})
    | None => False
    end) →
  envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ? ? HΔ.
  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_allocN.
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
  specialize (HΔ l).
  destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
  rewrite envs_app_sound //; simpl.
  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_allocN Δ s E j K v n Φ :
  (0 < n)%Z →
  (∀ l,
    match envs_app false (Esnoc Enil j (array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ with
    | Some Δ' =>
       envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }])
    | None => False
    end) →
  envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=> ? HΔ.
  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_allocN.
  rewrite left_id. apply forall_intro=> l.
  specialize (HΔ l).
  destruct (envs_app _ _ _) as [Δ'|] eqn:HΔ'; [ | contradiction ].
  rewrite envs_app_sound //; simpl.
  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  (∀ l,
    match envs_app false (Esnoc Enil j (l ↦ v)) Δ' with
    | Some Δ'' =>
       envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})
    | None => False
    end) →
  envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ? HΔ.
  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_alloc.
  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
  specialize (HΔ l).
  destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
  rewrite envs_app_sound //; simpl.
  apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_alloc Δ s E j K v Φ :
  (∀ l,
    match envs_app false (Esnoc Enil j (l ↦ v)) Δ with
    | Some Δ' =>
       envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }])
    | None => False
    end) →
  envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=> HΔ.
  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_alloc.
  rewrite left_id. apply forall_intro=> l.
  specialize (HΔ l).
  destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
  rewrite envs_app_sound //; simpl.
  apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_free Δ Δ' s E i K l v Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ v)%I →
  (let Δ'' := envs_delete false i false Δ' in
   envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
  envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ? Hlk Hfin.
  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_free.
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
  rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
  apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_free Δ s E i K l v Φ :
  envs_lookup i Δ = Some (false, l ↦ v)%I →
  (let Δ' := envs_delete false i false Δ in
   envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }])) →
  envs_entails Δ (WP fill K (Free (LitV l)) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=> Hlk Hfin.
  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_free.
  rewrite envs_lookup_split //; simpl.
  rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
  apply sep_mono_r, wand_intro_r. rewrite right_id //.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_load Δ Δ' s E i K b l q v Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (b, l ↦{q} v)%I →
  envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) →
  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ?? Hi.
  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_load.
  rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
  apply later_mono.
  destruct b; simpl.
  * iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
  * by apply sep_mono_r, wand_mono.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_load Δ s E i K b l dq v Φ :
  envs_lookup i Δ = Some (b, l ↦{dq} v)%I →
  envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
  envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=> ? Hi.
  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_load.
  rewrite envs_lookup_split //; simpl.
  destruct b; simpl.
  - iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
  - iIntros "[$ He]". iIntros "Hl". iApply Hi. iApply "He". iFrame "Hl".
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_store Δ Δ' s E i K l v v' Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ v)%I →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' with
  | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})
  | None => False
  end →
  envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ???.
  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  rewrite -wp_bind. eapply wand_apply; first by eapply wand_entails, wp_store.
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_store Δ s E i K l v v' Φ :
  envs_lookup i Δ = Some (false, l ↦ v)%I →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ with
  | Some Δ' => envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }])
  | None => False
  end →
  envs_entails Δ (WP fill K (Store (LitV l) v') @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal. intros.
  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  rewrite -twp_bind. eapply wand_apply; first by eapply wand_entails, twp_store.
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_xchg Δ Δ' s E i K l v v' Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ v)%I →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' with
  | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ v) @ s; E {{ Φ }})
  | None => False
  end →
  envs_entails Δ (WP fill K (Xchg (LitV l) (Val v')) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ???.
  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  rewrite -wp_bind. eapply wand_apply; first by eapply wand_entails, wp_xchg.
  rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
  rewrite right_id.
  by apply later_mono, sep_mono_r, wand_mono.
Qed.