proposition: Lemma update_clock: forall s s' l, (step s l s' /\ label_is_update l) -> let n' := label_orig_node l in let c' := label_clock l in let n := label_node l in let ls := label_post_state l in let co := clock ls in let ms := messages s in exists m, let mn' := msg_sender m in let mc' := msg_clock m in let mn := msg_receiver m in let u := msg_update m in let mco := sender_clock u in In m ms /\ n' = mn' /\ c' = mc' /\ n = mn /\ forall n'', In n'' nids -> mco n'' <= co n''.
proof: Proof. intros. open_conjs. inversion H. rewrite <- H3 in H0. unfold label_is_update in H0. contradiction. rewrite <- H3 in H0. unfold label_is_update in H0. contradiction. exists (message n'0 c'0 k v u n0 lp). simpl. split_all. subst ms. subst s. simpl. apply in_app_iff. right. apply in_eq. subst n'. rewrite <- H4. simpl. reflexivity. subst c'. rewrite <- H4. simpl. reflexivity. subst n. rewrite <- H4. simpl. reflexivity. unfold guard_method in H2. bool_to_prop_in H2. destruct H2 as [N1 N2]. intros. subst co. subst ls. rewrite <- H4. simpl in *. unfold override. destruct (eq_nat_dec n'' (sender_node u)). subst n''. apply Nat.le_refl. assert (A:= fold_left_and NId nids n'' (fun n => ((n =? sender_node u) || (sender_clock u n <=? clock s0 n)))). depremise A. split; assumption. simpl in A. bool_to_prop_in A. destruct A as [A | A]. bool_to_prop_in A. contradiction. bool_to_prop_in A. assumption. rewrite <- H3 in H0. unfold label_is_update in H0. contradiction. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)