Commit 1750671e authored by Dan Frumin's avatar Dan Frumin
Browse files

Factor out lemmas for vcg_sp_wf

parent 957e364f
......@@ -814,4 +814,26 @@ Section denv_spec.
denv_interp E m - denv_interp E' m.
Proof. Admitted.
Lemma denv_wf_delete_frac_3 mIn mOut mNew mIn' mOut' mNew' i E q dv :
denv_wf E mIn
Forall (denv_wf E) mOut
denv_wf E mNew
denv_delete_frac_3 i mIn mOut mNew = Some (mIn', mOut', mNew', q, dv)
denv_wf E mIn'
Forall (denv_wf E) mOut'
denv_wf E mNew'
dval_wf E dv.
Proof. Admitted.
Lemma denv_wf_delete_full_3 mIn mOut mNew mIn' mOut' mNew' i E dv :
denv_wf E mIn
Forall (denv_wf E) mOut
denv_wf E mNew
denv_delete_full_3 i mIn mOut mNew = Some (mIn', mOut', mNew', dv)
denv_wf E mIn'
Forall (denv_wf E) mOut'
denv_wf E mNew'
dval_wf E dv.
Proof. Admitted.
End denv_spec.
......@@ -421,17 +421,22 @@ Section vcg_spec.
destruct d as [i|?]; simplify_eq/=.
destruct (denv_delete_frac_3 i mIn1 mOut1 mNew1) as [[[[[mIn2 mOut2] mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (IHde _ _ _ _ _ _ HwfIn HwfOut Hwfde Hsp1) as (?&?&?&?).
repeat split; eauto.
admit. admit. admit. admit.
eapply denv_wf_delete_frac_3 in Hout1; eauto.
destruct Hout1 as (?&?&?&?).
repeat split; eauto using denv_wf_insert.
- destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
destruct dv1 as [dv1|dv1]; destruct dv1; simplify_eq/=.
destruct d as [i|?]; simplify_eq/=.
destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2)) as [[[[mIn3 mOut3] mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
destruct_ands?.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ _ _ HwfIn HwfOut Hwfde1 Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ _ _ HwfIn1 HwfOut1 Hwfde2 Hsp2) as (?&?&?&?).
repeat split; eauto. admit. admit. admit.
eapply denv_wf_delete_full_3 in Hout1; try eassumption.
destruct Hout1 as (?&?&?&?).
repeat split; eauto using denv_wf_insert.
eauto using denv_wf_merge.
- destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E mIn1 mOut1 de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=.
......@@ -455,7 +460,7 @@ Section vcg_spec.
destruct (IHde2 _ _ _ _ _ _ HwfIn1 HwfOut2 Hwfde2 Hsp2) as (?&Hall&?&?).
apply Forall_cons in Hall. destruct Hall.
repeat split; eauto using denv_wf_merge.
Admitted.
Qed.
Lemma vcg_sp_wf E de m mIn mOut mNew dv :
denv_wf E m
......
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