proposition: Lemma store_received: forall p h s n k, let st := alg_state (node_states s n) in let en := entry_node (store st k) in let ec := entry_clock (store st k) in step_star (init p) h s -> received st en >= ec.
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H. subst st. subst en. subst ec. subst s. simpl. apply Nat.le_refl. simpl in IHstep_star. depremise IHstep_star. assumption. inversion H0. subst st. subst en. subst ec. rewrite <- H4. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. destruct (eq_nat_dec k0 k). subst k. simpl_override. simpl. simpl_override. apply Nat.le_refl. simpl_override. unfold override at 2. unfold override at 2. rewrite eq_nat_dec_neq. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec n0 (entry_node (store s k))). simpl_override. rewrite <- e0 in IHstep_star. assert (B2 := rec_eq_clock p ls s2 n0). simpl in B2. depremise B2. subst s1. assumption. rewrite <- H2 in B2. simpl in B2. simpl_override_in B2. simpl in B2. rewrite B2 in IHstep_star. clear B2. rewrite Nat.add_comm. simpl. apply le_S. assumption. simpl_override. assumption. apply not_eq_sym. assumption. assert (B1: override nss n0 (node_state p0 s' (c + 1)) n = nss n). simpl_override. reflexivity. rewrite B1. clear B1. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst st. subst en. subst ec. rewrite <- H4. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst st. subst en. subst ec. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. destruct (eq_nat_dec k0 k). subst k. simpl_override. simpl. simpl_override. apply Nat.le_refl. unfold override at 2. unfold override at 2. rewrite eq_nat_dec_neq. destruct (eq_nat_dec (sender_node u) (entry_node (store s k))). simpl_override. assert (C1 := received_lt_message_clock p ls s2 (message n' c' k0 v u n0 lp) n0). simpl in C1. depremise C1. split_all. subst s1. assumption. rewrite <- H3. simpl. apply in_app_iff. right. apply in_eq. reflexivity. rewrite <- H3 in C1. simpl in C1. simpl_override_in C1. simpl in C1. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assert (C2 := message_update_node_clock_eq p ls s2 (message n' c' k0 v u n0 lp)). simpl in C2. depremise C2. split_all. subst s1. assumption. rewrite <- H3. simpl. apply in_app_iff. right. apply in_eq. destruct C2 as [C21 C22]. rewrite <- e0 in IHstep_star. rewrite <- C21 in IHstep_star. rewrite C22 in C1. apply Nat.lt_le_incl. eapply Nat.le_lt_trans; eassumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. apply not_eq_sym. assumption. simpl_override. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst st. subst en. subst ec. rewrite <- H4. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. rewrite <- H2 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl_override. rewrite <- H2 in IHstep_star. simpl in IHstep_star. 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)