proposition: Lemma cause_dep: forall p h s l l', (step_star (init p) h s /\ label_is_put l /\ cause h l l') -> (In (label_node l, label_clock l) (label_dep l') \/ (exists l'', label_is_put l'' /\ cause h l l'' /\ In (label_node l'', label_clock l'') (label_dep l') /\ prec h l'' l')).
proof: Proof. intros. destruct H as [N1 [N2 N3]]. induction N3. unfold cause_step in H. destruct H as [H | H]. destruct H as [M1 [M2 M3]]. destruct M3 as [M3 | M3]. destruct M3 as [M31 M32]. destruct l; simpl in *; try contradiction. destruct M3 as [M31 M32]. assert (A1 := prec_exec p h s l l'). depremise A1. split; assumption. destruct A1 as [h1 [s1 [s1' [h2 [s2' [s2 [h3 [A11 [A12 [A13 [A14 [A15 A16]]]]]]]]]]]]. assert (A2 := prec_in_dep p (h1 ++ [l]) s1' h2 s2' l (label_node l)). simpl in A2. depremise A2. split_all. apply step_star_app_one. exists s1. split; assumption. assumption. assumption. apply in_app_iff. right. apply in_eq. left. destruct l; simpl in *; try contradiction. clear M31. inversion A12. simpl. simpl_override. simpl. left. rewrite H2. apply f2_equal. split. reflexivity. assert (B1 := sem_clock_alg_state_clock p h1 s1 n1). simpl in B1. depremise B1. assumption. rewrite <- H0 in B1. simpl in B1. simpl_override_in B1. simpl in B1. rewrite B1. reflexivity. assert (A3: label_dep l' = dep (alg_state (node_states s2' (label_node l)))). destruct l'; simpl in *; try contradiction. clear M32. inversion A14. simpl. simpl_override. simpl. reflexivity. rewrite A3. clear A3. destruct A2 as [A2 | A2]. left. assumption. right. destruct A2 as [le [A21 [A22 [A23 A24]]]]. exists le. split_all. assumption. rewrite A16. rewrite cons_to_app. rewrite app_assoc. rewrite app_assoc. apply cause_ext_cause. assumption. assumption. apply cause_in in A22. destruct A22 as [_ A22]. apply in_split in A24. destruct A24 as [l1 [l2 A24]]. rewrite <- app_assoc in A24. rewrite <- cons_to_app in A24. rewrite app_comm_cons in A16. rewrite app_assoc in A16. rewrite A24 in A16. rewrite A16. unfold prec. exists l1. exists l2. exists h3. rewrite app_assoc. reflexivity. destruct H as [M1 [M2 [M3 [M4 M5]]]]. assert (A2 := reads_from_dep p h s l l'). depremise A2. split_all; assumption. assumption. depremise IHN3. assumption. depremise IHN3. assumption. assert (H' := H). unfold cause_step in H. destruct H. destruct H as [M1 [M2 [M3 | M3]]]; destruct M3 as [M3 M4]. assert (A1 := prec_exec p h s l' l''). depremise A1. split; assumption. destruct A1 as [h1 [s1 [s1' [h2 [s2' [s2 [h3 [A11 [A12 [A13 [A14 [A15 A16]]]]]]]]]]]]. assert (A2 := prec_in_dep p (h1++[l']) s1' h2 s2' l (label_node l')). simpl in A2. depremise A2. split_all. apply step_star_app_one. exists s1. split; assumption. assumption. assumption. apply in_app_iff. left. eapply prec_pre_post_in. split_all. subst h. rewrite <- cons_to_app. eassumption. subst h. rewrite <- cons_to_app. eapply cause_prec. split_all. eassumption. assumption. assert (B1: label_dep l' = dep (alg_state (node_states s1' (label_node l')))). destruct l'; simpl in *; try contradiction. clear M3. inversion A12. simpl. simpl_override. simpl. reflexivity. rewrite B1 in *; clear B1. destruct IHN3 as [IHN3 | IHN3]. left. assumption. right. destruct IHN3 as [le [IHN31 [IHN32 [IHN33 IHN34]]]]. exists le. split_all. assumption. assert (B2 := prec_pre_post_in p h1 (h2 ++ l'' :: h3) s le l'). depremise B2. split. apply step_star_app. exists s1. split. assumption. apply step_star_app. exists s1'. split. apply step_star_one. assumption. apply step_star_app. exists s2'. split. assumption. apply step_star_end. exists s2. split; assumption. rewrite A16 in IHN34. rewrite cons_to_app in IHN34. assumption. assert (B3 := cause_prefix_history p h1 (l' :: h2 ++ l'' :: h3) s l le). depremise B3. split_all. apply step_star_app. exists s1. split. assumption. apply step_star_end. exists s1'. split. assumption. apply step_star_app. exists s2'. split. assumption. apply step_star_end. exists s2. split; assumption. assumption. rewrite A16 in IHN32. assumption. apply cause_ext_cause. assumption. assumption. rewrite A16 in IHN34. assert (A2 := prec_pre_post_in p h1 (h2 ++ l'' :: h3) s le l'). depremise A2. split_all. subst h; assumption. assumption. apply in_app_iff. left. assumption. clear IHN3. assert (A3: label_dep l'' = dep (alg_state (node_states s2' (label_node l')))). destruct l''; simpl in *; try contradiction. clear M4. inversion A14. simpl. simpl_override. simpl. reflexivity. rewrite A3. destruct A2 as [A2 | A2]. left. assumption. right. destruct A2 as [le [A21 [A22 [A23 A24]]]]. exists le. split_all. assumption. rewrite A16. rewrite cons_to_app. rewrite app_assoc. rewrite app_assoc. eapply cause_ext_cause. assumption. assumption. apply cause_in in A22. destruct A22 as [_ A22]. apply in_split in A22. destruct A22 as [l1 [l2 A22]]. rewrite <- app_assoc in A22. rewrite <- cons_to_app in A22. rewrite app_comm_cons in A16. rewrite app_assoc in A16. rewrite A22 in A16. rewrite A16. unfold prec. exists l1. exists l2. exists h3. rewrite app_assoc. reflexivity. assert (A1 := prec_exec p h s l' l''). depremise A1. split; assumption. destruct A1 as [h1 [s1 [s1' [h2 [s2' [s2 [h3 [A11 [A12 [A13 [A14 [A15 A16]]]]]]]]]]]]. assert (A2 := prec_in_dep p h1 s1 (l' :: h2) s2' l (label_node l')). simpl in A2. depremise A2. split_all. assumption. apply step_star_end. exists s1'. split; assumption. assumption. eapply prec_pre_post_in. split_all. subst h. rewrite <- cons_to_app. eassumption. subst h. rewrite <- cons_to_app. eapply cause_prec. split_all. eassumption. assumption. assert (B1: label_dep l' = dep (alg_state (node_states s1 (label_node l')))). destruct l'; simpl in *; try contradiction. clear M3. inversion A12. simpl. simpl_override. simpl. reflexivity. rewrite B1 in *; clear B1. destruct IHN3 as [IHN3 | IHN3]. left. assumption. right. destruct IHN3 as [le [IHN31 [IHN32 [IHN33 IHN34]]]]. exists le. split_all. assumption. assert (B2 := prec_pre_post_in p h1 (h2 ++ l'' :: h3) s le l'). depremise B2. split. apply step_star_app. exists s1. split. assumption. apply step_star_app. exists s1'. split. apply step_star_one. assumption. apply step_star_app. exists s2'. split. assumption. apply step_star_end. exists s2. split; assumption. rewrite A16 in IHN34. rewrite cons_to_app in IHN34. assumption. assert (B3 := cause_prefix_history p h1 (l' :: h2 ++ l'' :: h3) s l le). depremise B3. split_all. apply step_star_app. exists s1. split. assumption. apply step_star_end. exists s1'. split. assumption. apply step_star_app. exists s2'. split. assumption. apply step_star_end. exists s2. split; assumption. assumption. rewrite A16 in IHN32. assumption. assumption. assumption. rewrite A16 in IHN34. assert (A2 := prec_pre_post_in p h1 (h2 ++ l'' :: h3) s le l'). depremise A2. split_all. subst h; assumption. assumption. assumption. clear IHN3. assert (A3: label_dep l'' = dep (alg_state (node_states s2' (label_node l')))). destruct l''; simpl in *; try contradiction. clear M4. inversion A14. simpl. simpl_override. simpl. reflexivity. rewrite A3. destruct A2 as [A2 | A2]. left. assumption. right. destruct A2 as [le [A21 [A22 [A23 A24]]]]. exists le. split_all. assumption. rewrite A16. rewrite cons_to_app. rewrite app_assoc. rewrite app_assoc. eapply cause_ext_cause. rewrite <- app_assoc. rewrite <- cons_to_app. assumption. assumption. apply cause_in in A22. destruct A22 as [_ A22]. apply in_split in A22. destruct A22 as [l1 [l2 A22]]. rewrite app_comm_cons in A16. rewrite app_assoc in A16. rewrite A22 in A16. rewrite A16. unfold prec. exists l1. exists l2. exists h3. rewrite app_assoc. reflexivity. open_conjs. clear IHN3. right. assert (A1 := reads_from_dep p h s l' l''). depremise A1. split_all; assumption. destruct A1 as [A1 | A1]. exists l'. split_all. assumption. assumption. assumption. assumption. destruct A1 as [le [A11 [A12 [A13 A14]]]]. exists le. split_all. assumption. eapply cause_cause_trans. split; eassumption. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)