proposition: Lemma update_dep_eq_msg_clock: forall p h s m, step_star (init p) h s /\ In m (messages s) -> sender_dep (msg_update m) (sender_node (msg_update m))= msg_clock m.
proof: Proof. intros. open_conjs. remember (init p) as s0 eqn: Hi. induction H. subst s. simpl in H0. contradiction. depremise IHstep_star. assumption. inversion H1. rewrite <- H5 in H0. simpl in H0. apply in_app_iff in H0. destruct H0 as [H0 | H0]. depremise IHstep_star. rewrite <- H3. simpl. assumption. assumption. apply in_map_iff in H0. destruct H0 as [n' [N1 N2]]. subst m. simpl in *. simpl_override. assert (A := sem_clock_alg_state_clock). specex_deprem A. subst s1. eassumption. specialize (A n). simpl in A. subv_in s2 A. simpl_override_in A. rewrite A. reflexivity. rewrite <- H3 in IHstep_star. simpl in IHstep_star. depremise IHstep_star. rewrite <- H5 in H0. assumption. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. depremise IHstep_star. rewrite <- H6 in H0. simpl in H0. apply in_app_iff in H0. destruct H0 as [H0 | H0]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. assumption. depremise IHstep_star. subv s2. subv_in s3 H0. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)