proposition: Lemma dep_received: forall p h s n n' c', let st := alg_state (node_states s n) in (step_star (init p) h s /\ In (n', c') (dep st)) -> received st n' >= c'.
proof: Proof. intros. destruct H as [H1 H2]. remember (init p) as s0 eqn: Hs. induction H1. subst st. subst s. simpl in H2. contradiction. simpl in IHstep_star. depremise IHstep_star. assumption. inversion H. subst st. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. rewrite <- H5 in H2. simpl in H2. simpl_override_in H2. simpl in H2. destruct H2 as [H2 | H2]; try contradiction. inversion H2. simpl_override. apply Nat.le_refl. simpl_override. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. rewrite <- H5 in H2. simpl in H2. simpl_override_in H2. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst st. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. rewrite <- H5 in H2. simpl in H2. simpl_override_in H2. simpl in H2. destruct (entry_node (store s k) <>? init_nid). simpl in H2. destruct H2 as [H2 | H2]. inversion H2. assert (A1 := store_received p ls s2 n0 k). simpl in A1. depremise A1. subst s1. assumption. rewrite <- H3 in A1. simpl in A1. simpl_override_in A1. simpl in A1. assumption. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. simpl. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. simpl. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. assumption. simpl_override. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. rewrite <- H5 in H2. simpl in H2. simpl_override_in H2. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. subst st. rewrite <- H6. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. simpl. depremise IHstep_star. rewrite <- H4. simpl. simpl_override. simpl. rewrite <- H6 in H2. simpl in H2. simpl_override_in H2. simpl in H2. assumption. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. simpl in IHstep_star. destruct (eq_nat_dec (sender_node u) n'). simpl_override. assert (B1 := received_lt_message_clock p ls s2 (message n'0 c'0 k v u n0 lp) n0). simpl in B1. depremise B1. split_all. subst s1. assumption. rewrite <- H4. simpl. apply in_app_iff. right. apply in_eq. reflexivity. rewrite <- H4 in B1. simpl in B1. simpl_override_in B1. simpl in B1. assert (B2 := message_update_node_clock_eq p ls s2 (message n'0 c'0 k v u n0 lp)). simpl in B2. depremise B2. split_all. subst s1. assumption. rewrite <- H4. simpl. apply in_app_iff. right. apply in_eq. destruct B2 as [B21 B22]. rewrite B21 in B1. rewrite e0 in B1. rewrite B22 in B1. clear B21 B22. apply Nat.lt_le_incl. eapply Nat.le_lt_trans; eassumption. simpl_override. assumption. simpl_override. rewrite <- H4 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. apply IHstep_star. rewrite <- H6 in H2. simpl in H2. simpl_override_in H2. assumption. subst st. rewrite <- H5. simpl. destruct (eq_nat_dec n0 n). subst n. simpl_override. rewrite <- H5 in H2. simpl in H2. simpl_override_in H2. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. assumption. rewrite <- H3 in IHstep_star. simpl in IHstep_star. simpl_override_in IHstep_star. assumption. simpl_override. rewrite <- H5 in H2. simpl in H2. simpl_override_in H2. depremise IHstep_star. rewrite <- H3. simpl. simpl_override. assumption. rewrite <- H3 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)