Commit 6b695042 authored by Dan Frumin's avatar Dan Frumin

simpl_subst in vcgen

(Fixes #4)
parent 148d00ca
...@@ -10,24 +10,20 @@ Import env_notations. ...@@ -10,24 +10,20 @@ Import env_notations.
Section vcg_continue. Section vcg_continue.
Context `{amonadG Σ}. Context `{amonadG Σ}.
Class FromKnownLocs (Γls : penv) (E_old : known_locs) (E_new : known_locs) := Class FromKnownLocs (Γls : penv) (E_old : known_locs) (E_new : known_locs).
from_known_locs: True. (*dom Γls ⊂ (elem_of E_old) disj_Union (elem_of E) *) (*dom Γls ⊂ (elem_of E_old) disj_Union (elem_of E) *)
Global Instance from_known_locs_Nil E_old: Global Instance from_known_locs_Nil E_old:
FromKnownLocs [] E_old []. FromKnownLocs [] E_old [].
Proof. done. Qed.
Global Instance from_known_locs_old_cons Γls E_old E_new x q v l i: Global Instance from_known_locs_old_cons Γls E_old E_new x q v l i:
LocLookup E_old l i LocLookup E_old l i
FromKnownLocs Γls E_old E_new FromKnownLocs Γls E_old E_new
FromKnownLocs (PenvItem l x q v :: Γls) E_old E_new. FromKnownLocs (PenvItem l x q v :: Γls) E_old E_new.
Proof. done. Qed.
Global Instance from_known_locs_new_cons Γls E_old E_new x q v l: Global Instance from_known_locs_new_cons Γls E_old E_new x q v l:
FromKnownLocs Γls E_old E_new FromKnownLocs Γls E_old E_new
FromKnownLocs (PenvItem l x q v :: Γls) E_old (l :: E_new) | 100. 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 : Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
MapstoListFromEnv Γs_in Γs_out Γls MapstoListFromEnv Γs_in Γs_out Γls
...@@ -94,7 +90,7 @@ Ltac vcg_solver := ...@@ -94,7 +90,7 @@ Ltac vcg_solver :=
| apply _ (* Reify the expression *) | apply _ (* Reify the expression *)
| vm_compute[reflexivity]; try done (* Prove that the reified expression is well-formed *) | vm_compute[reflexivity]; try done (* Prove that the reified expression is well-formed *)
| done (* Prove that the environment is well-formed *) | done (* Prove that the environment is well-formed *)
| simpl ]. | simpl; simpl_subst ].
Ltac vcg_continue := Ltac vcg_continue :=
eapply tac_exists_known_locs; eapply tac_exists_known_locs;
......
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