Commit aa42c811 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

remove is_true

parent 0dc74d32
......@@ -440,10 +440,10 @@ Section denv_spec.
end.
(* Definition denv_wf_interp E m : iProp Σ := ([∗ list] i↦dio ∈ m,
from_option (λ '(DenvItem _ _ dv), ⌜is_true (dval_wf E dv)⌝) True dio)%I.*)
from_option (λ '(DenvItem _ _ dv), ⌜(dval_wf E dv)⌝) True dio)%I.*)
(*Lemma denv_wf_spec (E: known_locs) (m: denv) :
is_true(denv_wf E m) → denv_wf_interp E m.
denv_wf E m → denv_wf_interp E m.
Proof. Admitted.*)
Lemma denv_wf_mono E E' m :
......
......@@ -75,7 +75,7 @@ Section tests_vcg.
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)))].
iExists (dLitV (dLitInt 10)). iSplit; [done|]. iSplit; [done|].
iFrame "Hk"; iSplitR; first done.
simpl. iSplit. done. iIntros "!> Hk Hl".
simpl. iIntros "!> Hk Hl".
iApply ("He" with "Hk"); iIntros "Hk".
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 2)))].
......
......@@ -139,7 +139,7 @@ Section vcg.
E' m' dv,
v = dval_interp E' dv
E `prefix_of` E'
is_true (denv_wf E' m')
(denv_wf E' m')
denv_interp E' m'
wp_interp_sane E' (Φ E' m' dv))%I.
Arguments vcg_wp_unknown : simpl never.
......@@ -392,7 +392,6 @@ Section vcg_spec.
iDestruct "H" as (E' m' dv ->) "(% & % & Hm & Hwp)".
rewrite wp_interp_sane_sound.
iExists E', dv, m'. repeat (iSplit; first done); iFrame.
naive_solver.
Qed.
Lemma vcg_wp_load_correct E m dv Φ :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment