Commit 1621092c authored by Robbert Krebbers's avatar Robbert Krebbers

Hacking.

parent f89f81a0
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
From iris.proofmode Require Import coq_tactics.
Section vcg.
Context `{heapG Σ}.
......@@ -389,10 +388,10 @@ Section vcg.
Lemma tac_vcg_opt_sound Δ e Φ E t :
WpQuote E e (λ dv, Base (Φ (dval_interp E dv))) t
envs_entails Δ (wp_interp_sane E (optimize None t))
envs_entails Δ (WP e {{ Φ }}).
coq_tactics.envs_entails Δ (wp_interp_sane E (optimize None t))
coq_tactics.envs_entails Δ (WP e {{ Φ }}).
Proof.
rewrite /WpQuote /= envs_entails_eq=> Hquote ->.
rewrite /WpQuote /= coq_tactics.envs_entails_eq=> Hquote ->.
rewrite wp_interp_sane_sound vcg_opt_sound Hquote. apply wp_mono=> v.
by iDestruct 1 as (dv ->) "?".
Qed.
......@@ -404,11 +403,8 @@ Section vcg.
end.
Definition exhale_list_interp
(E : list loc) (pl : list (nat * dval)) (P : iProp Σ) : iProp Σ :=
match pl with
| [] => P
| _ => (([ list] lw pl, dloc_interp E (dLoc lw.1) dval_interp E lw.2) - P)
end%I.
(E : list loc) (pl : list (nat * dval)) : iProp Σ :=
([ list] lw pl, dloc_interp E (dLoc lw.1) dval_interp E lw.2)%I.
(*Fixpoint exhale_list_interp'
(E : list loc) (s : list (nat * dval)) (P : iProp Σ) : iProp Σ :=
......@@ -418,19 +414,13 @@ Section vcg.
| [] => P
end%I.*)
Global Instance exhale_list_interp_mono' E s :
Proper (() ==> ()) (exhale_list_interp E s).
Proof. induction s; solve_proper. Qed.
Lemma vcg_exhale_list_sound' E s t :
wp_interp E (exhale_list s t) - exhale_list_interp E s (wp_interp E t).
wp_interp E (exhale_list s t) - exhale_list_interp E s - wp_interp E t.
Proof.
unfold exhale_list_interp.
induction s as [| [i w] s']; simpl.
- iIntros "$".
- iIntros "H". iIntros "[Hl H2]".
iSpecialize ("H" with "Hl").
rewrite IHs'. destruct s'; by iApply "H".
- by iIntros "$ _".
- iIntros "H [H1 H2]". iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
Qed.
Fixpoint find_and_remove (pl : list (nat * dval)) (dl: dloc) :
......
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