proposition: Lemma update_sender_clock: forall p h s l s', (step_star (init p) h s /\ step s l s' /\ label_is_update l) -> (let n := label_node l in let n' := label_orig_node l in sender_clock (msg_update (label_message l)) <= (received (alg_state (node_states s n)) n') + 1).
proof: Proof. intros. destruct H as [H1 [H2 H3]]. destruct l; simpl in *; try contradiction; clear H3. inversion H2. remember (update_label n0 n1 c n2 k v a m a0) as l eqn: Hl. remember (message n'0 c' k0 v0 u n3 lp) as msg eqn: Hm. subst s'2. subst s'3. subst s'4. subst s'5. subst s'6. subst c. subst n. subst n'. subst n2. subst k. subst v. subst a. subst n0. subst n'0. simpl. simpl_override. simpl. assert (A1 := Nat.le_gt_cases (sender_clock u) 1). destruct A1 as [A1 | A1]. assert (A2 := Nat.le_0_l (received s0 n1)). assert (A3 := plus_O_n (sender_clock u)). rewrite <- A3. eapply Nat.add_le_mono; eassumption. assert (A2 := update_pred p h s msg). simpl in A2. depremise A2. split. assumption. subst s. simpl. apply in_app_iff. right. apply in_eq. depremise A2. subst msg. simpl. assumption. rewrite Hm in A2. simpl in A2. unfold guard_method in H13. assert (A3 := fold_left_and (NId*Clock) (sender_dep u) (sender_node u, pred (sender_clock u)) (fun p => snd p <=? received s0 (fst p))). depremise A3. split; assumption. simpl in A3. bool_to_prop_in A3. apply Nat.succ_le_mono in A3. assert (A4 := Nat.succ_pred (sender_clock u)). depremise A4. intro. rewrite H in *. inversion A1. rewrite A4 in A3. clear A4. assert (A5 := message_update_node_clock_eq p h s msg). simpl in A5. depremise A5. split. assumption. subst s. simpl. apply in_app_iff. right. apply in_eq. destruct A5 as [A5 _]. rewrite Hm in A5. simpl in A5. rewrite A5. rewrite Nat.add_comm. simpl. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)