proposition: Lemma msg_update_label: forall p h s m, step_star (init p) h s /\ In m (messages s) -> (let lp := msg_label m in let u := msg_update m in label_is_put lp /\ sender_node u = label_node lp /\ sender_clock u = clock (label_post_state lp) /\ sender_clock u (sender_node u) = label_clock lp).
proof: Proof. intros. remember (init p) as s0 eqn: Hs. open_conjs. induction H. subst s. simpl in H0. contradiction. depremise IHstep_star. assumption. inversion H1. subst l0. subst u. simpl. rewrite <- H5 in H0. simpl in H0. apply in_app_iff in H0. destruct H0. depremise IHstep_star. rewrite <- H3. simpl. assumption. assumption. apply in_map_iff in H0. destruct H0 as [n' [N1 N2]]. rewrite <- N1. simpl. subst lp. rewrite <- N1. simpl. split. reflexivity. simpl_override. assert (A:= sem_clock_alg_state_clock p ls s2). depremise A. subst s1. assumption. specialize (A n). simpl in A. rewrite <- H3 in A. simpl in A. simpl_override_in A. simpl in A. rewrite A. split_all; reflexivity. subst u. rewrite <- H5 in H0. simpl in H0. depremise IHstep_star. rewrite <- H3. simpl. assumption. assumption. subst u. rewrite <- H6 in H0. simpl in H0. apply in_app_iff in H0. destruct H0 as [H0 | H0]. depremise IHstep_star. rewrite <- H4. simpl. apply in_app_iff. left. assumption. assumption. depremise IHstep_star. rewrite <- H4. simpl. apply in_app_iff. right. apply in_cons. assumption. assumption. subst u. rewrite <- H5 in H0. simpl in H0. depremise IHstep_star. rewrite <- H3. simpl. 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)