total_adequacy.v 651 Bytes
Newer Older
1 2 3 4 5 6
From iris.program_logic Require Export total_adequacy.
From iris.heap_lang Require Export adequacy.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".

7 8
(* TODO (MR) re-introduce lemma after we prove twp_total *)
(*
9 10
Definition heap_total Σ `{heapPreG Σ} s e σ φ :
  (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
11
  sn erased_step ([e], σ).
12
Proof.
13
  intros Hwp; eapply (twp_total _ _) with (κs := []); iIntros (?) "".
14
  iMod (gen_heap_init σ) as (?) "Hh".
15
  iModIntro. iExists (fun σ _ => gen_heap_ctx σ); iFrame.
16 17
  iApply (Hwp (HeapG _ _ _)).
Qed.
18
*)