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 := ICExec.msg_label (ICExec.label_message l') in (ICExec.StepStar.step_star (ICExec.init p) h s1 /\ ICExec.step s1 l' s2 /\ ICExec.label_is_put l /\ ICExec.label_is_update l' /\ cause h l lp) -> c <= algrec (ICExec.alg_state (ICExec.node_states s1 n')) n.
proof: Proof. intros. open_conjs. destruct l'; simpl in *; try contradiction. inversion H0. subst s'0. subst s'1. subst s'2. subst s'3. subst s'4. subst s'5. subst n'0. subst k0. subst v0. subst n3. subst a. subst c0. remember (update_label n0 n1 c' n2 k v s m a0) as l' eqn: L. assert (A2 := cause_dep p (h++[l']) s2 l lp). depremise A2. split_all. apply step_star_app_one. exists s1. split; assumption. assumption. apply cause_ext_cause. assumption. destruct A2 as [A2 | A2]. unfold guard_method in H16. assert (A3 := fold_left_and (NId*Clock) (sender_dep u) (label_node l, label_clock l) (fun p => snd p <=? received s (fst p))). depremise A3. split. rewrite <- H16 at 2. f_equal. assert (B1 := msg_update_label p h s1 m). depremise B1. split. assumption. subv s1. apply in_app_iff. right. subv m. apply in_eq. simpl in B1. open_conjs. subv_in m H11. rewrite <- H11. subv_in lp A2. subv_in m A2. assumption. simpl in A3. bool_to_prop_in A3. subst n'. simpl_override. simpl_override. assumption. destruct A2 as [l'' [A21 [A22 [A23 A24]]]]. remember (label_node l'') as n'' eqn: Hn''. remember (label_clock l'') as c'' eqn: Hc''. unfold guard_method in H16. assert (A3 := fold_left_and (NId*Clock) (sender_dep u) (n'', c'') (fun p => snd p <=? received s (fst p))). depremise A3. split. rewrite <- H16 at 2. f_equal. assert (B1 := msg_update_label p h s1 (message n1 c' k v u n2 lp0)). depremise B1. split. assumption. subv s1. apply in_app_iff. right. apply in_eq. simpl in B1. open_conjs. rewrite <- H11. subv_in lp A23. subv_in m A23. assumption. simpl in A3. bool_to_prop_in A3. assert (A4 := cause_received_received p h s1 l l'' n2). simpl in A4. depremise A4. split_all. assumption. assumption. assumption. assert (B1 := prec_pre_prec h l' l'' lp). depremise B1. split_all. assumption. intro. subst lp. assert (C1 := msg_update_label p h s1 (message n1 c' k v u n2 lp0)). depremise C1. split. assumption. subv s1. apply in_app_iff. right. apply in_eq. simpl in C1. open_conjs. subv_in m H5. subv_in lp0 H8. rewrite L in H8. simpl in H8. assumption. apply prec_in in B1. destruct B1 as [B1 _]. eapply cause_prefix_history_one. split_all. apply step_star_app_one. exists s1. split; eassumption. assumption. assumption. subst c''. subst n''. subv s1. simpl_override. assumption. assumption. simpl. subst c. subst n. subv_in s1 A4. subst n'. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)