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

fixed vcg_sp_length lemmas

parent 71518adc
...@@ -380,30 +380,50 @@ Section vcg_spec. ...@@ -380,30 +380,50 @@ Section vcg_spec.
vcg_sp E ms de n = Some (ms', mNew, dv) vcg_sp E ms de n = Some (ms', mNew, dv)
length ms = length ms'. length ms = length ms'.
Proof. Proof.
Admitted. revert ms ms' mNew dv de.
(* revert ms ms' mNew dv. induction de; induction n.
intros ms ms' mNew dv Hsp; simplify_eq/=; eauto. (*Base case*)
- by simplify_option_eq. - intros ms ms' mNew dv de Hsp.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout; simplify_eq /=. destruct de; by simplify_option_eq.
destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. (*Induction case*)
destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=. - intros ms ms' mNew dv de Hsp;
transitivity (length ms1). destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout.
+ by eapply IHde. destruct de; simplify_eq /=; try by simplify_option_eq.
+ by eapply denv_delete_frac_2_length. + (*bind case*)
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=. destruct (vcg_sp E ms de1 n)
destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq /=. destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2) n)
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
transitivity (length ms1). destruct ms2; simplify_eq/=. transitivity (length ms1).
+ by eapply IHde1. * by eapply IHn.
+ transitivity (length ms2). by eapply IHde2. * apply IHn in Hde2; by simplify_eq/=.
by eapply denv_delete_full_2_length. + destruct (vcg_sp E ms de n)
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (is_dloc _ _)
as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
transitivity (length ms1).
* by eapply IHn.
* by eapply denv_delete_frac_2_length.
+ destruct (vcg_sp E ms de1)
as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq /=.
destruct (is_dloc _ _)
as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
destruct (vcg_sp E ms1 de2)
as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
transitivity (length ms1).
* by eapply IHn.
* transitivity (length ms2). by eapply IHn.
by eapply denv_delete_full_2_length.
+ destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
simplify_eq/=. simplify_eq/=.
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
transitivity (length ms1); eauto. transitivity (length ms1); eauto.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=. destruct (is_dloc _ _) as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
simplify_eq/=. simplify_eq/=.
...@@ -412,21 +432,22 @@ Section vcg_spec. ...@@ -412,21 +432,22 @@ Section vcg_spec.
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
transitivity (length ms1); eauto. transitivity (length ms1); eauto.
transitivity (length ms2); eauto using denv_delete_full_2_length. transitivity (length ms2); eauto using denv_delete_full_2_length.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=. + destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=.
destruct (dun_op_eval E u dv1); simplify_eq/=. destruct (dun_op_eval E u dv1); simplify_eq/=.
by eapply IHde. by eapply IHn.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2) destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
destruct ms2; simplify_eq/=. transitivity (length ms1). destruct ms2; simplify_eq/=. transitivity (length ms1).
+ by eapply IHde1. * by eapply IHn.
+ apply IHde2 in Hde2; by simplify_eq/=. * apply IHn in Hde2; by simplify_eq/=.
- destruct (vcg_sp E ms de1) + destruct (vcg_sp E ms de1)
as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E ms1 de2) destruct (vcg_sp E ms1 de2)
as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
transitivity (length ms1); eauto. transitivity (length ms1); eauto.
Qed. *) + done.
Qed.
Lemma vcg_eval_dexpr_correct E de dv : Lemma vcg_eval_dexpr_correct E de dv :
vcg_eval_dexpr de = Some dv vcg_eval_dexpr de = Some dv
......
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