diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean index a8f91ef9..7ed1ffc7 100644 --- a/Iris/Iris/BI/Updates.lean +++ b/Iris/Iris/BI/Updates.lean @@ -401,6 +401,10 @@ theorem step_fupd_mask_mono {Eo₁ Eo₂ Ei₁ Ei₂ : CoPset} {P : PROP} refine fupd_frame_r.trans ?_ exact mono emp_sep.1 +theorem step_fupd_mono {Eo Ei : CoPset} {P Q : PROP} : + (Q ⊢ P) → (|={Eo}[Ei]▷=> Q) ⊢ |={Eo}[Ei]▷=> P := + (BIFUpdate.mono <| later_mono <| BIFUpdate.mono ·) + @[rocq_alias step_fupd_intro] theorem step_fupd_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : ▷ P ⊢ |={Eo}[Ei]▷=> P := by @@ -409,6 +413,18 @@ theorem step_fupd_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : _ ⊢ |={Ei}[Ei]▷=> P := mono <| later_mono fupd_intro _ ⊢ |={Eo}[Ei]▷=> P := step_fupd_mask_mono (subset_refl) Ei_Eo +@[rocq_alias step_fupdN_intro] +theorem step_fupdN_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : + ▷^[n] P ⊢ |={Eo}[Ei]▷=>^[n] P := + match n with + | 0 => .rfl + | n+1 => by + simp only [Nat.repeat] + refine .trans (later_laterN n).1 ?_ + refine .trans (step_fupd_intro Ei_Eo) ?_ + refine mono <| later_mono <| mono ?_ + exact step_fupdN_intro Ei_Eo + @[rocq_alias step_fupdN_le] theorem step_fupdN_le {n m : Nat} {Eo Ei : CoPset} {P : PROP} : n ≤ m → Ei ⊆ Eo → (|={Eo}[Ei]▷=>^[n] P) ⊢ |={Eo}[Ei]▷=>^[m] P diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean new file mode 100644 index 00000000..d1e2f7e3 --- /dev/null +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -0,0 +1,187 @@ +/- +Copyright (c) 2026 Fernando Leal. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.ProgramLogic.Lifting +public import Iris.ProgramLogic.EctxiLanguage + +namespace Iris.ProgramLogic + +open Language.Notation EctxLanguage EctxLanguage.Notation + +variable {hlc : outParam Bool} {Expr Ectx State Obs Val} +variable [Λ : EctxLanguage Expr Ectx State Obs Val] +variable {GF : BundledGFunctors} +variable [ι : IrisGS_gen hlc Expr GF] +variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} +variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} + +@[rocq_alias wp_lift_base_step_fupd] +theorem wp_lift_base_step_fupd (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜BaseStep.Reducible (e₁,σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁,σ₁) -->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=> + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + WP e₂ @ s; E {{ Φ }} ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro H + iapply wp_lift_step_fupd h + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ Hσ with ⟨%Hred, H⟩ + imodintro + isplit + · ipure_intro + grind [primStep_reducible_of_baseStep_reducible] + iintro %e₂ %σ₂ %eₜ %Hstep + iapply H $$ %_ %_ %_ + ipure_intro + exact baseStep_of_primStep_of_baseStep_reducible Hred Hstep + +@[rocq_alias wp_lift_base_step] +theorem wp_lift_base_step (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅,E}=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + WP e₂ @ s; E {{ Φ }} ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro H + iapply wp_lift_base_step_fupd h + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ [$] with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %eₜ %Hbstep Hcred !> !> + iapply H $$ %_ %_ %_ %Hbstep Hcred + +@[rocq_alias wp_lift_base_stuck] +theorem wp_lift_base_stuck (h : toVal e = none) : + SubredexesAreValues e → + (∀ σ ns obs' nt, stateInterp σ ns obs' nt ={E,∅}=∗ ⌜BaseStep.Stuck (e,σ)⌝) + ⊢ WP e @ E ? {{ Φ }} := by + iintro %sav_e H + iapply wp_lift_stuck h + iintro %σ %ns %obs' %nt Hσ + imod H $$ Hσ with %H + ipure_intro + exact primStep_stuck_of_baseStep_stuck H sav_e + +@[rocq_alias wp_lift_pure_base_stuck] +theorem wp_lift_pure_base_stuck (h : toVal e = none) : + SubredexesAreValues e → + (∀ σ, BaseStep.Stuck (e,σ)) → + ⊢ WP e @ E ?{{ Φ }} := by + iintro %sav_e %Hstuck + iapply wp_lift_base_stuck h sav_e + iintro %σ %ns %obs' %nt Hσ + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro - + ipure_intro + exact Hstuck _ + +@[rocq_alias wp_lift_atomic_base_step_fupd] +theorem wp_lift_atomic_base_step_fupd (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by + iintro H + iapply wp_lift_atomic_step_fupd (E₂ := E₂) h + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨%Hbred, H⟩ + imodintro + isplit + · ipure_intro; grind only [primStep_reducible_of_baseStep_reducible] + iintro %_ %_ %_ %Hstep + iapply H + ipure_intro + exact baseStep_of_primStep_of_baseStep_reducible Hbred Hstep + +@[rocq_alias wp_lift_atomic_base_step] +theorem wp_lift_atomic_base_step (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro H + iapply wp_lift_atomic_step h + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨%Hbred, H⟩ + imodintro + isplit + · ipure_intro; grind only [primStep_reducible_of_baseStep_reducible] + inext + iintro %e₂ %σ₂ %eₜ %Hstep Hcred + iapply H $$ %_ %_ %_ [] Hcred + ipure_intro + exact baseStep_of_primStep_of_baseStep_reducible Hbred Hstep + +@[rocq_alias wp_lift_atomic_base_step_no_fork_fupd] +theorem wp_lift_atomic_base_step_no_fork_fupd (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ + ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v)) + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by + iintro H + iapply wp_lift_atomic_base_step_fupd (E₂ := E₂) h + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ %_ %_ %_ %_ %_ Hσ₁ with ⟨$, H⟩ + imodintro + iintro %_ %_ %_ %Hbstep Hcred + imod H $$ %_ %_ %_ %Hbstep Hcred with H + iintro !> !> + imod H with ⟨%h, _, _⟩ + subst h + simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] + iframe + itrivial + +@[rocq_alias wp_lift_atomic_base_step_no_fork] +theorem wp_lift_atomic_base_step_no_fork (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v)) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro H + iapply wp_lift_atomic_base_step h + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨$, H⟩ + imodintro + inext + iintro %v2 %σ₂ %eₜ %Hstep Hcred + imod H $$ %_ %_ %_ %Hstep Hcred with ⟨%h, _, _⟩ + subst h + imodintro + simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] + iframe + +@[rocq_alias wp_lift_pure_det_base_step_no_fork] +theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (E₂ : CoPset) (h : toVal e₁ = none) + (Hbred : ∀ σ₁, BaseStep.Reducible (e₁, σ₁)) + (Hpure : ∀ σ₁ obs e₂' σ₂ eₜ', + (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) : + (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro _ + apply wp_lift_pure_det_step_no_fork + · grind [primStep_reducible_of_baseStep_reducible] + · grind only [→ baseStep_of_primStep_of_baseStep_reducible] + +@[rocq_alias wp_lift_pure_det_base_step_no_fork'] +theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] (h : toVal e₁ = none) + (Hbred : ∀ σ₁, BaseStep.Reducible (e₁, σ₁)) + (Hpure : ∀ σ₁ obs e₂' σ₂ eₜ', + (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) : + ▷ (£ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro _ + refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork E h Hbred Hpure + exact step_fupd_intro Std.LawfulSet.subset_refl diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean new file mode 100644 index 00000000..124e1aca --- /dev/null +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -0,0 +1,227 @@ +/- +Copyright (c) 2026 Fernando Leal. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Iris.ProofMode +public import Iris.ProgramLogic.WeakestPre + +public section + +namespace Iris.ProgramLogic + +open Language Language.Notation BI + +variable {hlc : outParam Bool} {Expr State Obs Val} +variable [Λ : Language Expr State Obs Val] +variable {GF : BundledGFunctors} +variable [ι : IrisGS_gen hlc Expr GF] +variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} +variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} + +@[rocq_alias wp_lift_step_fupdN] +theorem wp_lift_step_fupdN (h : toVal e₁ = none) : + (∀ σ₁ ns (obs obs' : List Obs) nt, + stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ + £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + WP e₂ @ s; E {{ Φ }} ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by simp [IProp.ext (wp_unfold (e := e₁)), wp.pre, h] + +@[rocq_alias wp_lift_step_fupd] +theorem wp_lift_step_fupd (h : toVal e₁ = none) : + (∀ σ₁ ns (obs obs' : List Obs) nt, + stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ + £ 1 ={∅}=∗ ▷ |={∅,E}=> + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ + WP e₂ @ s; E {{ Φ }} ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + refine .trans ?_ <| wp_lift_step_fupdN h + iintro Hwp %σ₁ %ns %obs %obs' %nt Hσ + imod Hwp $$ Hσ with ⟨$, Hwp⟩ + iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred + ihave Hcred := lc_weaken 1 (Nat.le_add_left 1 (ι.numLatersPerStep ns)) $$ Hcred + refine .trans ?_ <| step_fupd_mono <| + (laterN_intro _).trans <| step_fupdN_intro Std.LawfulSet.empty_subset + iintro ⟨Hwp, Hcred⟩ + imod Hwp $$ %_ %_ %_ %Hstep Hcred with Hwp + iapply step_fupd_intro Std.LawfulSet.empty_subset + iassumption + +@[rocq_alias wp_lift_stuck] +theorem wp_lift_stuck (h : toVal e = none) : + (∀ σ ns obs nt, stateInterp σ ns obs nt ={E,∅}=∗ ⌜PrimStep.Stuck (e,σ)⌝) + ⊢ WP e @ E ? {{ Φ }} := by + iintro H + rw [IProp.ext wp_unfold] + simp only [wp.pre, h] + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ Hσ with %Hirr + replace ⟨_, Hirr⟩ := Hirr + imodintro + isplit + · ipure_intro; simp [Stuckness.MaybeReducible] + iintro %e₂ %σ₂ %eₜ %Hstep + nomatch Hirr obs e₂ σ₂ eₜ Hstep + +/-! ## Derived lifting lemmas -/ + +@[rocq_alias wp_lift_step] +theorem wp_lift_step (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={∅,E}=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + WP e₂ @ s; E {{ Φ }} ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro H + iapply wp_lift_step_fupd h + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ %_ %_ %_ %_ %_ Hσ with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> + iapply H $$ %_ %_ %_ %Hstep Hcred + +@[rocq_alias wp_lift_pure_step_no_fork] +theorem wp_lift_pure_step_no_fork [Inhabited State] (E₂ : CoPset) : + (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → + (∀ obs σ₁ e₂ σ₂ eₜ, (e₁, σ₁) --> (e₂, σ₂, eₜ) → obs = [] ∧ σ₂ = σ₁ ∧ eₜ = []) → + (|={E₁}[E₂]▷=> ∀ obs e₂ eₜ σ, ⌜(e₁, σ) --> (e₂, σ, eₜ)⌝ -∗ £ 1 -∗ WP e₂ @ s; E₁ {{ Φ }}) + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by + iintro %Hsafe %Hpure H + have Hnone : toVal e₁ = none := by grind [Hsafe default] + iapply wp_lift_step Hnone + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro Hclose + isplit + · ipure_intro; cases s <;> grind -- TODO: Why is `grind [cases S]` not enough? + inext + iintro %e₂ %σ₂ %eₜ %Hstep Hcred + obtain ⟨rfl, rfl, rfl⟩ := Hpure _ _ _ _ _ Hstep + dsimp only [List.nil_append, List.length_nil] + imod ι.stateInterp_mono $$ Hσ with $ + imod Hclose + imod H + imodintro + simp only [Algebra.BigOpL.bigOpL_nil] + ispecialize H $$ %_ %_ %_ %_ %Hstep Hcred + iframe + +@[rocq_alias wp_lift_pure_stuck] +theorem wp_lift_pure_stuck [Inhabited State] : + (∀ σ, PrimStep.Stuck (e,σ)) → + True ⊢ WP e @ E ?{{ Φ }} := by + iintro %Hstuck - + have ⟨toVal_e, _⟩ := Hstuck default + iapply wp_lift_stuck toVal_e + iintro %σ %ns %obs' %nt - + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro - + ipure_intro + apply Hstuck + +@[rocq_alias wp_lift_atomic_step_fupd] +theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) (E₂ : CoPset) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by + iintro H + iapply wp_lift_step_fupd h + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨$, H⟩ + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro Hclose %e₂ %σ₂ %eₜ %Hstep Hcred + imod Hclose with - + imod H $$ %_ %_ %_ %Hstep Hcred with H + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro Hclose !> + imod Hclose with - + imod H with ⟨$, ⟨%v, %h, HQ⟩, $⟩ + iapply wp_value ⟨ToVal.coe_of_toVal_eq_some h⟩ $$ HQ + +@[rocq_alias wp_lift_atomic_step] +theorem wp_lift_atomic_step (h : toVal e₁ = none) : + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ + (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro H + iapply wp_lift_atomic_step_fupd (E₂ := E) h + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ [$] with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> + iapply H $$ %_ %_ %_ %Hstep Hcred + +@[rocq_alias wp_lift_pure_det_step_no_fork] +theorem wp_lift_pure_det_step_no_fork [Inhabited State] (E₂ : CoPset) + (Hsafe : ∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) + (Hpuredet : ∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) --> (e₂', σ₂, eₜ') → + obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) : + (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro H + iapply wp_lift_pure_step_no_fork E₂ Hsafe (by grind only) + iapply step_fupd_wand $$ H + iintro H + iintro %obs %e' %eₜ' %σ %aux + obtain ⟨rfl, _, rfl, rfl⟩ := Hpuredet _ _ _ _ _ aux + iassumption + +@[rocq_alias wp_pure_step_fupd] +theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset) + (Hexec : PureExec φ n e₁ e₂) (Hφ : φ) : + (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro Hwp + replace Hexec := Hexec.pureExec Hφ + induction Hexec using Relation.Iterate.head_induction_on with + | rfl => + simp only [Nat.repeat] + rw (occs := [2]) [IProp.ext fupd_wp_iff] + icases lc_zero with >Hz + iapply Hwp $$ Hz + | @head n e₁ e₃ _ _ IH => + obtain ⟨Hsafe, Hdet⟩ := ‹e₁ -ᵖ-> e₃› + iapply wp_lift_pure_det_step_no_fork E₂ (e₂ := e₃) ?Hred (by grind) + case Hred => + intro σ + have _ : PrimStep.Reducible (e₁, σ) := by grind only [reducible_of_reducibleNoObs] + grind [cases Stuckness] + simp only [Nat.repeat] + iapply step_fupd_wand $$ Hwp + iintro Hwp Hone + iapply IH + iapply step_fupdN_wand $$ Hwp + iintro Hwp Hc + iapply Hwp $$ [Hone Hc] + iapply lc_split + iframe + +@[rocq_alias wp_pure_step_later] +theorem wp_pure_step_later [Inhabited State] (Hexec : PureExec φ n e₁ e₂) (Hφ : φ) : + ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + refine .trans ?_ (wp_pure_step_fupd E Hexec Hφ) + suffices Hwp : ∀ (P : IProp GF), ▷^[n] P ⊢ |={E}▷=>^[n] P by iapply Hwp + intro P + clear Hexec + induction n with + | zero => exact .rfl + | succ n IH => + simp only [Nat.repeat] + rw [IProp.ext <| later_laterN n] + refine (later_mono IH).trans ?_ + exact step_fupd_intro Std.LawfulSet.subset_refl