Weakestpre sem completeness

theorem weakestpre_sem_completeness (e : Expr) (σ : State) (φ : Val → Prop)    (Hade : adequate .NotStuck e σ (fun v _ => φ v)) :    ⊢ tpInvIni (TI := TI) -∗      ACG.heap_inv [e] σ -∗      wp ⊤ e (fun v => iprop% ⌜φ v⌝) := by  have Hsafe0 : cfgSafeForking ([e], σ) .doesFork :=    fun {C₂} hreach =>      ⟨fun {e2} hmem => Hade.adequate_not_stuck _ _ e2 rfl hreach hmem,       fun hf => Forking.noConfusion hf⟩  iintro Hini Hheap  iapply LWP.fupd_wp  imod (tpInv_set [e]) $$ Hini with ⟨Hauth, Hfrags⟩  imod (CancelableInvariant.alloc ⊤ completenessN (cfgInv ([e], σ) .doesFork)) $$ [Hauth Hheap]    with ⟨%γ, #Hinv, Hq⟩  · inext    iexists ([e], σ)    iframe Hheap Hauth %Hsafe0    ipureintro    exact .refl  have Hn0 : (completenessN : CoPset) ⊆ ⊤ := fun _ _ => CoPset.mem_full  ihave He0 := BigSepL.bigSepL_singleton $$ Hfrags  imodintro  iapply LWP.wp_fupd  ihave Hccfg : iprop(isCcfg ([e], σ) .doesFork γ) $$ [Hinv]  · unfold isCcfg; itrivial  ihave Hwp := weakestpre_completeness $$ Hccfg Hq He0  iapply LWP.wp_wand $$ Hwp  iintro %v ⟨Hv, %q', Hq', _⟩  imod (CancelableInvariant.acc Hn0) $$ Hinv Hq' with ⟨>⟨%cfg, Hheap, Htpinv, %Hsafe2, %Hreach2⟩, Hq', Hclose2⟩  ihave %Hlu := tpInv_lookup $$ Htpinv Hv  imod Hclose2 $$ [Hheap Htpinv] with -  · inext    iexists cfg    iframe ∗ %  imodintro  ipureintro  obtain ⟨tp2, σ2⟩ := cfg  rcases tp2 with _ | ⟨hd, rest⟩  · simp at Hlu  · simp only [List.getElem?_cons_zero, Option.some.injEq] at Hlu    subst Hlu    exact Hade.adequate_result rest σ2 v Hreach2