Commit f002e839 authored by Léon Gondelman 's avatar Léon Gondelman

vcg_solver fixed

parent 4193161c
......@@ -28,6 +28,7 @@ Section vcg_continue.
FromKnownLocs (PenvItem l x q v :: Γls) E_old (l :: E_new) | 100.
Proof. done. Qed.
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
......@@ -41,15 +42,15 @@ Section vcg_continue.
envs_entails (Envs Γp Γs_in c) (awp e R Φ).
Proof.
intros Hsplit ->.
rewrite /ListOfMapsto. intros Hpenv [-> Hwf] Hmwf Hgoal.
rewrite /ListOfMapsto. intros Hpenv -> Hwf Hmwf Hgoal.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite environments.envs_entails_eq.
rewrite (vcg_wp_correct R); last done.
rewrite (vcg_wp_correct R); try done.
iIntros (->) "H1 H2".
iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
iIntros (v). iDestruct 1 as (E' dv m' Hpre) "(% & % & % & Hm & Hwp)".
rewrite Hpre.
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm"). done.
rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm").
Qed.
Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps v dv E_old E_new (Φ: known_locs denv dval iProp Σ):
......@@ -75,6 +76,7 @@ Section vcg_continue.
* by left.
* right. by apply Hsplit.
Qed.
End vcg_continue.
Arguments vcg_wp_continuation {_ _ _ _}.
......@@ -90,7 +92,7 @@ Ltac vcg_solver :=
| simpl; reflexivity (* Compute the known locations *)
| apply _ (* Compute the symbolic environment based on known locations *)
| apply _ (* Reify the expression *)
| vm_compute[reflexivity]; try done
| vm_compute[reflexivity]; try done (* Prove that the reified expression is well-formed *)
| done (* Prove that the environment is well-formed *)
| simpl ].
......
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