phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_xchg Δ 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 $ v) @ s; E [{ Φ }])
  | None => False
  end →
  envs_entails Δ (WP fill K (Xchg (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_xchg.
  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_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ v)%I →
  vals_compare_safe v v1 →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' with
  | Some Δ'' =>
     v = v1 →
     envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})
  | None => False
  end →
  (v ≠ v1 →
   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) →
  envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ??? Hsuc Hfail.
  destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  destruct (decide (v = v1)) as [Heq|Hne].
  - rewrite -wp_bind. eapply wand_apply.
    { eapply wand_entails, wp_cmpxchg_suc; eauto. }
    rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
    apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
  - rewrite -wp_bind. eapply wand_apply.
    { eapply wand_entails, wp_cmpxchg_fail; eauto. }
    rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
    apply later_mono, sep_mono_r. apply wand_mono; auto.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_cmpxchg Δ s E i K l v v1 v2 Φ :
  envs_lookup i Δ = Some (false, l ↦ v)%I →
  vals_compare_safe v v1 →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ with
  | Some Δ' =>
     v = v1 →
     envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])
  | None => False
  end →
  (v ≠ v1 →
   envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) →
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=> ?? Hsuc Hfail.
  destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  destruct (decide (v = v1)) as [Heq|Hne].
  - rewrite -twp_bind. eapply wand_apply.
    { eapply wand_entails, twp_cmpxchg_suc; eauto. }
    rewrite /= {1}envs_simple_replace_sound //; simpl.
    apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
  - rewrite -twp_bind. eapply wand_apply.
    { eapply wand_entails, twp_cmpxchg_fail; eauto. }
    rewrite /= {1}envs_lookup_split //; simpl.
    apply sep_mono_r. apply wand_mono; auto.
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K b l dq v v1 v2 Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (b, l ↦{dq} v)%I →
  v ≠ v1 → vals_compare_safe v v1 →
  envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) →
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ???? Hi.
  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_cmpxchg_fail.
  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 "#".
  - iIntros "[$ He]". iIntros "Hl". iApply Hi. iApply "He". iFrame "Hl".
Qed.
(* iris_heap_lang/proofmode.v *)
Lemma tac_twp_cmpxchg_fail Δ s E i K b l dq v v1 v2 Φ :
  envs_lookup i Δ = Some (b, l ↦{dq} v)%I →
  v ≠ v1 → vals_compare_safe v v1 →
  envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) →
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal. intros ??? Hi. rewrite -twp_bind.
  eapply wand_apply; first by apply wand_entails, twp_cmpxchg_fail.
  (* [//] solves some evars and enables further simplification. *)
  rewrite envs_lookup_split /= // /=.
  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_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ v)%I →
  v = v1 → vals_compare_safe v v1 →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' with
  | Some Δ'' =>
     envs_entails Δ'' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E {{ Φ }})
  | None => False
  end →
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ?????; subst.
  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  rewrite -wp_bind. eapply wand_apply.
  { eapply wand_entails, wp_cmpxchg_suc; eauto. }
  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_cmpxchg_suc Δ s E i K l v v1 v2 Φ :
  envs_lookup i Δ = Some (false, l ↦ v)%I →
  v = v1 → vals_compare_safe v v1 →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ with
  | Some Δ' =>
     envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool true)) @ s; E [{ Φ }])
  | None => False
  end →
  envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=>????; subst.
  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  rewrite -twp_bind. eapply wand_apply.
  { eapply wand_entails, twp_cmpxchg_suc; eauto. }
  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_faa Δ Δ' s E i K l z1 z2 Φ :
  MaybeIntoLaterNEnvs 1 Δ Δ' →
  envs_lookup i Δ' = Some (false, l ↦ LitV z1)%I →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ' with
  | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ LitV z1) @ s; E {{ Φ }})
  | None => False
  end →
  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
Proof.
  rewrite envs_entails_unseal=> ???.
  destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, (wp_faa _ _ _ z1 z2).
  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_faa Δ s E i K l z1 z2 Φ :
  envs_lookup i Δ = Some (false, l ↦ LitV z1)%I →
  match envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (z1 + z2)))) Δ with
  | Some Δ' => envs_entails Δ' (WP fill K (Val $ LitV z1) @ s; E [{ Φ }])
  | None => False
  end →
  envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
Proof.
  rewrite envs_entails_unseal=> ??.
  destruct (envs_simple_replace _ _ _) as [Δ'|] eqn:HΔ'; [ | contradiction ].
  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, (twp_faa _ _ _ z1 z2).
  rewrite envs_simple_replace_sound //; simpl.
  rewrite right_id. by apply sep_mono_r, wand_mono.
Qed.
(* iris_heap_lang/proofmode.v *)
(* The tactic [wp_apply_core lem tac_suc tac_fail] evaluates [lem] to a
hypothesis [H] that can be applied, and then runs [wp_bind_core K; tac_suc H]
for every possible evaluation context [K].

- The tactic [tac_suc] should do [iApplyHyp H] to actually apply the hypothesis,
  but can perform other operations in addition (see [wp_apply] and [awp_apply]
  below).
- The tactic [tac_fail cont] is called when [tac_suc H] fails for all evaluation
  contexts [K], and can perform further operations before invoking [cont] to
  try again.

TC resolution of [lem] premises happens *after* [tac_suc H] got executed. *)
Ltac wp_apply_core lem tac_suc tac_fail
:=
  iStartProof;
  first
  [iPoseProofCore lem as false (fun H =>
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; tac_suc H)
     | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         twp_bind_core K; tac_suc H)
     | _ => fail 1 "wp_apply: not a 'wp'"
     end)
  |tac_fail ltac:(fun _ => wp_apply_core lem tac_suc tac_fail)
  |let P := type of lem in
   fail "wp_apply: cannot apply" lem ":" P ].
(* iris_heap_lang/proph_erasure.v *)
Definition erase_base_lit (l : base_lit) : base_lit
:=
  match l with
  | LitProphecy p => LitPoison
  | _ => l
  end.
(* iris_heap_lang/proph_erasure.v *)
Definition erase_resolve (e0 e1 e2 : expr) : expr
:= Fst (Fst (e0, e1, e2)).
(* iris_heap_lang/proph_erasure.v *)
Definition erased_new_proph : expr
:= (λ: <>, #LitPoison)%V #().
(* iris_heap_lang/proph_erasure.v *)
Fixpoint erase_expr (e : expr) : expr
:=
  match e with
  | Val v => Val (erase_val v)
  | Var x => Var x
  | Rec f x e => Rec f x (erase_expr e)
  | App e1 e2 => App (erase_expr e1) (erase_expr e2)
  | UnOp op e => UnOp op (erase_expr e)
  | BinOp op e1 e2 => BinOp op (erase_expr e1) (erase_expr e2)
  | If e0 e1 e2 => If (erase_expr e0) (erase_expr e1) (erase_expr e2)
  | Pair e1 e2 => Pair (erase_expr e1) (erase_expr e2)
  | Fst e => Fst (erase_expr e)
  | Snd e => Snd (erase_expr e)
  | InjL e => InjL (erase_expr e)
  | InjR e => InjR (erase_expr e)
  | Case e0 e1 e2 => Case (erase_expr e0) (erase_expr e1) (erase_expr e2)
  | Fork e => Fork (erase_expr e)
  | AllocN e1 e2 => AllocN (erase_expr e1) (erase_expr e2)
  | Free e => Free (erase_expr e)
  | Load e => Load (erase_expr e)
  | Xchg e1 e2 => Xchg (erase_expr e1) (erase_expr e2)
  | Store e1 e2 => Store (erase_expr e1) (erase_expr e2)
  | CmpXchg e0 e1 e2 => CmpXchg (erase_expr e0) (erase_expr e1) (erase_expr e2)
  | FAA e1 e2 => FAA (erase_expr e1) (erase_expr e2)
  | NewProph => erased_new_proph
  | Resolve e0 e1 e2 =>
    erase_resolve (erase_expr e0) (erase_expr e1) (erase_expr e2)
  end
with
erase_val (v : val) : val :=
  match v with
  | LitV l => LitV (erase_base_lit l)
  | RecV f x e => RecV f x (erase_expr e)
  | PairV v1 v2 => PairV (erase_val v1) (erase_val v2)
  | InjLV v => InjLV (erase_val v)
  | InjRV v => InjRV (erase_val v)
  end.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_expr_subst x v e :
  erase_expr (subst x v e) = subst x (erase_val v) (erase_expr e)
with
erase_val_subst x v (w : val) :
  erase_expr (subst x v w) = subst x (erase_val v) (erase_val w).
Proof.
  - destruct e; simpl; try case_decide;
      rewrite ?erase_expr_subst ?erase_val_subst; auto.
  - by destruct v.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_expr_subst' x v e :
  erase_expr (subst' x v e) = subst' x (erase_val v) (erase_expr e).
Proof. destruct x; eauto using erase_expr_subst. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_val_subst' x v (w : val) :
  erase_expr (subst x v w) = subst x (erase_val v) (erase_val w).
Proof. destruct x; eauto using erase_val_subst. Qed.
(* iris_heap_lang/proph_erasure.v *)
Fixpoint erase_ectx_item (Ki : ectx_item) : list ectx_item
:=
  match Ki with
  | AppLCtx v2 => [AppLCtx (erase_val v2)]
  | AppRCtx e1 => [AppRCtx (erase_expr e1)]
  | UnOpCtx op => [UnOpCtx op]
  | BinOpLCtx op v2 => [BinOpLCtx op (erase_val v2)]
  | BinOpRCtx op e1 => [BinOpRCtx op (erase_expr e1)]
  | IfCtx e1 e2 => [IfCtx (erase_expr e1) (erase_expr e2)]
  | PairLCtx v2 => [PairLCtx (erase_val v2)]
  | PairRCtx e1 => [PairRCtx (erase_expr e1)]
  | FstCtx => [FstCtx]
  | SndCtx => [SndCtx]
  | InjLCtx => [InjLCtx]
  | InjRCtx => [InjRCtx]
  | CaseCtx e1 e2 => [CaseCtx (erase_expr e1) (erase_expr e2)]
  | AllocNLCtx v2 => [AllocNLCtx (erase_val v2)]
  | AllocNRCtx e1 => [AllocNRCtx (erase_expr e1)]
  | FreeCtx => [FreeCtx]
  | LoadCtx => [LoadCtx]
  | XchgLCtx v2 => [XchgLCtx (erase_val v2)]
  | XchgRCtx e1 => [XchgRCtx (erase_expr e1)]
  | StoreLCtx v2 => [StoreLCtx (erase_val v2)]
  | StoreRCtx e1 => [StoreRCtx (erase_expr e1)]
  | CmpXchgLCtx v1 v2 => [CmpXchgLCtx (erase_val v1) (erase_val v2)]
  | CmpXchgMCtx e0 v2 => [CmpXchgMCtx (erase_expr e0) (erase_val v2)]
  | CmpXchgRCtx e0 e1 => [CmpXchgRCtx (erase_expr e0) (erase_expr e1)]
  | FaaLCtx v2 => [FaaLCtx (erase_val v2)]
  | FaaRCtx e1 => [FaaRCtx (erase_expr e1)]
  | ResolveLCtx ctx v1 v2 =>
    erase_ectx_item ctx ++
    [PairLCtx (erase_val v1); PairLCtx (erase_val v2); FstCtx; FstCtx]
  | ResolveMCtx e0 v2 =>
    [PairRCtx (erase_expr e0); PairLCtx (erase_val v2); FstCtx; FstCtx]
  | ResolveRCtx e0 e1 =>
    [PairRCtx (erase_expr e0, erase_expr e1); FstCtx; FstCtx]
  end.
(* iris_heap_lang/proph_erasure.v *)
Definition erase_ectx (K : ectx heap_ectx_lang) : ectx heap_ectx_lang
:=
  mbind erase_ectx_item K.
(* iris_heap_lang/proph_erasure.v *)
Definition erase_tp (tp : list expr) : list expr
:= erase_expr <$> tp.
(* iris_heap_lang/proph_erasure.v *)
Definition erase_heap (h : gmap loc (option val)) : gmap loc (option val)
:=
  (λ ov : option val, erase_val <$> ov) <$> h.
(* iris_heap_lang/proph_erasure.v *)
Definition erase_state (σ : state) : state
:=
  {| heap := erase_heap (heap σ); used_proph_id := ∅ |}.
(* iris_heap_lang/proph_erasure.v *)
Definition erase_cfg (ρ : cfg heap_lang) : cfg heap_lang
:=
  (erase_tp ρ.1, erase_state ρ.2).
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_to_val e v :
  to_val (erase_expr e) = Some v → ∃ v', to_val e = Some v' ∧ erase_val v' = v.
Proof. destruct e; naive_solver. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_not_val e : to_val e = None → to_val (erase_expr e) = None.
Proof. by destruct e. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_ectx_app K K' : erase_ectx (K ++ K') = erase_ectx K ++ erase_ectx K'.
Proof. by rewrite /erase_ectx bind_app. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_ectx_expr K e :
  erase_expr (fill K e) = fill (erase_ectx K) (erase_expr e).
Proof.
  revert e.
  induction K as [|Ki K IHK] using rev_ind; simplify_eq/=; first done.
  intros e.
  rewrite !erase_ectx_app !fill_app /= -IHK {IHK}.
  induction Ki; rewrite /= ?fill_app /= /erase_resolve; eauto with f_equal.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma val_is_unboxed_erased v :
  val_is_unboxed (erase_val v) ↔ val_is_unboxed v.
Proof.
  destruct v; rewrite /= /lit_is_unboxed; repeat (done || simpl; case_match).
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma vals_compare_safe_erase v1 v2 :
  vals_compare_safe (erase_val v1) (erase_val v2) ↔
  vals_compare_safe v1 v2.
Proof. rewrite /vals_compare_safe !val_is_unboxed_erased. done. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_val_inj_iff v1 v2 :
  vals_compare_safe v1 v2 → erase_val v1 = erase_val v2 ↔ v1 = v2.
Proof.
  destruct v1, v2; rewrite /= /lit_is_unboxed;
    repeat (done || (by intros [[] | []]) || simpl; case_match).
Qed.
(* iris_heap_lang/proph_erasure.v *)
(* if [un_op_eval] succeeds on erased value,
    the so should it on the original value. *)
Lemma un_op_eval_erase op v v' :
  un_op_eval op (erase_val v) = Some v' ↔
  ∃ w, un_op_eval op v = Some w ∧ erase_val w = v'.
Proof.
  destruct op; simpl; repeat case_match; naive_solver.
Qed.
(* iris_heap_lang/proph_erasure.v *)
(* if [bin_op_eval] succeeds on erased value,
    then so should it on the original value. *)
Lemma bin_op_eval_erase op v1 v2 v' :
  bin_op_eval op (erase_val v1) (erase_val v2) = Some v' ↔
  ∃ w, bin_op_eval op v1 v2 = Some w ∧ erase_val w = v'.
Proof.
  rewrite /bin_op_eval /bin_op_eval_int /bin_op_eval_bool /bin_op_eval_loc;
    split; [intros ?|intros (?&?&?)];
      repeat (case_match; simplify_eq/=); eauto.
  - eexists _; split; eauto; simpl.
    erewrite bool_decide_ext; first by eauto.
    rewrite erase_val_inj_iff; done.
  - by assert (vals_compare_safe v1 v2) by by apply vals_compare_safe_erase.
  - by erewrite bool_decide_ext; last apply erase_val_inj_iff.
  - by assert (vals_compare_safe (erase_val v1) (erase_val v2))
      by by apply vals_compare_safe_erase.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma lookup_erase_heap_None h l : erase_heap h !! l = None ↔ h !! l = None.
Proof. rewrite lookup_fmap; by destruct (h !! l). Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma lookup_erase_heap h l : erase_heap h !! l = (λ ov, erase_val <$> ov) <$> h !! l.
Proof. by rewrite lookup_fmap. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_heap_insert_Some h l v :
  erase_heap (<[l := Some v]> h) = <[l := Some $ erase_val v]> (erase_heap h).
Proof.
  by rewrite /erase_heap fmap_insert.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_heap_insert_None h l v :
  erase_heap (<[l := None]> h) = <[l := None]> (erase_heap h).
Proof.
  by rewrite /erase_heap fmap_insert.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma fmap_heap_array (f : val → val) l vs :
  (λ ov : option val, f <$> ov) <$> heap_array l vs = heap_array l (f <$> vs).
Proof.
  revert l; induction vs as [|v vs IHvs]; intros l;
    first by rewrite /= fmap_empty.
  by rewrite /= -!insert_union_singleton_l !fmap_insert IHvs.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_heap_array l i v h :
  erase_heap (heap_array l (replicate i v) ∪ h) =
  heap_array l (replicate i (erase_val v)) ∪ erase_heap h.
Proof.
  apply map_eq => l'.
  rewrite /erase_heap lookup_fmap !lookup_union -fmap_replicate
  - fmap_heap_array !lookup_fmap.
    by destruct (heap_array l (replicate i v) !! l'); destruct (h !! l').
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erase_state_init l n v σ:
  erase_state (state_init_heap l n v σ) =
  state_init_heap l n (erase_val v) (erase_state σ).
Proof. by rewrite /erase_state /state_init_heap /= erase_heap_array. Qed.
(* iris_heap_lang/proph_erasure.v *)
Definition base_steps_to_erasure_of (e1 : expr) (σ1 : state) (e2 : expr)
           (σ2 : state) (efs : list expr)
:=
  ∃ κ' e2' σ2' efs',
    base_step e1 σ1 κ' e2' σ2' efs' ∧
    erase_expr e2' = e2 ∧ erase_state σ2' = σ2 ∧ erase_tp efs' = efs.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_rec f x e v σ :
  base_steps_to_erasure_of ((rec: f x := e)%V v) σ
    (subst' x (erase_val v)
            (subst' f (rec: f x := erase_expr e) (erase_expr e)))
    (erase_state σ) [].
Proof. by repeat econstructor; rewrite !erase_expr_subst'. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_NewProph σ :
  base_steps_to_erasure_of NewProph σ #LitPoison (erase_state σ) [].
Proof. eexists _, _, _, _; split; first eapply new_proph_id_fresh; done. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_AllocN n v σ l :
  (0 < n)%Z →
  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → erase_heap (heap σ) !! (l +ₗ i) = None) →
  base_steps_to_erasure_of
    (AllocN #n v) σ #l (state_init_heap l n (erase_val v) (erase_state σ)) [].
Proof.
  eexists _, _, _, _; simpl; split;
    first econstructor; try setoid_rewrite <- lookup_erase_heap_None;
      rewrite ?erase_heap_insert /=; eauto using erase_state_init.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_Free l v σ :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (Free #l) σ #()
   {| heap := <[l:=None]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
  rewrite /state_upd_heap /erase_state /= erase_heap_insert_None //.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_Load l σ v :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (! #l) σ v (erase_state σ) [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_Xchg l v w σ :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (Xchg #l w) σ v
   {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
  rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_Store l v w σ :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (#l <- w) σ #()
   {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
  rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_CmpXchg l v w σ vl :
  erase_heap (heap σ) !! l = Some (Some vl) →
  vals_compare_safe vl (erase_val v) →
  base_steps_to_erasure_of
    (CmpXchg #l v w) σ
    (vl, #(bool_decide (vl = erase_val v)))%V
    (if bool_decide (vl = erase_val v)
     then {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ));
             used_proph_id := ∅ |}
     else erase_state σ) [].
Proof.
  intros Hl Hvl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[u|]|] eqn:?; simplify_eq/=.
  rewrite -> vals_compare_safe_erase in Hvl.
  destruct (decide (u = v)) as [->|Hneq].
  - eexists _, _, _, _; simpl; split.
    { econstructor; eauto. }
    rewrite !bool_decide_eq_true_2; eauto using erase_val_inj_iff; [].
    rewrite -?erase_heap_insert_Some.
    split_and!; auto.
  - eexists _, _, _, _; simpl; split.
    { econstructor; eauto. }
    rewrite !bool_decide_eq_false_2; eauto; [].
    by rewrite erase_val_inj_iff.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_base_step_base_step_FAA l n m σ :
  erase_heap (heap σ) !! l = Some (Some #n) →
  base_steps_to_erasure_of
    (FAA #l #m) σ #n
    {| heap := <[l:= Some #(n + m)]> (erase_heap (heap σ));
       used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[[[]| | | |]|]|] eqn:?; simplify_eq/=.
  repeat econstructor; first by eauto.
  by rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some.
Qed.
(* iris_heap_lang/proph_erasure.v *)
(* When the erased program makes a base step, so does the original program. *)
Lemma erased_base_step_base_step e1 σ1 κ e2 σ2 efs:
  base_step (erase_expr e1) (erase_state σ1) κ e2 σ2 efs →
  base_steps_to_erasure_of e1 σ1 e2 σ2 efs.
Proof.
  intros Hhstep.
  inversion Hhstep; simplify_eq/=;
    repeat match goal with
           | H : _ = erase_expr ?e |- _ => destruct e; simplify_eq/=
           | H : _ = erase_val ?v |- _ => destruct v; simplify_eq/=
           | H : _ = erase_base_lit ?l |- _ => destruct l; simplify_eq/=
           | H : context [erased_new_proph] |- _ => unfold erased_new_proph in H
           | H : un_op_eval _ (erase_val _) = Some _ |- _ =>
             apply un_op_eval_erase in H as [? [? ?]]
           | H : bin_op_eval _ (erase_val _) (erase_val _) = Some _ |- _ =>
             apply bin_op_eval_erase in H as [? [? ?]]
           | H : val_is_unboxed (erase_val _) |- _ =>
             apply -> val_is_unboxed_erased in H
           end; simplify_eq/=;
    try (by repeat econstructor);
  eauto using erased_base_step_base_step_rec,
    erased_base_step_base_step_NewProph,
    erased_base_step_base_step_AllocN,
    erased_base_step_base_step_Free,
    erased_base_step_base_step_Load,
    erased_base_step_base_step_Xchg,
    erased_base_step_base_step_Store,
    erased_base_step_base_step_CmpXchg,
    erased_base_step_base_step_FAA.
Qed.