proposition: Lemma reads_from_dep: forall p h s l l', (step_star (init p) h s /\ prec h l l' /\ label_is_put l /\ label_is_get l' /\ label_node l = label_orig_node l' /\ label_clock l = label_clock 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 [N4 [N5 N6]]]]]. 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 := reads_from_cause p (h1++[l]++h2) s2' l' s2). simpl in A2. depremise A2. split_all. apply step_star_app. exists s1. split. assumption. apply step_star_end. exists s1'. split; assumption. assumption. assumption. rewrite <- N5. eapply label_node_not_in_nids. split. apply N1. apply prec_in in N2. destruct N2; assumption. destruct A2 as [lp [A21 [A22 [A24 A25]]]]. assert (A3 := put_unique p h s l lp). depremise A3. split_all. assumption. apply prec_in in N2. destruct N2; assumption. apply cause_in in A25. destruct A25 as [A25 _]. rewrite A16. rewrite app_comm_cons. rewrite app_assoc. apply in_app_iff in A25. destruct A25. apply in_app_iff. left. assumption. apply in_app_iff. right. simpl in H. destruct H; try contradiction. subst l'. apply in_eq. assumption. assumption. rewrite N5. rewrite <- A22. reflexivity. rewrite N6. rewrite <- A24. reflexivity. subst lp. destruct (eq_nat_dec (label_node l) (label_node l')). assert (A4 := prec_in_dep p (h1++[l]) s1' (h2++[l']) s2 l (label_node l)). simpl in A4. depremise A4. split_all. apply step_star_app_one. exists s1. split; assumption. apply step_star_app_one. exists s2'. split; assumption. assumption. apply in_app_iff. right. apply in_eq. left. destruct l; simpl in *; try contradiction. inversion A12. simpl. simpl_override. simpl. left. rewrite H2. assert (B1 := sem_clock_alg_state_clock p h1 s1 n1). simpl in B1. depremise B1. assumption. subst s1. simpl in B1. simpl_override_in B1. simpl in B1. rewrite B1. reflexivity. assert (B1: dep (alg_state (node_states s2 (label_node l'))) = label_dep l'). destruct l'; simpl in *; try contradiction. inversion A14. simpl. simpl_override. simpl. reflexivity. destruct A4 as [A41 | A42]. left. rewrite e in A41 at 2. rewrite B1 in A41. assumption. right. destruct A42 as [le [A421 [A422 [A423 A424]]]]. exists le. split_all. assumption. rewrite A16. rewrite cons_to_app. assert (B2 := cons_to_app h3 l'). rewrite B2. clear B2. rewrite app_assoc. rewrite app_assoc. rewrite app_assoc. eapply cause_ext_cause. rewrite <- app_assoc. apply A422. rewrite e in A423. rewrite B1 in A423. assumption. rewrite app_assoc in A424. apply in_app_iff in A424. destruct A424 as [A424 | A424]. rewrite A16. apply in_split in A424. destruct A424 as [l1 [l2 A424]]. rewrite cons_to_app. rewrite app_assoc. rewrite app_assoc. rewrite A424. unfold prec. exists l1. exists l2. exists h3. rewrite app_assoc. reflexivity. simpl in A424. destruct A424; try contradiction. subst le. destruct l'; simpl in *; contradiction. left. assert (A3 := label_node_not_in_nids p (h1++[l]) s1' l). depremise A3. split. apply step_star_app_one. exists s1. split; assumption. apply in_app_iff. right. apply in_eq. assert (A4 := get_from_map p (h1++[l]++h2) s2' s2 l'). simpl in A4. depremise A4. split_all. apply step_star_app. exists s1. split. assumption. apply step_star_end. exists s1'. split; assumption. assumption. assumption. assert (A5 := inst_entry_eq p (h1++[l]++h2) s2' (label_node l') (label_key l')). simpl in A5. depremise A5. split_all. apply step_star_app. exists s1. split. assumption. apply step_star_end. exists s1'. split; assumption. destruct l'; simpl in *; try contradiction. inversion A14. subst n2. subst k. rewrite <- H0 in A4. simpl in A4. simpl_override_in A4. simpl in A4. destruct A4 as [A41 [A42 A43]]. rewrite <- H0 in A5. simpl in A5. simpl_override_in A5. simpl in A5. destruct A5 as [A51 A52]. subst s'. subst r. simpl. rewrite A22. rewrite A24. rewrite A41. rewrite A42. rewrite A51. rewrite A52. destruct (inst_val_nid (entry_val (store s0 k0)) =? init_nid) eqn: He. bool_to_prop_in He. subst n1. subst n'. rewrite <- H2 in A3. subst u. simpl in A3. contradiction. bool_to_prop_in He. simpl. left. reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)