Commit 957e364f by Dan Frumin

Progress towards vcg_sp_wf

parent e1f34b73
 ... ... @@ -399,12 +399,76 @@ Section vcg_spec. by iApply denv_stack_reverse. Qed. Lemma denv_wf_stack_merge ms E : Forall (denv_wf E) ms → denv_wf E (denv_stack_merge ms). Proof. induction ms as [|m ms]; simpl; eauto. rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms]. apply denv_wf_merge; eauto. Qed. Lemma vcg_sp_wf' E de mIn mOut mIn' mOut' mNew dv : denv_wf E mIn → Forall (denv_wf E) mOut → dcexpr_wf E de → vcg_sp E mIn mOut de = Some (mIn', mOut', mNew, dv) → denv_wf E mIn' ∧ Forall (denv_wf E) mOut' ∧ denv_wf E mNew ∧ dval_wf E dv . Proof. revert mIn mOut mIn' mOut' mNew dv. induction de; intros mIn mOut mIn' mOut' mNew dv HwfIn HwfOut Hwfde Hsp; simplify_eq/=; eauto. - destruct (vcg_sp E mIn mOut de) 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 (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. - 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/=. 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. - 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/=. 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. apply denv_wf_merge; eauto. eapply (dbin_op_eval_dSome_wf _ dv1 dv2); eauto. - destruct (vcg_sp E mIn mOut de) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (IHde _ _ _ _ _ _ HwfIn HwfOut Hwfde Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1). destruct (dun_op_eval E u dv1) as [|?|?] eqn:Hop; simplify_eq/=. repeat split; eauto. eapply dun_op_eval_dSome_wf; eauto. - destruct (vcg_sp E mIn mOut de1) as [[[[mIn1 mOut1] mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct (vcg_sp E mIn1 (denv_unlock mNew1 :: mOut1) de2) as [[[[mIn2 mOut2] mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. destruct mOut2; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (IHde1 _ _ _ _ _ _ HwfIn HwfOut Hwfde1 Hsp1) as (HwfIn1&HwfOut1&HwfNew1&Hwfdv1). assert (Forall (denv_wf E) (denv_unlock mNew1 :: mOut1)) as HwfOut2. { apply Forall_cons. split; eauto. by apply denv_wf_unlock. } destruct (IHde2 _ _ _ _ _ _ HwfIn1 HwfOut2 Hwfde2 Hsp2) as (?&Hall&?&?). apply Forall_cons in Hall. destruct Hall. repeat split; eauto using denv_wf_merge. Admitted. Lemma vcg_sp_wf E de m mIn mOut mNew dv : denv_wf E m → dcexpr_wf E de → vcg_sp E m [] de = Some (mIn, mOut, mNew, dv) → denv_wf E mIn ∧ denv_wf E (denv_stack_merge mOut) ∧ denv_wf E mNew ∧ dval_wf E dv . Proof. Admitted. Proof. intros Hm Hde Hsp. assert (Forall (denv_wf E) []) as Hout by econstructor. destruct (vcg_sp_wf' E de m [] mIn mOut mNew _ Hm Hout Hde Hsp) as (?&?&?&?). repeat split; eauto. by apply denv_wf_stack_merge. Qed. Lemma vcg_wp_unknown_correct R E m de Φ : 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!