phanerozoic/Coq-Iris huggingface dataset:
(* iris_unstable/heap_lang/interpreter.v *)
Definition interp_modify_state (f: state → state): InterpretM ()
:=
    interp_modify (modify_lang_state f).
(* iris_unstable/heap_lang/interpreter.v *)
Definition interp_read {A} (f: state → A): InterpretM A
:=
    λ s, (inl (f s.(lang_state)), s).
(* iris_unstable/heap_lang/interpreter.v *)
Definition interp_error {A} (msg: string) : InterpretM A
:= λ s, (inr (Stuck msg), s).
(* iris_unstable/heap_lang/interpreter.v *)
Definition interp_alloc (n:Z): InterpretM loc
:=
    λ s, (inl {| loc_car := s.(next_loc)|}, interp_state_alloc n s).
(* iris_unstable/heap_lang/interpreter.v *)
Definition read_loc (method: string) (vl: val) : InterpretM (loc*val)
:=
      match vl with
      | LitV (LitLoc l) =>
        mv ← interp_read (λ σ, σ.(heap) !! l);
        match mv with
        | Some (Some v) => mret (l, v)
        | Some None =>
          interp_error $ method +:+ ": use after free at location: " +:+ pretty l
        | None =>
          interp_error $ method +:+ ": unallocated location: " +:+ pretty l
        end
      | _ => interp_error $ method +:+ ": applied to non-loc " +:+ pretty vl
      end.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma error_not_inl {A} {msg s} {v: A} {s'} :
    interp_error msg s = (inl v, s') → False.
Proof. by inversion 1. Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma mret_inv {A} (v: A) s v' s' :
    (mret v : InterpretM A) s = (inl v', s') → v = v' ∧ s = s'.
Proof. by inversion 1. Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interp_bind_inv A B (x: InterpretM A) (f: A → InterpretM B) r s s' :
    (x ≫= f) s = (r, s') →
    (∃ e, x s = (inr e, s') ∧ r = inr e) ∨
    (∃ s0 x', x s = (inl x', s0) ∧
              f x' s0 = (r, s')).
Proof.
    rewrite /mbind /interp_bind.
    repeat case_match; inversion 1; subst; eauto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interp_bind_inl_inv A B (x: InterpretM A) (f: A → InterpretM B) (r: B) s s' :
    (x ≫= f) s = (inl r, s') →
    ∃ s0 x', x s = (inl x', s0) ∧
             f x' s0 = (inl r, s').
Proof.
    intros [(e & ? & ?) | (s0 & x' & H1 & H2)]%interp_bind_inv.
    - congruence.
    - rewrite H1.
      eexists _, _; eauto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interp_fmap_inv {A B} (f: A → B) x s v s' :
    (fmap f x : InterpretM B) s = (inl v, s') →
    ∃ v0, v = f v0 ∧ x s = (inl v0, s').
Proof.
    rewrite /fmap /interp_fmap.
    repeat case_match; inversion 1; subst; eauto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma read_loc_inv method vl s l v s' :
    read_loc method vl s = (inl (l, v), s') →
    vl = LitV (LitLoc l) ∧
    s' = s ∧
    s.(lang_state).(heap) !! l = Some (Some v).
Proof.
    rewrite /read_loc.
    destruct vl as [l' | | | | ]; try by inversion 1.
    destruct l' as [| | | | l' |]; intro H; try by inversion H.
    apply interp_bind_inl_inv in H as (s0 & mv & Heq1 & Heq2).
    destruct mv as [mv|]; try by inversion Heq2.
    destruct mv; inversion Heq2; subst; clear Heq2.
    inversion Heq1; subst; clear Heq1.
    eauto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Ltac errored
:=
    lazymatch goal with
    | H: interp_error _ _ = (inl _, _) |- _ => solve [ exfalso; apply (error_not_inl H) ]
    | H: (inr _, _) = (inl _, _) |- _ => solve [ exfalso; inversion H ]
    end.
(* iris_unstable/heap_lang/interpreter.v *)
Ltac success
:=
    repeat
      lazymatch goal with
      | H: mret _ _ = (inl _, _) |- _ =>
        let Heqv := fresh "Heqv" in
        let Heqs := fresh "Heqs" in
        apply mret_inv in H as [Heqv Heqs]; subst
      | H: (_ ≫= (λ x, _)) _ = (inl _, _) |- _ =>
        let s := fresh "s" in
        let x := fresh x in
        let Heq1 := fresh "Heq" in
        let Heq2 := fresh "Heq" in
        apply interp_bind_inl_inv in H as (s & x & Heq1 & Heq2); subst
      | H: (_ <$> _) _ = (inl ?v, _) |- _ =>
        let s := fresh "s" in
        let v_tmp := fresh "v" in
        rename v into v_tmp;
        apply interp_fmap_inv in H as (v & -> & H)
      | H: interp_modify _ _ = (inl _, _) |- _ => invc H
      | H: interp_modify_state _ _ = (inl _, _) |- _ => invc H
      | H: interp_read _ _ = (inl _, _) |- _ => invc H
      | H: read_loc _ _ _ = (inl _, _) |- _ =>
        apply read_loc_inv in H as (-> & -> & H)
      end; subst.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interp_bind_inr_inv {A B} (x: InterpretM A) (f: A → InterpretM B) r s s' :
    (x ≫= f) s = (inr r, s') →
    (x s = (inr r, s')) ∨
    (∃ s0 x', x s = (inl x', s0) ∧ f x' s0 = (inr r, s')).
Proof.
    rewrite /mbind /interp_bind.
    repeat case_match; intros; simplify_eq/=; eauto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interp_fmap_inr_inv {A B} (f: A → B) (x: InterpretM A) s e s' :
    (fmap f x : InterpretM B) s = (inr e, s') →
    x s = (inr e, s').
Proof.
    rewrite /fmap /interp_fmap.
    repeat case_match; intros; simplify_eq/=; auto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma read_loc_inr_inv method vl s err s' :
    read_loc method vl s = (inr err, s') →
    s = s' ∧ match vl with
             | LitV (LitLoc l) => ∀ v, s.(lang_state).(heap) !! l ≠ Some (Some v)
             | _ => True
             end.
Proof.
    rewrite /read_loc.
    repeat case_match; subst; try solve [ inversion 1; subst; auto ].
    intros H.
    apply interp_bind_inr_inv in H as [H|(s0&x& Hexec1 & Hexec2)]; success.
    - invc H.
    - repeat case_match; invc Hexec2.
      + intuition congruence.
      + intuition congruence.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Ltac failure
:=
    repeat
      match goal with
      | H: (_ ≫= _) _ = (inr _, _) |- _ =>
        let s := fresh "s" in
        let x := fresh "x" in
        let Heq := fresh "Heq" in
        apply interp_bind_inr_inv in H as [H | (s & x & Heq & H)]
      | H: interp_error _ _ = (inr _, _) |- _ => invc H
      | H: mret _ _ = (inr _, _) |- _ => solve [ inversion H ]
      | H: interp_modify _ _ = (inr _, _) |- _ => solve [ inversion H ]
      | H: interp_modify_state _ _ = (inr _, _) |- _ => solve [ inversion H ]
      | H: (_ <$> _) _ = (inr _, _) |- _ =>
        apply interp_fmap_inr_inv in H
      | H: read_loc _ _ _ = (inr _, _) |- _ =>
        apply read_loc_inr_inv in H as [-> H]
      end; subst.
(* iris_unstable/heap_lang/interpreter.v *)
(* to make the below definition work with strings as well we add an
  instance of [Pretty string] *)
Instance pretty_string : Pretty string
:= λ s, s.
(* iris_unstable/heap_lang/interpreter.v *)
Definition pretty_app (s: string) {A} `{Pretty A} (x:A) : string
:=
    s +:+ pretty x.
(* iris_unstable/heap_lang/interpreter.v *)
(* We explain errors which in the semantics are represented by a pure function
     returning None; to sanity-check these definitions, we prove they cover
     exactly the cases where the underlying operation returns None. *)
Definition option_opposites {A B} (m1 : option A) (m2 : option B)
:=
    is_Some m1 ↔ m2 = None.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma option_opposites_alt {A B} (m1 : option A) (m2 : option B) :
    option_opposites m1 m2 ↔ match m1, m2 with
                             | Some _, None   => True
                             | None  , Some _ => True
                             | _     , _      => False
                             end.
Proof.
    rewrite /option_opposites is_Some_alt.
    repeat case_match; intuition congruence.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* produce an error message for [un_op_eval] *)
Definition explain_un_op_fail op v : option string
:=
    match op with
    | NegOp => match v with
               | LitV (LitInt _) => None
               | LitV (LitBool _) => None
               | _ => Some $ "~ (NegOp) can only be applied to integers and booleans, got " + v
               end
    | MinusUnOp =>
      match v with
      | LitV (LitInt _) => None
      | _ => Some $ "unary - (MinusUnOp) can only be applied to integers, got " + v
      end
    end.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma explain_un_op_fail_wf op v :
    option_opposites (explain_un_op_fail op v) (un_op_eval op v).
Proof.
    apply option_opposites_alt.
    rewrite /explain_un_op_fail /un_op_eval.
    repeat case_match; simplify_eq/=; auto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Definition explain_unboxed v : option string
:=
    match v with
    | LitV l | InjLV (LitV l) | InjRV (LitV l) =>
      match l with
      | LitPoison => Some "poison values (from erasing prophecies) cannot be compared"
      | LitProphecy _ => Some "prophecies cannot be compared"
      | _ => None
      end
    | InjLV _ | InjRV _ => Some "sum values can only be compared if they contain literals"
    | PairV _ _ => Some "pairs are large and considered boxed, must compare by field"
    | RecV _ _ _ => Some "closures are large and cannot be compared"
    end.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma explain_unboxed_wf v :
    match explain_unboxed v with
    | Some _ => ~val_is_unboxed v
    | None   => val_is_unboxed v
    end.
Proof.
    rewrite /explain_unboxed /val_is_unboxed /lit_is_unboxed.
    repeat case_match; intuition congruence.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Definition explain_vals_compare_safe_fail v1 v2 : option string
:=
    match explain_unboxed v1, explain_unboxed v2 with
    | Some msg1, Some msg2 =>
      Some $ "one of " + v1 + " and " + v2 + " must be unboxed to compare: "
      + v1 + ": " + msg1 + ", "
      + v2 + ": " + msg2
    | _, _ => None
    end.
(* iris_unstable/heap_lang/interpreter.v *)
(* [explain_vals_compare_safe_fail] gives an explanation when
  [vals_compare_safe] would be false (that is, when v1 and v2 cannot be
  compared) *)
Lemma explain_vals_compare_safe_fail_wf v1 v2 :
    is_Some (explain_vals_compare_safe_fail v1 v2) ↔ ~vals_compare_safe v1 v2.
Proof.
    cut (explain_vals_compare_safe_fail v1 v2 = None ↔ vals_compare_safe v1 v2).
    { rewrite is_Some_alt.
      destruct (explain_vals_compare_safe_fail _ _); intuition congruence. }
    rewrite /explain_vals_compare_safe_fail /vals_compare_safe.
    pose proof (explain_unboxed_wf v1).
    pose proof (explain_unboxed_wf v2).
    destruct (explain_unboxed v1), (explain_unboxed v2); intuition congruence.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* produce an error message for [bin_op_eval] *)
Definition explain_bin_op_fail op v1 v2 : option string
:=
    if decide (op = EqOp)
    then (explain_vals_compare_safe_fail v1 v2)
    else match v1, v2 with
         | LitV (LitInt _), LitV (LitInt _) =>
           match op with
           | OffsetOp => Some $ "cannot add to integer " + v1 + " with +ₗ (only locations)"
           | _ => None
           end
         | LitV (LitBool b1), LitV (LitBool b2) =>
           match bin_op_eval_bool op b1 b2 with
           | Some _ => None
           | None => Some $ "non-boolean operator applied to booleans " + op
           end
         | LitV (LitLoc _), _ =>
           match op, v2 with
           | OffsetOp, LitV (LitInt _) => None
           | OffsetOp, _ => Some $ "can only call +ₗ on integers, got " + v2
           | LeOp, LitV (LitLoc _) => None
           | LeOp, _ => Some $ "cannot use ≤ on location " + v1 + " and " + v2
           | LtOp, LitV (LitLoc _) => None
           | LtOp, _ => Some $ "cannot use < on location " + v1 + " and " + v2
           | _, _ => Some $ "the only supported operations on locations are " +
                            " +ₗ #i, ≤ #l and < #l; got " + op + " " + v2
           end
         | _, _ => Some $ "mismatched types of values " + v1 + " and " + v2
         end.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma explain_bin_op_fail_wf op v1 v2 :
    option_opposites (explain_bin_op_fail op v1 v2) (bin_op_eval op v1 v2).
Proof.
    apply option_opposites_alt.
    rewrite /explain_bin_op_fail /bin_op_eval
            /bin_op_eval_int /bin_op_eval_bool /bin_op_eval_loc.
    repeat (case_match; simplify_eq/=; auto).
    - pose proof (explain_vals_compare_safe_fail_wf v1 v2).
      intuition eauto.
    - pose proof (explain_vals_compare_safe_fail_wf v1 v2) as Hwf.
      replace (explain_vals_compare_safe_fail v1 v2) in Hwf.
      rewrite -> is_Some_alt in Hwf.
      intuition eauto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* define a shorthand for readability below *)
Notation error
:= interp_error.
(* iris_unstable/heap_lang/interpreter.v *)
(* * Theory for proving steps are sound. *)
Lemma atomic_step e σ e' σ' :
  base_step e σ [] e' σ' [] →
  ∀ tp, rtc erased_step (e :: tp, σ) (e' :: tp, σ').
Proof.
  intros ? tp.
  apply rtc_once.
  exists [].
  eapply (step_atomic e σ e' σ' [] [] tp); simpl; auto.
  - rewrite app_nil_r //.
  - eapply (Ectx_step []); eauto.
Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma step_inv ts1 σ1 κ ts2 σ2 :
  step (Λ:=heap_lang) (ts1, σ1) κ (ts2, σ2) →
  ∃ (t1 : list expr) (e1 : expr) (t2 : list expr) (e2 : expr) (efs: list expr),
    ts1 = t1 ++ e1 :: t2 ∧
    ts2 = t1 ++ e2 :: t2 ++ efs ∧
    prim_step e1 σ1 κ e2 σ2 efs.
Proof.
  inversion 1.
  simplify_eq.
  eauto 10.
Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma fill_step K (e: expr) σ tp κ e' σ' tp' :
  step (e :: tp, σ) κ (e' :: tp', σ') →
  step (fill K e :: tp, σ) κ (fill K e' :: tp', σ').
Proof.
  intros Hstep.
  apply step_inv in Hstep as (t1 & e1 & t2 & e2 & efs & Heq1 & Heq2 & Hprim_step).
  pose proof Hprim_step as H.
  apply (fill_prim_step K) in H.
  simpl in H.
  destruct t1 as [|e0 t1].
  - simplify_eq/=.
    eapply (step_atomic _ _ _ _ efs [] t2); eauto.
  - simplify_eq/=.
    eapply (step_atomic _ _ _ _ efs (fill K e0 :: t1) t2); eauto.
Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma fill_erased_step (e: expr) σ tp e' σ' tp' K :
  erased_step (e :: tp, σ) (e' :: tp', σ') →
  erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ').
Proof.
  rewrite /erased_step.
  intros [κ Hstep].
  exists κ.
  apply fill_step; auto.
Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma step_cons_no_destroy (e: expr) tp σ κ ρ2 :
  step (e :: tp, σ) κ ρ2 →
  ∃ e' tp' σ', ρ2 = (e' :: tp', σ').
Proof.
  destruct ρ2 as [ts' σ'].
  intros (t1&?&?&?&?&?&?&?)%step_inv; subst.
  destruct t1; simplify_eq/=; eauto.
Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma language_nsteps_inv_r (Λ: language) n ρ1 κs ρ2 :
  language.nsteps (Λ:=Λ) (S n) ρ1 κs ρ2 →
  ∃ ρ' κ κs', step ρ1 κ ρ' ∧ κs = κ ++ κs' ∧
              language.nsteps n ρ' κs' ρ2.
Proof. inversion 1; subst; eauto 10. Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma fill_erased_steps (e: expr) σ tp e' σ' tp' K :
  rtc erased_step (e :: tp, σ) (e' :: tp', σ') →
  rtc erased_step (fill K e :: tp, σ) (fill K e' :: tp', σ').
Proof.
  rewrite !erased_steps_nsteps.
  destruct 1 as (n & κs & Hsteps).
  generalize dependent e.
  generalize dependent tp.
  generalize dependent σ.
  generalize dependent e'.
  generalize dependent tp'.
  generalize dependent σ'.
  generalize dependent κs.
  induction n as [|n IHn]; intros ??????? Hsteps.
  - invc Hsteps.
    exists 0, [].
    constructor.
  - apply language_nsteps_inv_r in Hsteps as (ρ2 & κ & κs' & (Hstep & -> & Hsteps)).
    (* here is the crucial step: to apply [fill_step] need to know that [ρ2] has
    the right structure, which comes from threads not getting destroyed *)
    edestruct step_cons_no_destroy as (e''&tp''&σ''&Heq); eauto; subst.
    apply (fill_step K) in Hstep.
    apply IHn in Hsteps as (n'&κs&?).
    exists (S n'), (κ ++ κs).
    econstructor; eauto.
Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Ltac change_to_fill e
:=
    reshape_expr e ltac:(fun K e' =>
                           (* find a non-trivial context *)
                           lazymatch K with
                           | [_] => change e with (fill K e')
                           end).
(* iris_unstable/heap_lang/interpreter.v *)
Ltac step_ctx
:=
    lazymatch goal with
    | |- rtc erased_step (?e :: _, _) _ =>
      change_to_fill e;
      step by (apply fill_erased_steps; eauto)
    end.
(* iris_unstable/heap_lang/interpreter.v *)
Ltac step_atomic
:=
    step by (apply atomic_step; eauto using base_step);
    try reflexivity.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma state_wf_init_alloc (v0 : val) (s : interp_state) (n : Z) :
    (0 ≤ n)%Z →
    state_wf s →
    state_wf
      (modify_lang_state
          (λ σ : state, state_init_heap {| loc_car := next_loc s |} n v0 σ)
          (interp_state_alloc n s)).
Proof.
    intros Hn.
    constructor; rewrite /modify_lang_state /interp_state_alloc /=; intros l ?.
    apply fin_maps.lookup_union_None; split.
    - destruct (heap_array _ _ !! l) eqn:Hlookup; auto.
      apply heap_array_lookup in Hlookup as (j & w & Hle & ? & ? & Hlookup); subst.
      apply lookup_replicate in Hlookup as [? ?]; subst.
      simpl in *.
      lia.
    - apply state_wf_holds; auto.
      lia.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma state_wf_same_dom s f :
    (dom (f s.(lang_state)).(heap) = dom s.(lang_state).(heap)) →
    state_wf s →
    state_wf (modify_lang_state f s).
Proof.
    intros Hdom_eq Hwf.
    constructor; rewrite /modify_lang_state /= => l ?.
    apply (fin_map_dom.not_elem_of_dom (D:=gset loc)).
    rewrite Hdom_eq.
    apply fin_map_dom.not_elem_of_dom.
    apply state_wf_holds; auto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma state_wf_upd s l mv0 v' :
    state_wf s →
    heap (lang_state s) !! l = Some mv0 →
    state_wf (modify_lang_state (λ σ : state, state_upd_heap <[l:=v']> σ) s).
Proof.
    intros Hwf Heq.
    apply state_wf_same_dom; auto.
    rewrite fin_map_dom.dom_insert_L.
    apply (fin_map_dom.elem_of_dom_2 (D:=gset loc)) in Heq.
    set_solver.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interpret_wf fuel (e: expr) s v s' :
    state_wf s →
    interpret fuel e s = (inl v, s') →
    state_wf s'.
Proof.
    revert e s v s'.
    induction fuel as [|fuel]; simpl; intros e s v s' **; [ errored | ].
    destruct e; try errored; success; eauto;
      (repeat case_match; subst; try errored;
       success;
       eauto using state_wf_upd).
    - match goal with
      | H: interp_alloc _ _ = (_, _) |- _ => invc H
      end.
      apply state_wf_init_alloc; eauto.
      lia.
    - apply state_wf_same_dom; eauto.
    - constructor; intros.
      simpl.
      apply state_wf_holds; auto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma interpret_sound fuel e s v s' :
    state_wf s →
    interpret fuel e s = (inl v, s') →
    rtc erased_step (e :: s.(forked_threads), s.(lang_state)) (Val v :: s'.(forked_threads), s'.(lang_state)).
Proof.
    revert e s v s'.
    induction fuel as [|fuel]; simpl; intros e s v s' **; [ errored | ].
    destruct e; try errored; success; cbn [forked_threads lang_state];
      repeat match goal with
             | H: (match ?x with
                   | _ => _
                   end _ = (inl _, _)) |- _ =>
               let Heqn := fresh "Heqn" in
               destruct x eqn:Heqn; try errored; [idtac]
             | _ => progress success
             | _ => step_ctx
             | _ => step_atomic
             end.
    - (* Val *)
      reflexivity.
    - (* App *)
      eauto.
    - (* If *)
      lazymatch goal with
      | |- context[LitBool ?b] => destruct b; step_atomic; eauto
      end.
    - (* Case *)
      lazymatch goal with
      | |- context[Case (Val ?v)] => destruct v; try errored; step_atomic; eauto
      end.
    - (* AllocN *)
      lazymatch goal with
      | H: interp_alloc _ _ = _ |- _ => invc H
      end.
      eapply atomic_step. constructor; auto; intros.
      simpl. apply state_wf_holds; eauto.
      simpl; lia.
    - (* Fork *)
      eapply rtc_once. exists [].
      lazymatch goal with
      | |- context[Fork ?e] => eapply (step_atomic _ _ _ _ [e] []); simpl; eauto
      end.
      apply base_prim_step; simpl.
      eauto using base_step.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* * Theory for expressions that are stuck after some execution steps. *)
Definition eventually_stuck (e: expr) tp σ tp' σ'
:=
    ∃ e'', rtc erased_step (e :: tp, σ) (e'':: tp', σ') ∧ stuck e'' σ'.
(* iris_unstable/heap_lang/interpreter.v *)
(* a stuck expression is eventually stuck *)
Lemma eventually_stuck_now (e: expr) tp σ :
    stuck e σ →
    eventually_stuck e tp σ tp σ.
Proof.
    intros.
    exists e.
    split; [ reflexivity | auto ].
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* we can "peel off" some number of execution steps before proving that an
  expression is stuck *)
Lemma eventually_stuck_steps e tp σ tp0 σ0 e' tp' σ' :
    rtc erased_step (e :: tp, σ) (e' :: tp0, σ0) →
    eventually_stuck e' tp0 σ0 tp' σ' →
    eventually_stuck e tp σ tp' σ'.
Proof.
    intros Hsteps (e'' & Hsteps' & Hstuck).
    eexists. split; [ etrans; eauto | eauto ].
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* [eventually_stuck] respects evaluation contexts *)
Lemma eventually_stuck_fill K e tp σ tp' σ' :
    eventually_stuck e tp σ tp' σ' →
    eventually_stuck (fill K e) tp σ tp' σ'.
Proof.
    intros (e' & Hsteps & Hstuck).
    eexists (fill K e'). split.
    - apply fill_erased_steps; auto.
    - apply stuck_fill; auto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* peel off execution steps and use above automation to prove the [rtc
  erased_steps] premise *)
Ltac stuck_steps
:=
    eapply eventually_stuck_steps;
    [ repeat step_ctx; (step_atomic || reflexivity)
    |].
(* iris_unstable/heap_lang/interpreter.v *)
(* automate using hypotheses about stuckness inside an evaluation context *)
Ltac stuck_fill
:=
    lazymatch goal with
    | |- eventually_stuck ?e _ _ _ _ =>
      change_to_fill e; apply eventually_stuck_fill; solve [ eauto ]
    end.
(* iris_unstable/heap_lang/interpreter.v *)
(* [terminal_expr e] holds when e cannot be the result of taking a context
  step. Slightly more formally, e doesn't have the shape [fill K e'] where e' is
  reducible. *)
Definition terminal_expr e
:=
    ∀ K e', to_val e' = None →
            e = fill K e' →
            K = [] ∧ e' = e.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma stuck_not_val e σ :
    to_val e = None →
    (∀ (κs: list observation) (e': expr) (σ': state) (efs: list expr),
        prim_step e σ κs e' σ' efs → False) →
    stuck e σ.
Proof.
    rewrite /stuck /irreducible.
    intuition.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* This theorem expresses the point of [terminal_expr e]: a terminal_expr is
  stuck if it can't take a head step, because there's *)
Lemma terminal_expr_stuck e σ :
    to_val e = None →
    terminal_expr e →
    (∀ κ e' σ' efs, base_step e σ κ e' σ' efs → False) →
    stuck e σ.
Proof.
    intros Hnot_val Hterminal Hno_base_step.
    apply stuck_not_val; first done; intros * Hstep.
    invc Hstep; simpl in *.
    lazymatch type of Hnot_val with
    | to_val (fill ?K ?e1') = None => edestruct (Hterminal K e1') as [-> ?]; eauto
    end.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Lemma fill_not_val' K e v :
    to_val e = None →
    Val v = fill K e →
    False.
Proof.
    intros H Hfill.
    apply (fill_not_val K) in H; simpl in *.
    rewrite -Hfill /= in H.
    congruence.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
(* to prove [terminal_expr], we work by contradiction in the case where [K] is
  non-empty; to deal with [fill], which is a fold left, we express a non-empty
  list as [l ++ [x]] rather than the usual [x::l]. *)
Lemma list_rev_case {A} (l: list A) :
    l = [] ∨ ∃ x l', l = l' ++ [x].
Proof.
    induction l using rev_ind; eauto.
  Qed.
(* iris_unstable/heap_lang/interpreter.v *)
Ltac ctx_case K Ki
:=
    let K' := fresh "K" in
    destruct (list_rev_case K) as [->| (Ki & K' & ->)]; [by auto|];
    rewrite ?fill_app /=.
(* iris_unstable/heap_lang/interpreter.v *)
Ltac prove_terminal
:=
    lazymatch goal with
    | |- terminal_expr _ =>
      let K := fresh "K" in
      let e := fresh "e" in
      let Ki := fresh "Ki" in
      intros K e; ctx_case K Ki;
      destruct Ki;
      let H := fresh in
      intros ? H; invc H;
      solve [ exfalso; eauto using fill_not_val' ]
    | _ => fail "not a terminal_expr goal"
    end.
(* iris_unstable/heap_lang/interpreter.v *)
(* demo the [prove_terminal] tactic *)
Lemma fill_app_inv v1 v2 :
    terminal_expr (App (Val v1) (Val v2)).
Proof. prove_terminal. Qed.