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 /\ In lp h /\ label_node lp = sender_node u /\ label_clock lp = sender_clock u /\ label_dep lp = sender_dep u /\ label_key lp = msg_key m /\ label_val lp = msg_val m).
proof: Proof. intros. remember (init p) as s0 eqn: Hs. destruct H as [H1 H2]. induction H1. subst s. simpl in H2. contradiction. depremise IHstep_star. assumption. inversion H. subst l0. subst u. rewrite <- H5 in H2. simpl in H2. apply in_app_iff in H2. destruct H2. depremise IHstep_star. rewrite <- H3. simpl. assumption. open_conjs. split_all; try assumption. apply in_app_iff. left. assumption. apply in_map_iff in H2. destruct H2 as [n' [N1 N2]]. rewrite <- N1. simpl. subst lp. rewrite <- N1. simpl. split_all. apply I. apply in_app_iff. right. apply in_eq. 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. reflexivity. reflexivity. reflexivity. subst u. rewrite <- H5 in H2. simpl in H2. depremise IHstep_star. rewrite <- H3. simpl. assumption. open_conjs. split_all; try assumption. apply in_app_iff. left. assumption. subst u. rewrite <- H6 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. depremise IHstep_star. rewrite <- H4. simpl. apply in_app_iff. left. assumption. open_conjs. split_all; try assumption. apply in_app_iff. left. assumption. depremise IHstep_star. rewrite <- H4. simpl. apply in_app_iff. right. apply in_cons. assumption. open_conjs. split_all; try assumption. apply in_app_iff. left. assumption. subst u. rewrite <- H5 in H2. simpl in H2. depremise IHstep_star. rewrite <- H3. simpl. assumption. open_conjs. split_all; try assumption. apply in_app_iff. left. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)