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 (entry_val iv) in let ivc := inst_val_clock (entry_val 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'). subst n'. assert (E := H0). inversion H0. destruct (eq_nat_dec k k0). clear IHstep_star. right. subst l0. rewrite H4 in *. exists l. left. split_all. apply in_or_app. right. apply in_eq. subst l. unfold label_is_put. apply I. assert (A1 := put_change s2 s3 l). simpl in A1. depremise A1. split. assumption. subst l. simpl. apply I. destruct A1 as [A1 _]. subst ivn. subst iv. subst m. subst n. subst k. rewrite <- H4 in A1 at 2. simpl in A1. symmetry. assumption. assert (A1 := put_change s2 s3 l). simpl in A1. depremise A1. split. assumption. subst l. simpl. apply I. destruct A1 as [_ A1]. subst ivc. subst iv. subst m. subst n. subst k. rewrite <- H4 in A1 at 2. simpl in A1. symmetry. assumption. symmetry. assumption. 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 *; clear L. 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. rewrite <- H5 in e. simpl in e. destruct (eq_nat_dec k k0). clear IHstep_star. right. exists l. right. split. subst l. apply in_or_app. right. apply in_eq. 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. simpl in IHstep_star. subv_in s2 IHstep_star. simpl_override_in IHstep_star. subst ivn. subst ivc. subst iv. subst m. subv s3. destruct IHstep_star. left. destruct (eq_nat_dec n0 n). rewrite e1 in *. simpl_override. simpl_override_in H6. assumption. simpl_override. simpl_override_in H6. assumption. right. destruct H6 as [l' H6]. exists l'. destruct H6; open_conjs. left. split. apply in_or_app. left. assumption. split. assumption. destruct (eq_nat_dec n0 n). rewrite e1 in *. simpl_override. simpl_override_in H8. simpl_override_in H9. split_all; assumption. simpl_override. simpl_override_in H8. simpl_override_in H9. split_all; assumption. right. split. apply in_or_app. left. assumption. split. assumption. destruct (eq_nat_dec n0 n). rewrite e1 in *. simpl_override. simpl_override_in H8. simpl_override_in H9. split_all; assumption. simpl_override. simpl_override_in H8. simpl_override_in H9. 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 List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)