proposition: Lemma message_pre_put: forall p h s m, let ms := messages s in (step_star (init p) h s /\ In m ms) -> let mn := msg_sender m in let mc := msg_clock m in let u := msg_update m in let mco := sender_clock u in exists l, let n := label_node l in let c := label_clock l in let ls := label_post_state l in let co := clock ls in In l h /\ label_is_put l /\ mn = n /\ mc = c /\ mco = co.
proof: Proof. intros. open_conjs. remember (init p) as p0 eqn: Hp. induction H. subst ms. subst s. unfold init in H0. simpl in H0. contradiction. simpl in IHstep_star. depremise IHstep_star. assumption. inversion H1. subst ms. rewrite <- H5 in H0. simpl in H0. apply in_app_iff in H0. destruct H0. depremise IHstep_star. rewrite <- H3. simpl. assumption. destruct IHstep_star as [l' [L1 [L2 [L3 [L4 L5]]]]]. exists l'. simpl. split_all. apply in_app_iff. left. assumption. assumption. assumption. assumption. assumption. apply in_map_iff in H0. destruct H0 as [n' H0]. open_conjs. exists l. simpl. split_all. apply in_app_iff. right. subst l. apply in_eq. subst l. unfold label_is_put. apply I. subst mn. rewrite <- H4. rewrite <- H0. simpl. reflexivity. subst mc. rewrite <- H4. rewrite <- H0. simpl. reflexivity. subst mco. rewrite <- H4. simpl. apply functional_extensionality. intro n''. unfold override. destruct (eq_nat_dec n'' n). subst n''. subst u. rewrite <- H0. simpl. simpl_override. reflexivity. subst u. rewrite <- H0. simpl. simpl_override. reflexivity. depremise IHstep_star. rewrite <- H3. simpl. subst ms. rewrite <- H5 in H0. simpl in H0. assumption. destruct IHstep_star as [l' [L1 [L2 [L3 [L4 L5]]]]]. exists l'. simpl; split_all. apply in_app_iff. left. assumption. assumption. assumption. assumption. assumption. depremise IHstep_star. rewrite <- H4. simpl. subst ms. rewrite <- H6 in H0. simpl in H0. apply in_app_iff in H0. destruct H0. apply in_app_iff. left. assumption. apply in_app_iff. right. apply in_cons. assumption. destruct IHstep_star as [l' [L1 [L2 [L3 [L4 L5]]]]]. exists l'. simpl; split_all. apply in_app_iff. left. assumption. assumption. assumption. assumption. assumption. depremise IHstep_star. subv s2. subv_in ms H0. subv_in s3 H0. assumption. destruct IHstep_star as [l' [L1 [L2 [L3 [L4 L5]]]]]. exists l'. simpl; split_all. apply in_app_iff. left. assumption. assumption. assumption. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith List) Coq(Program.Equality ListSet Program.Basics Bool) Coq(Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs KVStore)