proposition: Lemma cause_rec: forall p h s1 l s2 l', let n := label_node l in let c := label_clock l in let n' := label_node l' in let lp := msg_label (label_message l') in (step_star (init p) h s1 /\ step s1 l' s2 /\ label_is_put l /\ label_is_update l' /\ cause h l lp) -> c <= algrec (alg_state (node_states s1 n')) n.
proof: Proof. intros. destruct H as [N1 [N2 [N3 [N4 N5]]]]. unfold algrec. destruct l'; try contradiction. remember (update_label n0 n1 c0 n2 k v a m a0) as l' eqn: Hu. assert (A1: c = clock (label_post_state l) n). subv c. subv n. apply cause_in in N5. destruct N5 as [N5 _]. assert (B1 := in_exec). specex_deprem B1. split; eassumption. destruct B1 as [h1 [sm1 [sm2 [h2 [B11 [B12 [B13 B14]]]]]]]. assert (B2 := label_clock_label_post_state_clock). specex_deprem B2. split_all. apply B12. eassumption. eassumption. simpl in B2. assumption. rewrite A1. clear A1. assert (A2 := cause_clock). specex_deprem A2. split_all. eassumption. eassumption. eapply label_node_in_nids. split. eassumption. apply cause_in in N5. destruct N5 as [N5 _]. eassumption. simpl in A2. subst n. remember (label_node l) as n eqn: Hn. destruct A2 as [A21 A22]. assert (A3: (clock (label_post_state lp) (label_node lp) = clock (alg_state (node_states s1 n')) (label_node lp) + 1) /\ (forall n, In n nids /\ (n <> label_node lp)-> clock (label_post_state lp) n <= clock (alg_state (node_states s1 n')) n)). subv_in l' N2. inversion N2; simpl in *; try contradiction. subst s'0. subst a. subst s'5. subst s'4. subst s'3. subst s'2. subst v0. subst k0. subst n3. subst c0. subst n'0. subst s'1. subv n'. subv l'. simpl_override. subv lp. subv l'. subv m. unfold guard_method in H11. bool_to_prop_in H11. destruct H11 as [U1 U2]. bool_to_prop_in U1. assert (B1 := msg_update_label). specex_deprem B1. split_all. eassumption. subv s1. apply in_app_iff. right. apply in_eq. simpl in B1. destruct B1 as [B11 [B12 [B13 B14]]]. split. rewrite B13 in U1. rewrite B12 in U1. assumption. intros. open_conjs. assert (B2 := fold_left_and NId nids n3 (fun n => ((n =? sender_node u) || (sender_clock u n <=? clock s n)))). depremise B2. split. rewrite <- U2 at 2. f_equal. assumption. simpl in B2. bool_to_prop_in B2. destruct B2 as [B2 | B2]. exfalso. bool_to_prop_in B2. subst n3. contradiction. bool_to_prop_in B2. rewrite B13 in B2. assumption. destruct A3 as [A31 A32]. destruct (eq_nat_dec n (label_node lp)). clear A21 A32. subv n. depremise A22. split. symmetry. assumption. assert (B := msg_update_label). subv_in l' N2. inversion N2. specex_deprem B. split_all. eassumption. subv s1. apply in_app_iff. right. apply in_eq. simpl in B. destruct B as [B _]. subv lp. subv l'. subv m. assumption. rewrite e in A22. rewrite A31 in A22. clear A31. rewrite Nat.add_comm in A22. simpl in A22. apply (proj1 (Nat.lt_succ_r _ _)) in A22. assumption. clear A22 A31. specialize (A32 n). depremise A32. assert (B := label_node_in_nids). specex_deprem B. split. eassumption. apply cause_in in N5. destruct N5 as [N5 _]. eassumption. simpl in B. subv n. split. assumption. subst n. assumption. eapply Nat.le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)