proposition: Lemma ExecToSeqExec': forall p h s, CExec.StepStar.step_star (CExec.init p) h s -> exists h' s', SExec.StepStar.step_star (SExec.init) h' s' /\ h' = CExec.eff_hist h /\ forall n k, store (CExec.alg_state (CExec.node_states s n)) k = s' n k.
proof: Proof. intros. remember (CExec.init p) as s0. induction H. exists nil. eexists. split_all. constructor. reflexivity. intros. subst s. reflexivity. depremise IHstep_star. assumption. destruct IHstep_star as [h' [s' [N1 [N2 N3]]]]. exists (h' ++ [CExec.eff l]). inversion H0. exists (override s' n (override (s' n) k v)). split_all. apply SExec.StepStar.step_star_app_one. eexists. split_all. eassumption. simpl. unfold SExec.StepStarArgs.step. assert (A: s' = override s' n (s' n)). apply functional_extensionality. intro n'. destruct (eq_nat_dec n n'). subst n'. simpl_override. reflexivity. simpl_override. reflexivity. rewrite A at 1. apply SExec.put_step. simpl. subv h'. rewrite exec_eff_app. f_equal. intros. simpl. destruct (eq_nat_dec n n0). subst n0. simpl_override. simpl_override. destruct (eq_nat_dec k k0). subst k0. simpl_override. simpl_override. reflexivity. simpl_override. simpl_override. specialize (N3 n k0). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. simpl_override. specialize (N3 n0 k0). subv_in s2 N3. simpl_override_in N3. assumption. exists (override s' n (s' n)). split_all. apply SExec.StepStar.step_star_app_one. eexists. split_all. eassumption. simpl. unfold SExec.StepStarArgs.step. assert (A: s' = override s' n (s' n)). apply functional_extensionality. intro n'. destruct (eq_nat_dec n n'). subst n'. simpl_override. reflexivity. simpl_override. reflexivity. rewrite A at 1. subv v'. specialize (N3 n k). subv_in s2 N3. simpl_override_in N3. rewrite N3. apply SExec.get_step. simpl. subv h'. rewrite exec_eff_app. f_equal. intros. simpl. destruct (eq_nat_dec n n0). subst n0. simpl_override. simpl_override. specialize (N3 n k0). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. simpl_override. specialize (N3 n0 k0). subv_in s2 N3. simpl_override_in N3. assumption. simpl. exists (override s' n (override (s' n) k v)). split_all. apply SExec.StepStar.step_star_app_one. eexists. split_all. eassumption. unfold SExec.StepStarArgs.step. assert (A: s' = override s' n (s' n)). apply functional_extensionality. intro n'. destruct (eq_nat_dec n n'). subst n'. simpl_override. reflexivity. simpl_override. reflexivity. rewrite A at 1. apply SExec.put_step. simpl. subv h'. rewrite exec_eff_app. f_equal. intros. destruct (eq_nat_dec n n0). subst n0. simpl_override. simpl_override. destruct (eq_nat_dec k k0). subst k0. simpl_override. simpl_override. reflexivity. simpl_override. simpl_override. specialize (N3 n k0). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. simpl_override. specialize (N3 n0 k0). subv_in s2 N3. simpl_override_in N3. assumption. exists (override s' n (s' n)). split_all. apply SExec.StepStar.step_star_app_one. eexists. split_all. eassumption. simpl. unfold SExec.StepStarArgs.step. assert (A: s' = override s' n (s' n)). apply functional_extensionality. intro n'. destruct (eq_nat_dec n n'). subst n'. simpl_override. reflexivity. simpl_override. reflexivity. rewrite A at 1. constructor. simpl. subv h'. rewrite exec_eff_app. f_equal. intros. simpl. destruct (eq_nat_dec n n0). subst n0. simpl_override. simpl_override. specialize (N3 n k0). subv_in s2 N3. simpl_override_in N3. assumption. simpl_override. simpl_override. specialize (N3 n0 k0). subv_in s2 N3. simpl_override_in N3. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)