From 6c3ed7ff305846a6a02cbbbe4ae728d9ac83f75e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9on=20Gondelman?=
Date: Tue, 2 Oct 2018 15:10:10 +0200
Subject: [PATCH] fixed vcg_sp_length lemmas
---
theories/vcgen/vcgen.v | 75 +++++++++++++++++++++++++++---------------
1 file changed, 48 insertions(+), 27 deletions(-)
diff --git a/theories/vcgen/vcgen.v b/theories/vcgen/vcgen.v
index 88aa8ae..c2a9379 100644
--- a/theories/vcgen/vcgen.v
+++ b/theories/vcgen/vcgen.v
@@ -380,30 +380,50 @@ Section vcg_spec.
vcg_sp E ms de n = Some (ms', mNew, dv) →
length ms = length ms'.
Proof.
- Admitted.
- (* revert ms ms' mNew dv. induction de;
- intros ms ms' mNew dv Hsp; simplify_eq/=; eauto.
- - by simplify_option_eq.
- - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout; 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 IHde.
- + 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 IHde1.
- + transitivity (length ms2). by eapply IHde2.
- by eapply denv_delete_full_2_length.
- - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
+ revert ms ms' mNew dv de.
+ induction n.
+ (*Base case*)
+ - intros ms ms' mNew dv de Hsp.
+ destruct de; by simplify_option_eq.
+ (*Induction case*)
+ - intros ms ms' mNew dv de Hsp;
+ destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout.
+ destruct de; simplify_eq /=; try by simplify_option_eq.
+ + (*bind case*)
+ destruct (vcg_sp E ms de1 n)
+ as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
+ destruct (vcg_sp E (mNew1 :: ms1) (dce_subst E s dv1 de2) n)
+ as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
+ destruct ms2; simplify_eq/=. transitivity (length ms1).
+ * by eapply IHn.
+ * apply IHn in Hde2; by simplify_eq/=.
+ + destruct (vcg_sp E ms de n)
+ 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;
simplify_eq/=.
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
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 (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2;
simplify_eq/=.
@@ -412,21 +432,22 @@ Section vcg_spec.
destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=.
transitivity (length ms1); eauto.
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/=.
- by eapply IHde.
- - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
+ by eapply IHn.
+ + destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=.
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
destruct ms2; simplify_eq/=. transitivity (length ms1).
- + by eapply IHde1.
- + apply IHde2 in Hde2; by simplify_eq/=.
- - destruct (vcg_sp E ms de1)
+ * by eapply IHn.
+ * apply IHn in Hde2; by simplify_eq/=.
+ + 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; simplify_eq/=.
transitivity (length ms1); eauto.
- Qed. *)
+ + done.
+ Qed.
Lemma vcg_eval_dexpr_correct E de dv :
vcg_eval_dexpr de = Some dv →
--
GitLab