proposition: Lemma messages_no_dup: forall p h s, step_star (init p) h s -> NoDup (messages s).
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H. subst s. simpl. constructor. inversion H0. simpl. apply nodup_app. split_all. depremise IHstep_star. assumption. rewrite <- H2 in IHstep_star. simpl in IHstep_star. assumption. apply nodup_map. apply nodup_filter. apply nodup_nids. intros x y _ _ N1. intro N2. inversion N2. contradiction. unfold disjoint. intro m. intros. apply in_map_iff in IN2. destruct IN2 as [rn [IN21 _]]. assert (A1 := message_clock_le_state_clock p ls s2 m). simpl in A1. depremise A1. split. subst s1. assumption. rewrite <- H2. simpl. assumption. rewrite <- IN21 in A1. simpl in A1. rewrite <- H2 in A1. simpl in A1. simpl_override_in A1. simpl in A1. assert (A2 := sem_clock_alg_state_clock p ls s2 n). simpl in A2. depremise A2. subst s1. assumption. rewrite <- H2 in A2. simpl in A2. simpl_override_in A2. simpl in A2. rewrite <- A2 in A1. rewrite Nat.add_comm in A1. simpl in A1. apply Nat.nle_succ_diag_l in A1. assumption. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. apply IHstep_star. assumption. simpl. rewrite <- H3 in IHstep_star. simpl in IHstep_star. depremise IHstep_star. assumption. apply NoDup_remove_1 in IHstep_star. assumption. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. apply IHstep_star. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)