proposition: Lemma update_pred: forall p h s m, (step_star (init p) h s /\ In m (messages s)) -> (let u := msg_update m in let n := sender_node u in let c := sender_clock u in let d := sender_dep u in c > 1 -> In (n, pred c) d).
proof: Proof. intros. destruct H as [H1 H2]. remember (init p) as s0 eqn: Hs. induction H1. subst s. simpl in H2. contradiction. depremise IHstep_star. assumption. inversion H. rewrite <- H6 in H2. simpl in H2. apply in_app_iff in H2. destruct H2 as [H2 | H2]. apply IHstep_star. rewrite <- H4. simpl. assumption. apply in_map_iff in H2. destruct H2 as [rn [H21 H22]]. subst d. subst u. subst c. subst n. rewrite <- H21. simpl. rewrite Nat.add_comm. simpl. assert (A1 := clock_in_dep p ls s2 n0). simpl in A1. depremise A1. subst s1. assumption. rewrite <- H4 in A1. simpl in A1. simpl_override_in A1. simpl in A1. rewrite <- H21 in H0. simpl in H0. apply A1. rewrite Nat.add_comm in H0. simpl in H0. apply Nat.lt_succ_lt_pred in H0. rewrite <- pred_Sn in H0. assumption. apply IHstep_star. rewrite <- H4. simpl. rewrite <- H6 in H2. simpl in H2. assumption. apply IHstep_star. 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. apply IHstep_star. rewrite <- H4. simpl. rewrite <- H6 in H2. simpl in H2. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)