proposition: Lemma message_clock_neq: forall p h s m m', let n := msg_sender m in let c := msg_clock m in let rn := msg_receiver m in let n' := msg_sender m' in let c' := msg_clock m' in let rn' := msg_receiver m' in (step_star (init p) h s /\ In m (messages s) /\ In m' (messages s) /\ n = n' /\ rn = rn' /\ not (m = m')) -> not (c = c').
proof: Proof. intros. destruct H as [H1 [H2 [H3 [H4 [Hr Hn]]]]]. remember (init p) as s0 eqn: Hs. induction H1. subst s. simpl in H2. contradiction. depremise IHstep_star. assumption. inversion H. rewrite <- H7 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. rewrite <- H7 in H3. simpl in H3. apply in_app_iff in H3. destruct H3 as [H3 | H3]. apply IHstep_star. rewrite <- H5. simpl. assumption. rewrite <- H5. simpl. assumption. apply in_map_iff in H3. destruct H3 as [tn [H31 H32]]. assert (A1 := message_clock_le_state_clock p ls s2 m). simpl in A1. depremise A1. split. subst s1. assumption. rewrite <- H5. simpl. assumption. subst n. subst n'. rewrite H4 in A1. rewrite <- H31 in A1. simpl in A1. rewrite <- H5 in A1. simpl in A1. simpl_override_in A1. simpl in A1. subst c. subst c'. rewrite <- H31. simpl. assert (A2 := sem_clock_alg_state_clock p ls s2 n0). simpl in A2. depremise A2. subst s1. assumption. rewrite <- H5 in A2. simpl in A2. simpl_override_in A2. simpl in A2. rewrite <- A2 in A1. intro. rewrite H3 in A1. rewrite Nat.add_comm in A1. simpl in A1. apply Nat.nle_succ_diag_l in A1. assumption. rewrite <- H7 in H3. simpl in H3. apply in_app_iff in H3. destruct H3 as [H3 | H3]. apply in_map_iff in H2. destruct H2 as [tn [H21 H22]]. assert (A1 := message_clock_le_state_clock p ls s2 m'). simpl in A1. depremise A1. split. subst s1. assumption. rewrite <- H5. simpl. assumption. subst n. subst n'. rewrite <- H4 in A1. rewrite <- H21 in A1. simpl in A1. rewrite <- H5 in A1. simpl in A1. simpl_override_in A1. simpl in A1. subst c. subst c'. rewrite <- H21. simpl. assert (A2 := sem_clock_alg_state_clock p ls s2 n0). simpl in A2. depremise A2. subst s1. assumption. rewrite <- H5 in A2. simpl in A2. simpl_override_in A2. simpl in A2. rewrite <- A2 in A1. intro. rewrite <- H2 in A1. rewrite Nat.add_comm in A1. simpl in A1. apply Nat.nle_succ_diag_l in A1. assumption. exfalso. apply in_map_iff in H2. destruct H2 as [tn [H21 H22]]. apply in_map_iff in H3. destruct H3 as [tn' [H31 H32]]. rewrite <- H21 in Hn. rewrite <- H31 in Hn. apply Hn. f_equal. subst rn. subst rn'. rewrite <- H21 in Hr. rewrite <- H31 in Hr. simpl in Hr. assumption. apply IHstep_star. rewrite <- H5. simpl. rewrite <- H7 in H2. simpl in H2. assumption. rewrite <- H5. simpl. rewrite <- H7 in H3. simpl in H3. assumption. apply IHstep_star. rewrite <- H6. simpl. rewrite <- H8 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. rewrite <- H6. simpl. rewrite <- H8 in H3. simpl in H3. apply in_app_iff in H3. destruct H3 as [H3 | H3]. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. apply IHstep_star. rewrite <- H5. simpl. rewrite <- H7 in H2. simpl in H2. assumption. rewrite <- H5. simpl. rewrite <- H7 in H3. simpl in H3. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)