proposition: Lemma message_update_node_clock_eq: forall p h s m, let ms := messages s in (step_star (init p) h s /\ In m ms) -> let mn := msg_sender m in let mc := msg_clock m in let u := msg_update m in let un := sender_node u in let uc := sender_clock u in mn = un /\ mc = uc.
proof: Proof. intros. open_conjs. remember (init p) as s0 eqn: Hs. induction H. subst ms. subst s. simpl in *. contradiction. inversion H1. subst ms. rewrite <- H5 in H0. simpl in H0. apply in_app_iff in H0. destruct H0. simpl in IHstep_star. depremise IHstep_star. assumption. depremise IHstep_star. rewrite <- H3. simpl. assumption. assumption. clear IHstep_star. apply in_map_iff in H0. destruct H0 as [nt [H01 H02]]. subst mn. subst mc. subst un. subst uc. subst u. subst m. simpl. split. reflexivity. assert (A := sem_clock_alg_state_clock p ls s2 n). depremise A. subst s1. assumption. simpl in A. rewrite <- H3 in A. simpl in A. simpl_override_in A. simpl in A. rewrite A. reflexivity. subst ms. rewrite <- H5 in H0. simpl in H0. simpl in IHstep_star. depremise IHstep_star. assumption. depremise IHstep_star. rewrite <- H3. simpl. assumption. assumption. subst ms. rewrite <- H6 in H0. simpl in H0. simpl in IHstep_star. depremise IHstep_star. assumption. depremise IHstep_star. rewrite <- H4. simpl. apply in_app_iff in H0. destruct H0. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. assumption. subst ms. subv_in s3 H0. simpl in IHstep_star. depremise IHstep_star. assumption. depremise IHstep_star. subv s2. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)