proposition: Lemma received_lt_message_clock: forall p h s m n, let st := alg_state (node_states s n) in let msn := msg_sender m in let mc := msg_clock m in let mrn := msg_receiver m in (step_star (init p) h s /\ In m (messages s) /\ mrn = n) -> received st msn < mc.
proof: Proof. intros. destruct H as [H1 [H2 H3]]. remember (init p) as s0 eqn: Hi. induction H1. rewrite Hi in H2. simpl in H2. contradiction. simpl in IHstep_star. depremise IHstep_star. assumption. inversion H. subst l0. subst st. rewrite <- H6. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. destruct (eq_nat_dec n0 msn). simpl_override. exfalso. rewrite <- H6 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. assert (A1 := no_self_message p ls s2 m). depremise A1. split. subst s1. assumption. rewrite <- H4. simpl. assumption. subst msn. subst mrn. rewrite e1 in e0. contradiction. apply in_map_iff in H2. destruct H2 as [mrn' [H21 H22]]. apply filter_In in H22. destruct H22 as [H221 H222]. subst mrn. subst msn. subst mc. subst m. simpl in *. subst mrn'. rewrite eq_nat_dec_eq in H222. inversion H222. simpl_override. rewrite <- H6 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. depremise IHstep_star. rewrite <- H4. simpl. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. rewrite <- e0 in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. apply in_map_iff in H2. destruct H2 as [mrn' [H21 H22]]. apply filter_In in H22. destruct H22 as [H221 H222]. subst mrn. subst msn. subst mc. subst m. simpl in *. subst mrn'. rewrite eq_nat_dec_eq in H222. inversion H222. simpl_override. rewrite <- H6 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. depremise IHstep_star. rewrite <- H4. simpl. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. apply in_map_iff in H2. destruct H2 as [mrn' [H21 H22]]. apply filter_In in H22. destruct H22 as [H221 H222]. assert (A1 := received_lt_sent p ls s2 n msn). simpl in A1. depremise A1. subst s1. assumption. rewrite <- H4 in A1. simpl in A1. simpl_override_in A1. simpl in A1. subst msn. subst mc. subst mrn. subst m. simpl in *. simpl_override_in A1. simpl in A1. assert (A2 := sem_clock_alg_state_clock p ls s2 n0). depremise A2. subst s1. assumption. simpl in A2. rewrite <- H4 in A2. simpl in A2. simpl_override_in A2. simpl in A2. rewrite <- A2 in A1. clear A2. rewrite Nat.add_comm. simpl. apply Nat.lt_succ_r. assumption. subst st. rewrite <- H6. simpl. rewrite <- H6 in H2. simpl in H2. depremise IHstep_star. rewrite <- H4. simpl. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n0 n). simpl_override. simpl. rewrite e0 in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. simpl. simpl_override_in IHstep_star. assumption. subst st. rewrite <- H7. simpl. destruct (eq_nat_dec n0 n). simpl_override. simpl. destruct (eq_nat_dec (sender_node u) msn). simpl_override. subst mc. assert (A1 := message_update_node_clock_eq p ls s2 (message n' c' k v u n0 lp)). simpl in A1. depremise A1. split. subst s1. assumption. rewrite <- H5. simpl. apply in_app_iff. right. apply in_eq. destruct A1 as [A11 A12]. rewrite <- A12. assert (A2 := update_pred p ls s2 (message n' c' k v u n0 lp)). depremise A2. split. subst s1. assumption. rewrite <- H5. simpl. apply in_app_iff. right. apply in_eq. simpl in A2. rewrite <- A11 in A2. rewrite <- A12 in A2. assert (A3 := Nat.le_gt_cases c' 1). destruct A3 as [A3 | A3]. assert (A4 := message_clock_ge_one p ls s2 m). depremise A4. split. subst s1. assumption. rewrite <- H7 in H2. simpl in H2. apply in_app_iff in H2. rewrite <- H5. simpl. destruct H2 as [H2 | H2]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. assert (A5: c' <= msg_clock m). eapply Nat.le_trans; eassumption. apply Nat.lt_eq_cases in A5. destruct A5 as [A5 | A5]. assumption. exfalso. assert (A6 := message_clock_neq p ls s2 (message n' c' k v u n0 lp) m). simpl in A6. depremise A6. split_all. subst s1. assumption. rewrite <- H5. simpl. apply in_app_iff. right. apply in_eq. rewrite <- H5. simpl. rewrite <- H7 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. subst msn. rewrite <- e1. assumption. subst mrn. subst n. assumption. intro. assert (B1 := messages_no_dup p ls s2). depremise B1. subst s1. assumption. rewrite <- H5 in B1. simpl in B1. apply NoDup_remove_2 in B1. rewrite H8 in B1. rewrite <- H7 in H2. simpl in H2. contradiction. contradiction. depremise A2. assumption. unfold guard_method in H4. assert (A7 := fold_left_and (NId*Clock) (sender_dep u) (n', pred c') (fun p => snd p <=? received s (fst p))). depremise A7. split; assumption. simpl in A7. bool_to_prop_in A7. depremise IHstep_star. rewrite <- H7 in H2. simpl in H2. apply in_app_iff in H2. rewrite <- H5. simpl. destruct H2 as [H2 | H2]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. rewrite <- H5 in IHstep_star. simpl in IHstep_star. rewrite e0 in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. rewrite <- e1 in IHstep_star. rewrite <- A11 in IHstep_star. assert (A8: pred c' < msg_clock m). eapply Nat.le_lt_trans; eassumption. apply Nat.lt_succ_pred in A3. apply eq_sym in A3. apply Nat.le_succ_l in A8. rewrite <- A3 in A8. apply Nat.lt_eq_cases in A8. destruct A8 as [A8 | A8]. assumption. exfalso. assert (A9 := message_clock_neq p ls s2 (message n' c' k v u n0 lp) m). simpl in A9. depremise A9. split_all. subst s1. assumption. rewrite <- H5. simpl. apply in_app_iff. right. apply in_eq. rewrite <- H5. simpl. rewrite <- H7 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. subst msn. rewrite <- e1. assumption. subst mrn. subst n. assumption. intro. assert (B1 := messages_no_dup p ls s2). depremise B1. subst s1. assumption. rewrite <- H5 in B1. simpl in B1. apply NoDup_remove_2 in B1. rewrite H8 in B1. rewrite <- H7 in H2. simpl in H2. contradiction. contradiction. simpl_override. rewrite <- H7 in H2. simpl in H2. apply in_app_iff in H2. depremise IHstep_star. rewrite <- H5. simpl. destruct H2 as [H2 | H2]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. rewrite <- H5 in IHstep_star. simpl in IHstep_star. rewrite e0 in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. rewrite <- H7 in H2. simpl in H2. depremise IHstep_star. rewrite <- H5. simpl. apply in_app_iff in H2. destruct H2 as [H2 | H2]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. rewrite <- H5 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst st. rewrite <- H6. simpl. rewrite <- H6 in H2. simpl in H2. depremise IHstep_star. rewrite <- H4. simpl. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n0 n). simpl_override. rewrite e0 in IHstep_star. simpl_override_in IHstep_star. assumption. simpl_override. simpl_override_in IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)