proposition: Lemma reads_from_cause: forall p h s1 l s2, let n' := label_orig_node l in let c' := label_clock l in let k := label_key l in let n := label_node l in (step_star (init p) h s1 /\ step s1 l s2 /\ label_is_get l /\ n' <> init_nid) -> exists l', label_is_put l' /\ label_node l' = n' /\ label_clock l' = c' /\ cause (h ++ [l]) l' l.
proof: Proof. intros. destruct H as [N1 [N2 [N3 N4]]]. assert (L := get_from_map p h s1 s2 l). depremise L. split_all; assumption. assert (M := in_map_from_put_update p h s1 k n). depremise M. assumption. destruct M as [M | M]. simpl in L. subst k. remember (label_key l) as k eqn: Hk . subst n. remember (label_node l) as n eqn: Hn . destruct L as [L1 [L2 L3]]. destruct M as [M1 M2]. clear L2 L3 M2. rewrite M1 in L1. subst n'. contradiction. destruct M as [lw [M | M]]. destruct M as [M1 [M2 [M3 [M4 M5]]]]. simpl in L. destruct L as [L1 [L2 _]]. subst k. remember (label_key l) as k eqn: Hk. subst n. remember (label_node l) as n eqn: Hn. remember (alg_state (node_states s1 n)) as as1 eqn: Ha. exists lw. split_all. assumption. rewrite M3. rewrite <- L1. subst n'. reflexivity. rewrite M4. rewrite <- L2. subst c'. reflexivity. apply cause_cause_step. unfold cause_step. right. split_all. apply in_split in M1. destruct M1 as [l1 [l2 M1]]. unfold prec. rewrite M1. exists l1. exists l2. exists nil. rewrite app_assoc. reflexivity. assumption. assumption. rewrite M3. rewrite <- L1. reflexivity. rewrite M4. rewrite <- L2. reflexivity. destruct M as [M1 [M2 [M3 [M4 M5]]]]. simpl in L. destruct L as [L1 [L2 _]]. subst k. remember (label_key l) as k eqn: Hk. subst n. remember (label_node l) as n eqn: Hn. remember (alg_state (node_states s1 n)) as as1 eqn: Ha. assert (P := in_exec h (init p) s1 lw). depremise P. split; assumption. destruct P as [h2'' [s2'' [s3'' [h3'' [P1 [P2 [P3 P4]]]]]]]. assert (Q := update_dep s2'' s3'' lw). depremise Q. split; assumption. simpl in Q. destruct Q as [me [Q1 [Q2 [Q3 [Q4 _]]]]]. assert (R := message_pre_put p h2'' s2'' me). simpl in R. depremise R. split; assumption. destruct R as [lp [R1 [R2 [R3 [R4 R5]]]]]. exists lp. split_all. assumption. rewrite <- R3. rewrite <- Q2. rewrite M3. rewrite <- L1. subst n'. reflexivity. rewrite <- R4. rewrite <- Q3. rewrite M4. rewrite <- L2. subst c'. reflexivity. apply cause_cause_step. unfold cause_step. right. split_all. apply in_split in R1. destruct R1 as [l1 [l2 R1]]. unfold prec. rewrite P1. rewrite R1. exists l1. exists (l2++lw::h3''). exists nil. rewrite app_assoc. rewrite app_comm_cons. rewrite app_assoc. reflexivity. assumption. assumption. rewrite <- R3. rewrite <- Q2. rewrite M3. rewrite <- L1. reflexivity. rewrite <- R4. rewrite <- Q3. rewrite M4. rewrite <- L2. reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)