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

fix tac_vcg_sound proof

parent f515ba5b
......@@ -464,17 +464,27 @@ Section vcg_spec.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
Admitted.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
MapstoListFromEnv Γs_in Γs_out Γls
E = penv_to_known_locs Γls
dcexpr_wf E de
ListOfMapsto Γls E m
IntoDCexpr E e dce
IntoDCexpr E e de
environments.envs_entails (environments.Envs Γp Γs_out c)
(wp_interp_sane E (vcg_wp E m dce R (λ E m dv,
(wp_interp_sane E (vcg_wp E m de R (λ E m dv,
mapsto_wand_list m $ Base (Φ (dval_interp E dv)))))
environments.envs_entails (environments.Envs Γp Γs_in c) (awp e R Φ).
Proof.
Admitted.
rewrite /IntoDCexpr /=. intros Hsplit ->.
rewrite /ListOfMapsto. intros Hwf Hpenv -> Hgoal.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq.
rewrite (vcg_wp_correct R); last done.
iIntros (->) "H1 H2". rewrite wp_interp_sane_sound.
iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
iIntros (v) "H". iDestruct "H" as (E' dv m' Hpre) "(-> & Hm & Hwp)".
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm").
Qed.
End vcg_spec.
......@@ -484,6 +494,7 @@ Ltac vcg_solver :=
eapply tac_vcg_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| (* dcexpr_wf E de *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| simpl ].
| simpl ]; intuition.
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