proposition: Lemma in_dep_get_or_put: forall p h s n, let d := dep (alg_state (node_states s n)) in step_star (init p) h s -> forall id, let n' := fst id in let c' := snd id in In id d -> (exists l' l, label_node l = n /\ label_is_get l /\ label_is_put l' /\ label_node l' = n' /\ label_clock l' = c' /\ cause h l' l) \/ (exists l, label_node l = n /\ label_node l = n' /\ label_clock l = c' /\ label_is_put l /\ In l h).
proof: Proof. intros. remember (init p) as s0 eqn: Hs. induction H as [s | s1 h s2 l s3 N1 N2 N3]. subst d. subst s. simpl in H0. contradiction. simpl in N2. depremise N2. assumption. destruct (eq_nat_dec (label_node l) n). inversion N3. subst l0. rewrite <- H2 in e. simpl in e. subst d. subst n. rewrite <- H3 in H0. simpl in H0. simpl_override_in H0. simpl in H0. destruct H0 as [H0 | H0]; try contradiction. right. clear N2. exists l. split_all. subst l. simpl. reflexivity. subst l. simpl. subst n'. subst id. simpl. reflexivity. subst l. simpl. subst c'. subst id. simpl. assert (A := sem_clock_alg_state_clock p h s2 n0). simpl in A. depremise A. subst s1. assumption. rewrite <- H1 in A. simpl in A. simpl_override_in A. simpl in A. rewrite A. reflexivity. subst l. simpl. apply I. subst l. apply in_app_iff. right. apply in_eq. rewrite <- H2 in e. simpl in e. subst d. subst n. rewrite <- H3 in H0. simpl in H0. simpl_override_in H0. simpl in H0. assert (A1: (id = (entry_node (store s k), entry_clock (store s k)) /\ entry_node (store s k) <> init_nid) \/ In id (dep s)). destruct (entry_node (store s k) <>? init_nid) eqn: Hn. simpl in H0. destruct H0. left. split. symmetry. assumption. bool_to_prop_in Hn. assumption. right. assumption. right. assumption. clear H0. destruct A1 as [A1 | A1]. destruct A1 as [A11 A12]. clear N2. left. assert (A2 := reads_from_cause p h s2 l s3). simpl in A2. depremise A2. split_all. subst s1. assumption. assumption. subst l. simpl. apply I. subst l. simpl. subst n'0. subst u. subst r. simpl. assert (A := inst_entry_eq p h s2 n0 k). depremise A. subst s1. assumption. simpl in A. rewrite <- H1 in A. simpl in A. simpl_override_in A. simpl in A. destruct A as [A1 A2]. rewrite A1 in A12. assumption. rewrite <- H2 in A2. simpl in A2. destruct A2 as [l' [A21 [A22 [A23 A24]]]]. assert (A3:= inst_entry_eq p h s2 n0 k). depremise A3. subst s1. assumption. simpl in A3. rewrite <- H1 in A3. simpl in A3. simpl_override_in A3. simpl in A3. destruct A3 as [A31 A32]. exists l'. exists l. split_all. subst l. simpl. reflexivity. subst l. simpl. apply I. assumption. clear A24. rewrite A22. subst n'0. subst u. subst r. subst n'. subst id. simpl. symmetry. assumption. clear A24. rewrite A23. subst c'0. subst u. subst r. subst c'. subst id. simpl. symmetry. assumption. rewrite H2 in *. assumption. rewrite <- H1 in N2. simpl in N2. simpl_override_in N2. simpl in N2. depremise N2. assumption. destruct N2 as [N2 | N2]. destruct N2 as [l' [l'' [N21 [N22 [N23 [N24 [N25 N26]]]]]]]. left. exists l'. exists l''. split_all. assumption. assumption. assumption. assumption. assumption. eapply cause_ext_cause. assumption. destruct N2 as [l' [N21 [N22 [N23 [N24 N25]]]]]. right. exists l'. split_all. assumption. assumption. assumption. assumption. apply in_app_iff. left. assumption. rewrite <- H3 in e. simpl in e. subst d. subst n. rewrite <- H4 in H0. simpl in H0. simpl_override_in H0. simpl in H0. rewrite <- H2 in N2. simpl in N2. simpl_override_in N2. simpl in N2. depremise N2. assumption. destruct N2 as [N2 | N2]. destruct N2 as [l' [l'' [N21 [N22 [N23 [N24 [N25 N26]]]]]]]. left. exists l'. exists l''. split_all. assumption. assumption. assumption. assumption. assumption. eapply cause_ext_cause. assumption. destruct N2 as [l' [N21 [N22 [N23 [N24 N25]]]]]. right. exists l'. split_all. assumption. assumption. assumption. assumption. apply in_app_iff. left. assumption. rewrite <- H2 in e. simpl in e. subst d. subst n. rewrite <- H3 in H0. simpl in H0. simpl_override_in H0. simpl in H0. depremise N2. subv s2. simpl_override. assumption. destruct N2 as [N2 | N2]. destruct N2 as [l' [l'' [N21 [N22 [N23 [N24 [N25 N26]]]]]]]. left. exists l'. exists l''. split_all. assumption. assumption. assumption. assumption. assumption. eapply cause_ext_cause. assumption. destruct N2 as [l' [N21 [N22 [N23 [N24 N25]]]]]. right. exists l'. split_all. assumption. assumption. assumption. assumption. apply in_app_iff. left. assumption. subst d. assert (A: dep (alg_state (node_states s3 n)) = dep (alg_state (node_states s2 n))). clear H0 N2. inversion N3; subst l; simpl in *; simpl_override; simpl_override; reflexivity. rewrite A in *. clear A. depremise N2. assumption. destruct N2 as [N2 | N2]. destruct N2 as [l' [l'' [N21 [N22 [N23 [N24 [N25 N26]]]]]]]. left. exists l'. exists l''. split_all. assumption. assumption. assumption. assumption. assumption. eapply cause_ext_cause. assumption. destruct N2 as [l' [N21 [N22 [N23 [N24 N25]]]]]. right. exists l'. split_all. assumption. assumption. assumption. assumption. apply in_app_iff. left. assumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)