phanerozoic/Coq-Iris huggingface dataset:
(* iris/program_logic/ectx_language.v *)
Definition base_reducible_no_obs (e : expr Λ) (σ : state Λ)
:=
    ∃ e' σ' efs, base_step e σ [] e' σ' efs.
(* iris/program_logic/ectx_language.v *)
Definition base_irreducible (e : expr Λ) (σ : state Λ)
:=
    ∀ κ e' σ' efs, ¬base_step e σ κ e' σ' efs.
(* iris/program_logic/ectx_language.v *)
Definition base_stuck (e : expr Λ) (σ : state Λ)
:=
    to_val e = None ∧ base_irreducible e σ.
(* iris/program_logic/ectx_language.v *)
(* All non-value redexes are at the root.  In other words, all sub-redexes are
     values. *)
Definition sub_redexes_are_values (e : expr Λ)
:=
    ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
(* iris/program_logic/ectx_language.v *)
Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
      (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop
:=
    Ectx_step K e1' e2' :
      e1 = fill K e1' → e2 = fill K e2' →
      base_step e1' σ1 κ e2' σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
(* iris/program_logic/ectx_language.v *)
Lemma Ectx_step' K e1 σ1 κ e2 σ2 efs :
    base_step e1 σ1 κ e2 σ2 efs → prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
Proof. econstructor; eauto. Qed.
(* iris/program_logic/ectx_language.v *)
Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
Proof.
    split.
    - apply ectx_language_mixin.
    - apply ectx_language_mixin.
    - intros ?????? [??? -> -> ?%val_base_stuck].
      apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
  Qed.
(* iris/program_logic/ectx_language.v *)
Canonical ectx_lang : language
:= Language ectx_lang_mixin.
(* iris/program_logic/ectx_language.v *)
Definition base_atomic (a : atomicity) (e : expr Λ) : Prop
:=
    ∀ σ κ e' σ' efs,
      base_step e σ κ e' σ' efs →
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
(* iris/program_logic/ectx_language.v *)
Lemma base_reducible_no_obs_reducible e σ :
    base_reducible_no_obs e σ → base_reducible e σ.
Proof. intros (?&?&?&?). eexists. eauto. Qed.
(* iris/program_logic/ectx_language.v *)
Lemma not_base_reducible e σ : ¬base_reducible e σ ↔ base_irreducible e σ.
Proof. unfold base_reducible, base_irreducible. naive_solver. Qed.
(* iris/program_logic/ectx_language.v *)
(* The decomposition into base redex and context is unique.

      In all sensible instances, [comp_ectx K' empty_ectx] will be the same as
      [K'], so the conclusion is [K = K' ∧ e = e'], but we do not require a law
      to actually prove that so we cannot use that fact here. *)
Lemma base_redex_unique K K' e e' σ :
    fill K e = fill K' e' →
    base_reducible e σ →
    base_reducible e' σ →
    K = comp_ectx K' empty_ectx ∧ e = e'.
Proof.
    intros Heq (κ & e2 & σ2 & efs & Hred) (κ' & e2' & σ2' & efs' & Hred').
    edestruct (step_by_val K' K e' e) as [K'' HK];
      [by eauto using val_base_stuck..|].
    subst K. move: Heq. rewrite -fill_comp. intros <-%(inj (fill _)).
    destruct (base_ctx_step_val _ _ _ _ _ _ _ Hred') as [[]%not_eq_None_Some|HK''].
    { by eapply val_base_stuck. }
    subst K''. rewrite fill_empty. done.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_prim_step e1 σ1 κ e2 σ2 efs :
    base_step e1 σ1 κ e2 σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_step_not_stuck e σ κ e' σ' efs : base_step e σ κ e' σ' efs → not_stuck e σ.
Proof. rewrite /not_stuck /reducible /=. eauto 10 using base_prim_step. Qed.
(* iris/program_logic/ectx_language.v *)
Lemma fill_prim_step K e1 σ1 κ e2 σ2 efs :
    prim_step e1 σ1 κ e2 σ2 efs → prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
Proof.
    destruct 1 as [K' e1' e2' -> ->].
    rewrite !fill_comp. by econstructor.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma fill_reducible K e σ : reducible e σ → reducible (fill K e) σ.
Proof.
    intros (κ&e'&σ'&efs&?). exists κ, (fill K e'), σ', efs.
    by apply fill_prim_step.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma fill_reducible_no_obs K e σ : reducible_no_obs e σ → reducible_no_obs (fill K e) σ.
Proof.
    intros (e'&σ'&efs&?). exists (fill K e'), σ', efs.
    by apply fill_prim_step.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_prim_reducible e σ : base_reducible e σ → reducible e σ.
Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply base_prim_step. Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_prim_fill_reducible e K σ :
    base_reducible e σ → reducible (fill K e) σ.
Proof. intro. by apply fill_reducible, base_prim_reducible. Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_prim_reducible_no_obs e σ : base_reducible_no_obs e σ → reducible_no_obs e σ.
Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply base_prim_step. Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_prim_irreducible e σ : irreducible e σ → base_irreducible e σ.
Proof.
    rewrite -not_reducible -not_base_reducible. eauto using base_prim_reducible.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_prim_fill_reducible_no_obs e K σ :
    base_reducible_no_obs e σ → reducible_no_obs (fill K e) σ.
Proof. intro. by apply fill_reducible_no_obs, base_prim_reducible_no_obs. Qed.
(* iris/program_logic/ectx_language.v *)
Lemma prim_base_reducible e σ :
    reducible e σ → sub_redexes_are_values e → base_reducible e σ.
Proof.
    intros (κ&e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
    assert (K = empty_ectx) as -> by eauto 10 using val_base_stuck.
    rewrite fill_empty /base_reducible; eauto.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma prim_base_irreducible e σ :
    base_irreducible e σ → sub_redexes_are_values e → irreducible e σ.
Proof.
    rewrite -not_reducible -not_base_reducible. eauto using prim_base_reducible.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_stuck_stuck e σ :
    base_stuck e σ → sub_redexes_are_values e → stuck e σ.
Proof.
    intros [] ?. split; first done.
    by apply prim_base_irreducible.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma ectx_language_atomic a e :
    base_atomic a e → sub_redexes_are_values e → Atomic a e.
Proof.
    intros Hatomic_step Hatomic_fill σ κ e' σ' efs [K e1' e2' -> -> Hstep].
    assert (K = empty_ectx) as -> by eauto 10 using val_base_stuck.
    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_reducible_prim_step_ctx K e1 σ1 κ e2 σ2 efs :
    base_reducible e1 σ1 →
    prim_step (fill K e1) σ1 κ e2 σ2 efs →
    ∃ e2', e2 = fill K e2' ∧ base_step e1 σ1 κ e2' σ2 efs.
Proof.
    intros (κ'&e2''&σ2''&efs''&HhstepK) [K' e1' e2' HKe1 -> Hstep].
    edestruct (step_by_val K) as [K'' ?];
      eauto using val_base_stuck; simplify_eq/=.
    rewrite -fill_comp in HKe1; simplify_eq.
    exists (fill K'' e2'). rewrite fill_comp; split; first done.
    apply base_ctx_step_val in HhstepK as [[v ?]|?]; simplify_eq.
    { apply val_base_stuck in Hstep; simplify_eq. }
    by rewrite !fill_empty.
  Qed.
(* iris/program_logic/ectx_language.v *)
Lemma base_reducible_prim_step e1 σ1 κ e2 σ2 efs :
    base_reducible e1 σ1 →
    prim_step e1 σ1 κ e2 σ2 efs →
    base_step e1 σ1 κ e2 σ2 efs.
Proof.
    intros.
    edestruct (base_reducible_prim_step_ctx empty_ectx) as (?&?&?);
      rewrite ?fill_empty; eauto.
    by simplify_eq; rewrite fill_empty.
  Qed.
(* iris/program_logic/ectx_language.v *)
(* Every evaluation context is a context. *)
Instance ectx_lang_ctx K : LanguageCtx (fill K).
Proof.
    split; simpl.
    - eauto using fill_not_val.
    - intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
      by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
    - intros e1 σ1 κ e2 σ2 efs Hnval [K'' e1'' e2'' Heq1 -> Hstep].
      destruct (step_by_val K K'' e1 e1'' σ1 κ e2'' σ2 efs) as [K' ->]; eauto.
      rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
      exists (fill K' e2''); rewrite -fill_comp; split; auto.
      econstructor; eauto.
  Qed.
(* iris/program_logic/ectx_language.v *)
Record pure_base_step (e1 e2 : expr Λ)
:= {
    pure_base_step_safe σ1 : base_reducible_no_obs e1 σ1;
    pure_base_step_det σ1 κ e2' σ2 efs :
      base_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []
  }.
(* iris/program_logic/ectx_language.v *)
Lemma pure_base_step_pure_step e1 e2 : pure_base_step e1 e2 → pure_step e1 e2.
Proof.
    intros [Hp1 Hp2]. split.
    - intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
      eexists e2', σ2, efs. by apply base_prim_step.
    - intros σ1 κ e2' σ2 efs ?%base_reducible_prim_step; eauto using base_reducible_no_obs_reducible.
  Qed.
(* iris/program_logic/ectx_language.v *)
(* This is not an instance because HeapLang's [wp_pure] tactic already takes
      care of handling the evaluation context.  So the instance is redundant.
      If you are defining your own language and your [wp_pure] works
      differently, you might want to specialize this lemma to your language and
      register that as an instance. *)
Lemma pure_exec_fill K φ n e1 e2 :
    PureExec φ n e1 e2 →
    PureExec φ n (fill K e1) (fill K e2).
Proof. apply: pure_exec_ctx. Qed.
(* iris/program_logic/ectx_language.v *)
Coercion ectx_lang : ectxLanguage >-> language.
(* iris/program_logic/ectx_language.v *)
(* This definition makes sure that the fields of the [language] record do not
refer to the projections of the [ectxLanguage] record but to the actual fields
of the [ectxLanguage] record. This is crucial for canonical structure search to
work.

Note that this trick no longer works when we switch to canonical projections
because then the pattern match [let '...] will be desugared into projections. *)
Definition LanguageOfEctx (Λ : ectxLanguage) : language
:=
  let '@EctxLanguage E V C St K of_val to_val empty comp fill base mix := Λ in
  @Language E V St K of_val to_val _
    (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill base mix)).
(* iris/program_logic/ectx_lifting.v *)
Definition reducible_not_val_inhabitant e
:= reducible_not_val e inhabitant.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_base_step_fupd {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
    ⌜base_reducible e1 σ1⌝ ∗
    ∀ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=>
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E {{ Φ }} ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 ns κ κs nt) "Hσ".
  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
  iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs ?).
  iApply "H"; eauto.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_base_step {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
    ⌜base_reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={∅,E}=∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E {{ Φ }} ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_base_step_fupd; [done|]. iIntros (?????) "?".
  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "Hcred !> !>". by iApply "H".
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_base_stuck E Φ e :
  to_val e = None →
  sub_redexes_are_values e →
  (∀ σ ns κs nt, state_interp σ ns κs nt ={E,∅}=∗ ⌜base_stuck e σ⌝)
  ⊢ WP e @ E ?{{ Φ }}.
Proof.
  iIntros (??) "H". iApply wp_lift_stuck; first done.
  iIntros (σ ns κs nt) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_pure_base_stuck E Φ e :
  to_val e = None →
  sub_redexes_are_values e →
  (∀ σ, base_stuck e σ) →
  ⊢ WP e @ E ?{{ Φ }}.
Proof using Hinh.
  iIntros (?? Hstuck). iApply wp_lift_base_stuck; [done|done|].
  iIntros (σ ns κs nt) "_". iApply fupd_mask_intro; by auto with set_solver.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_atomic_base_step_fupd {s E1 E2 Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
    ⌜base_reducible e1 σ1⌝ ∗
    ∀ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={E1}[E2]▷=∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      from_option Φ False (to_val e2) ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E1 {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
  iApply "H"; eauto.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_atomic_base_step {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
    ⌜base_reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={E}=∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      from_option Φ False (to_val e2) ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
  iApply "H"; eauto.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_atomic_base_step_no_fork_fupd {s E1 E2 Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
    ⌜base_reducible e1 σ1⌝ ∗
    ∀ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={E1}[E2]▷=∗
      ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt ∗ from_option Φ False (to_val e2))
  ⊢ WP e1 @ s; E1 {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_base_step_fupd; [done|].
  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iIntros (v2 σ2 efs Hstep) "Hcred".
  iMod ("H" $! v2 σ2 efs with "[# //] Hcred") as "H".
  iIntros "!> !>". iMod "H" as "(-> & ? & ?) /=". by iFrame.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_atomic_base_step_no_fork {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
    ⌜base_reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={E}=∗
      ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt ∗ from_option Φ False (to_val e2))
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_base_step; eauto.
  iIntros (σ1 ns κ κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iNext; iIntros (v2 σ2 efs Hstep) "Hcred".
  iMod ("H" $! v2 σ2 efs with "[//] Hcred") as "(-> & ? & ?) /=". by iFrame.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_pure_det_base_step_no_fork {s E E' Φ} e1 e2 :
  to_val e1 = None →
  (∀ σ1, base_reducible e1 σ1) →
  (∀ σ1 κ e2' σ2 efs',
    base_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
  (|={E}[E']▷=> £ 1 -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
  intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2); eauto.
  destruct s; by auto.
Qed.
(* iris/program_logic/ectx_lifting.v *)
Lemma wp_lift_pure_det_base_step_no_fork' {s E Φ} e1 e2 :
  to_val e1 = None →
  (∀ σ1, base_reducible e1 σ1) →
  (∀ σ1 κ e2' σ2 efs',
    base_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
  ▷ (£ 1 -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
  intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_base_step_no_fork //.
  rewrite -step_fupd_intro //.
Qed.
(* iris/program_logic/language.v *)
Record LanguageMixin
:= {
    mixin_to_of_val v : to_val (of_val v) = Some v;
    mixin_of_to_val e v : to_val e = Some v → of_val v = e;
    mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None
  }.
(* iris/program_logic/language.v *)
Structure language
:= Language {
  expr : Type;
  val : Type;
  state : Type;
  observation : Type;
  of_val : val → expr;
  to_val : expr → option val;
  prim_step : expr → state → list observation → expr → state → list expr → Prop;
  language_mixin : LanguageMixin of_val to_val prim_step
}.
(* iris/program_logic/language.v *)
Canonical stateO Λ
:= leibnizO (state Λ).
(* iris/program_logic/language.v *)
Canonical valO Λ
:= leibnizO (val Λ).
(* iris/program_logic/language.v *)
Canonical exprO Λ
:= leibnizO (expr Λ).
(* iris/program_logic/language.v *)
Definition cfg (Λ : language)
:= (list (expr Λ) * state Λ)%type.
(* iris/program_logic/language.v *)
Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ)
:= {
  fill_not_val e :
    to_val e = None → to_val (K e) = None;
  fill_step e1 σ1 κ e2 σ2 efs :
    prim_step e1 σ1 κ e2 σ2 efs →
    prim_step (K e1) σ1 κ (K e2) σ2 efs;
  fill_step_inv e1' σ1 κ e2 σ2 efs :
    to_val e1' = None → prim_step (K e1') σ1 κ e2 σ2 efs →
    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
}.
(* iris/program_logic/language.v *)
Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Proof. constructor; naive_solver. Qed.
(* iris/program_logic/language.v *)
Inductive atomicity
:= StronglyAtomic | WeaklyAtomic.
(* iris/program_logic/language.v *)
Definition stuckness_to_atomicity (s : stuckness) : atomicity
:=
  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
(* iris/program_logic/language.v *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof. apply language_mixin. Qed.
(* iris/program_logic/language.v *)
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof. apply language_mixin. Qed.
(* iris/program_logic/language.v *)
Lemma val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None.
Proof. apply language_mixin. Qed.
(* iris/program_logic/language.v *)
Definition reducible (e : expr Λ) (σ : state Λ)
:=
    ∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
(* iris/program_logic/language.v *)
(* Total WP only permits reductions without observations *)
Definition reducible_no_obs (e : expr Λ) (σ : state Λ)
:=
    ∃ e' σ' efs, prim_step e σ [] e' σ' efs.
(* iris/program_logic/language.v *)
Definition irreducible (e : expr Λ) (σ : state Λ)
:=
    ∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
(* iris/program_logic/language.v *)
Definition stuck (e : expr Λ) (σ : state Λ)
:=
    to_val e = None ∧ irreducible e σ.
(* iris/program_logic/language.v *)
Definition not_stuck (e : expr Λ) (σ : state Λ)
:=
    is_Some (to_val e) ∨ reducible e σ.
(* iris/program_logic/language.v *)
(* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
     invariants when WP ensures safety, i.e., programs never can get stuck.  We
     have an example in lambdaRust of an expression that is atomic in this
     sense, but not in the stronger sense defined below, and we have to be able
     to open invariants around that expression.  See `CasStuckS` in
     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).

     [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure
     safety, we need a stronger form of atomicity.  With the above definition,
     in case `e` reduces to a stuck non-value, there is no proof that the
     invariants have been established again. *)
Class Atomic (a : atomicity) (e : expr Λ) : Prop
:=
    atomic σ e' κ σ' efs :
      prim_step e σ κ e' σ' efs →
      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
(* iris/program_logic/language.v *)
Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop
:=
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
       ρ1 = (t1 ++ e1 :: t2, σ1) →
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
       prim_step e1 σ1 κ e2 σ2 efs →
       step ρ1 κ ρ2.
(* iris/program_logic/language.v *)
Inductive nsteps : nat → cfg Λ → list (observation Λ) → cfg Λ → Prop
:=
    | nsteps_refl ρ :
       nsteps 0 ρ [] ρ
    | nsteps_l n ρ1 ρ2 ρ3 κ κs :
       step ρ1 κ ρ2 →
       nsteps n ρ2 κs ρ3 →
       nsteps (S n) ρ1 (κ ++ κs) ρ3.
(* iris/program_logic/language.v *)
Definition erased_step (ρ1 ρ2 : cfg Λ)
:= ∃ κ, step ρ1 κ ρ2.
(* iris/program_logic/language.v *)
(* [rtc erased_step] and [nsteps] encode the same thing, just packaged
      in a different way. *)
Lemma erased_steps_nsteps ρ1 ρ2 :
    rtc erased_step ρ1 ρ2 ↔ ∃ n κs, nsteps n ρ1 κs ρ2.
Proof.
    split.
    - induction 1; firstorder eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
    - intros (n & κs & Hsteps). unfold erased_step.
      induction Hsteps; eauto using rtc_refl, rtc_l.
  Qed.
(* iris/program_logic/language.v *)
Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
Proof. intros <-. by rewrite to_of_val. Qed.
(* iris/program_logic/language.v *)
Lemma not_reducible e σ : ¬reducible e σ ↔ irreducible e σ.
Proof. unfold reducible, irreducible. naive_solver. Qed.
(* iris/program_logic/language.v *)
Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.
(* iris/program_logic/language.v *)
Lemma reducible_no_obs_reducible e σ : reducible_no_obs e σ → reducible e σ.
Proof. intros (?&?&?&?); eexists; eauto. Qed.
(* iris/program_logic/language.v *)
Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
(* iris/program_logic/language.v *)
Instance of_val_inj : Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
(* iris/program_logic/language.v *)
Lemma not_not_stuck e σ : ¬not_stuck e σ ↔ stuck e σ.
Proof.
    rewrite /stuck /not_stuck -not_eq_None_Some -not_reducible.
    destruct (decide (to_val e = None)); naive_solver.
  Qed.
(* iris/program_logic/language.v *)
Lemma strongly_atomic_atomic e a :
    Atomic StronglyAtomic e → Atomic a e.
Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
(* iris/program_logic/language.v *)
Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
    reducible e σ → reducible (K e) σ.
Proof. unfold reducible in *. naive_solver eauto using fill_step. Qed.
(* iris/program_logic/language.v *)
Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ :
    to_val e = None → reducible (K e) σ → reducible e σ.
Proof.
    intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
(* iris/program_logic/language.v *)
Lemma reducible_no_obs_fill `{!@LanguageCtx Λ K} e σ :
    reducible_no_obs e σ → reducible_no_obs (K e) σ.
Proof. unfold reducible_no_obs in *. naive_solver eauto using fill_step. Qed.
(* iris/program_logic/language.v *)
Lemma reducible_no_obs_fill_inv `{!@LanguageCtx Λ K} e σ :
    to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ.
Proof.
    intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
(* iris/program_logic/language.v *)
Lemma irreducible_fill `{!@LanguageCtx Λ K} e σ :
    to_val e = None → irreducible e σ → irreducible (K e) σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill_inv. Qed.
(* iris/program_logic/language.v *)
Lemma irreducible_fill_inv `{!@LanguageCtx Λ K} e σ :
    irreducible (K e) σ → irreducible e σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
(* iris/program_logic/language.v *)
Lemma not_stuck_fill_inv K `{!@LanguageCtx Λ K} e σ :
    not_stuck (K e) σ → not_stuck e σ.
Proof.
    rewrite /not_stuck -!not_eq_None_Some. intros [?|?].
    - auto using fill_not_val.
    - destruct (decide (to_val e = None)); eauto using reducible_fill_inv.
  Qed.
(* iris/program_logic/language.v *)
Lemma stuck_fill `{!@LanguageCtx Λ K} e σ :
    stuck e σ → stuck (K e) σ.
Proof. rewrite -!not_not_stuck. eauto using not_stuck_fill_inv. Qed.
(* iris/program_logic/language.v *)
Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
    t1 ≡ₚ t1' → step (t1,σ1) κ (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) κ (t2',σ2).
Proof.
    intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
    move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
    intros (tl'&tr'&->&Ht)%Permutation_cons_inv_r.
    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
    by rewrite -!Permutation_middle !assoc_L Ht.
  Qed.