proposition: Lemma in_map_from_put_update: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(k: Key)(n: NId), step_star (init p) h s -> let m := store (alg_state ((node_states s) n)) in let iv := m k in let ivn := inst_val_nid iv in let ivc := inst_val_clock iv in (ivn = init_nid /\ ivc = 0) \/ (exists (l: Label), (In l h /\ label_is_put l /\ label_node l = ivn /\ label_clock l = ivc /\ label_node l = n) \/ (In l h /\ label_is_update l /\ label_orig_node l = ivn /\ label_clock l = ivc /\ label_node l = n)).
proof: Proof. intros. remember (init p) as s0 eqn: H1. induction H. left. subst ivn. subst ivc. subst iv. subst m. subst s. unfold init. simpl. split; reflexivity. depremise IHstep_star. assumption. pose (n' := label_node l). destruct (eq_nat_dec n n') eqn: N. subst n'. assert (E := H0). inversion H0. destruct (eq_nat_dec k k0) eqn: K. clear IHstep_star. right. exists l. left. split. subst l. apply in_or_app. right. unfold In. left. reflexivity. split. subst l. unfold label_is_put. apply I. rewrite <- H4. simpl. assert (L := put_change s2 s3 l). simpl in L. depremise L. split. assumption. rewrite <- H4. simpl. apply I. rewrite <- H4 in L. simpl in L. open_conjs. subst ivn. subst ivc. subst iv. subst m. subst k. subst n. subst l. simpl. split_all. symmetry; assumption. symmetry; assumption. reflexivity. clear H2 H5. assert (L := put_nochange s2 s3 l). simpl in L. depremise L. split. assumption. subst l. simpl. apply I. rewrite <- H4 in L. simpl in L. specialize (L k). depremise L. apply not_eq_sym. assumption. simpl in IHstep_star. rewrite e in IHstep_star. rewrite <- H4 in IHstep_star. simpl in IHstep_star. rewrite L in *; clear L. destruct IHstep_star. left. subst ivn. subst ivc. subst iv. subst m. subst n. subst l. simpl. assumption. right. destruct H2 as [l' H2]. destruct H2; open_conjs; exists l'. left. split_all. apply in_or_app. left. assumption. assumption. subst ivn. subst iv. subst m. subst n. subst l. simpl. assumption. subst ivc. subst iv. subst m. subst n. subst l. simpl. assumption. rewrite e. rewrite <- H4. simpl. assumption. right. split_all. apply in_or_app. left. assumption. assumption. subst ivn. subst iv. subst m. subst n. subst l. simpl. assumption. subst ivc. subst iv. subst m. subst n. subst l. simpl. assumption. rewrite e. rewrite <- H4. simpl. assumption. assert (L := get_nochange s2 s3 l n). simpl in L. depremise L. split. assumption. subst l. unfold label_is_get. apply I. rewrite L in *. destruct IHstep_star. left. subst ivn. subst ivc. subst iv. subst m. assumption. right. destruct H6 as [l' H6]. exists l'. destruct H6; open_conjs. left. split. apply in_or_app. left. assumption. split. assumption. subst ivn. subst ivc. subst iv. subst m. split_all; assumption. right. split. apply in_or_app. left. assumption. split. assumption. subst ivn. subst ivc. subst iv. subst m. split_all; assumption. clear N. rewrite <- H5 in e. simpl in e. destruct (eq_nat_dec k k0) eqn: K. clear IHstep_star. right. exists l. right. split. subst l. apply in_or_app. right. unfold In. left. reflexivity. split. subst l. unfold label_is_update. apply I. rewrite <- H5. simpl. assert (L := update_change s2 s3 l). simpl in L. depremise L. split. assumption. rewrite <- H5. simpl. apply I. rewrite <- H5 in L. simpl in L. open_conjs. subst ivn. subst ivc. subst iv. subst m. subst k. subst n. subst l. simpl. split_all; try reflexivity; symmetry; assumption. clear H2 H3 H6. assert (L := update_nochange s2 s3 l). simpl in L. depremise L. split. assumption. subst l. simpl. apply I. rewrite <- H5 in L. simpl in L. specialize (L k). depremise L. apply not_eq_sym. assumption. simpl in IHstep_star. rewrite e in IHstep_star. simpl in IHstep_star. rewrite L in *; clear L. destruct IHstep_star. left. subst ivn. subst ivc. subst iv. subst m. subst n. subst l. simpl. assumption. right. destruct H2 as [l' H2]. destruct H2; open_conjs; exists l'. left. split_all. apply in_or_app. left. assumption. assumption. subst ivn. subst iv. subst m. subst n. subst l. simpl. assumption. subst ivc. subst iv. subst m. subst n. subst l. simpl. assumption. rewrite e. assumption. right. split_all. apply in_or_app. left. assumption. assumption. subst ivn. subst iv. subst m. subst n. subst l. simpl. assumption. subst ivc. subst iv. subst m. subst n. subst l. simpl. assumption. rewrite e. assumption. subst ivn. subst ivc. subst iv. subst m. subv s3. simpl in IHstep_star. subv_in s2 IHstep_star. destruct (eq_nat_dec n n0). subst n0. simpl_override. simpl_override_in IHstep_star. destruct IHstep_star. left. assumption. right. destruct H6 as [l' H6]. exists l'. destruct H6; open_conjs. left. split. apply in_or_app. left. assumption. split. assumption. split_all; assumption. right. split. apply in_or_app. left. assumption. split. assumption. split_all; assumption. simpl_override. simpl_override_in IHstep_star. destruct IHstep_star. left. assumption. right. destruct H6 as [l' H6]. exists l'. destruct H6; open_conjs. left. split. apply in_or_app. left. assumption. split. assumption. split_all; assumption. right. split. apply in_or_app. left. assumption. split. assumption. split_all; assumption. assert (L := node_nochange s2 s3 l n). simpl in L; depremise L. split. assumption. subst n'. apply not_eq_sym. assumption. rewrite L in *. clear L. destruct IHstep_star. left. subst ivn. subst ivc. subst iv. subst m. assumption. right. destruct H2 as [l' H2]. exists l'. destruct H2; open_conjs. left. split_all. apply in_or_app. left. assumption. assumption. subst ivn. subst iv. subst m. assumption. subst ivc. subst iv. subst m. assumption. assumption. right. split_all. apply in_or_app. left. assumption. assumption. subst ivn. subst iv. subst m. assumption. subst ivc. subst iv. subst m. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)