proposition: Lemma msg_clock_lte_state_clock: forall p h s m, let n := msg_sender m in let c := msg_clock m in step_star (init p) h s /\ In m (messages s) -> c <= clock_state (node_states s n).
proof: Proof. intros. remember (init p) as s0 eqn: Hs. destruct H as [N1 N2]. induction N1. subst s. simpl in N2. contradiction. depremise IHN1. assumption. inversion H. subst l0. simpl. destruct (eq_nat_dec n0 n). simpl_override. simpl. rewrite <- H3 in N2. simpl in N2. apply in_app_iff in N2. destruct N2 as [N2 | N2]. depremise IHN1. rewrite <- H1. simpl. assumption. rewrite <- H1 in IHN1. simpl in IHN1. rewrite e0 in IHN1. simpl_override_in IHN1. lia. apply in_map_iff in N2. destruct N2 as [tn [N2 _]]. subst c. rewrite <- N2. simpl. apply Nat.le_refl. simpl_override. depremise IHN1. rewrite <- H1. simpl. rewrite <- H3 in N2. simpl in N2. apply in_app_iff in N2. destruct N2 as [N2 | N2]. assumption. exfalso. apply in_map_iff in N2. destruct N2 as [tn [N21 N22]]. apply filter_In in N22. destruct N22 as [_ N22]. destruct (nid_eq_dec n0 tn). inversion N22. subst n. rewrite <- N21 in n1. simpl in n1. apply n1. reflexivity. rewrite <- H1 in IHN1. simpl in IHN1. simpl_override_in IHN1. assumption. simpl. destruct (eq_nat_dec n0 n). simpl_override. simpl. depremise IHN1. rewrite <- H1. simpl. rewrite <- H3 in N2. simpl in N2. assumption. rewrite <- H1 in IHN1. simpl in IHN1. rewrite e0 in IHN1. simpl_override_in IHN1. simpl in IHN1. assumption. simpl_override. depremise IHN1. rewrite <- H1. simpl. rewrite <- H3 in N2. simpl in N2. assumption. rewrite <- H1 in IHN1. simpl in IHN1. simpl_override_in IHN1. simpl in IHN1. assumption. simpl. destruct (eq_nat_dec n0 n). simpl_override. simpl. depremise IHN1. rewrite <- H2. simpl. rewrite <- H4 in N2. simpl in N2. apply in_app_iff in N2. destruct N2. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. rewrite <- H2 in IHN1. simpl in IHN1. rewrite e0 in IHN1. simpl_override_in IHN1. simpl in IHN1. assumption. simpl_override. depremise IHN1. rewrite <- H2. simpl. rewrite <- H4 in N2. simpl in N2. apply in_app_iff in N2. destruct N2. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. rewrite <- H2 in IHN1. simpl in IHN1. simpl_override_in IHN1. simpl in IHN1. assumption. simpl. destruct (eq_nat_dec n0 n). subst n. subst n0. simpl_override. depremise IHN1. rewrite <- H1. simpl. rewrite <- H3 in N2. simpl in N2. assumption. subv_in s2 IHN1. simpl_override_in IHN1. simpl in IHN1. assumption. simpl_override. depremise IHN1. rewrite <- H1. simpl. rewrite <- H3 in N2. simpl in N2. assumption. subv_in s2 IHN1. simpl_override_in IHN1. simpl in IHN1. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)