proposition: Lemma cause_received_received: forall p h s l l' n'', let rec := received (alg_state (node_states s n'')) in let n := label_node l in let c := label_clock l in let n' := label_node l' in let c' := label_clock l' in (step_star (init p) h s /\ label_is_put l /\ label_is_put l' /\ cause h l l' /\ c' <= rec n' /\ In n'' nids) -> c <= rec n.
proof: Proof. intros. destruct H as [H1 [H2 [H3 [H4 [H5 Hnid]]]]]. remember (init p) as s0 eqn: Hi. subst c. subst c'. subst n. subst n'. subst rec. generalize dependent l'. generalize dependent l. induction H1 as [s | s1 h s2 lc s3 H11 H12 H13]. intros. apply cause_in in H4. open_conjs. unfold In in H. contradiction. intros. depremise H12. assumption. assert (A1 := H4). apply cause_in in A1. destruct A1 as [_ A1]. assert (A2 := eq_label_dec p (h ++ [lc]) s3 lc l'). depremise A2. split_all. apply step_star_app_one. exists s2. subst s1. split; assumption. apply in_app_iff. right. apply in_eq. assumption. destruct A2 as [A2 | A2]. subst lc. clear A1. remember (label_node l) as n eqn: Hn. remember (label_clock l) as c eqn: Hc. remember (label_node l') as n' eqn: Hn'. remember (label_clock l') as c' eqn: Hc'. destruct (eq_nat_dec n'' n'). assert (A3 := cause_dep p (h++[l']) s3 l l'). depremise A3. split_all. apply step_star_app_one. exists s2. subst s1. split; assumption. assumption. assumption. destruct A3 as [A3 | A3]. clear H12. subst n''. assert (A4 := dep_received p h s2 n' n c). simpl in A4. depremise A4. split_all. subst s1. assumption. assert (B1: label_dep l' = dep (alg_state (node_states s2 n'))). destruct l'; simpl in *; try contradiction. inversion H13. simpl. simpl_override. simpl. reflexivity. rewrite <- B1. subst n. subst c. assumption. assert (B1 := rec_inc p h s2 [l'] s3 n' n). depremise B1. split_all. subst s1. assumption. apply step_star_one. assumption. eapply Nat.le_trans; eassumption. destruct A3 as [lm [A31 [A32 [A33 A34]]]]. subst n''. remember (label_node lm) as nm eqn: Hnm. remember (label_clock lm) as cm eqn: Hcm. assert (A4 := dep_received p h s2 n' nm cm). simpl in A4. depremise A4. split_all. subst s1. assumption. assert (B1: label_dep l' = dep (alg_state (node_states s2 n'))). destruct l'; simpl in *; try contradiction. inversion H13. simpl. simpl_override. simpl. reflexivity. rewrite <- B1. assumption. specialize (H12 l). depremise H12. assumption. specialize (H12 lm). depremise H12. assumption. depremise H12. assert (A5 := prec_pre_in p h s3 l' lm). depremise A5. split. apply step_star_app_one. exists s2. subst s1. split; assumption. assumption. eapply cause_prefix_history_one. split_all. subst s1. apply step_star_app_one. exists s2. split; eassumption. assumption. assumption. depremise H12. subst nm. subst cm. assumption. subst c. subst n. assert (B1 := rec_inc p h s2 [l'] s3 n' (label_node l)). depremise B1. split_all. subst s1. assumption. apply step_star_one. assumption. eapply Nat.le_trans; eassumption. exfalso. destruct l'; simpl in *; try contradiction. inversion H13. simpl in *. assert (B1: In (message n2 (c1 + 1) k v u0 n'' l1) (messages s3)). rewrite <- H1. simpl. apply in_app_iff. right. apply in_map_iff. exists n''. split. reflexivity. apply filter_In. split. assumption. rewrite <- Hn'. rewrite eq_nat_dec_neq. reflexivity. apply not_eq_sym. assumption. assert (B2 := received_lt_message_clock p (h++[(put_label n1 n2 c0 k v a a0 u)]) s3 (message n2 (c1 + 1) k v u0 n'' l1) n''). simpl in B2. depremise B2. split_all. apply step_star_app_one. exists s2. subst s1. split; assumption. rewrite <- H1. simpl. apply in_app_iff. right. apply in_map_iff. exists n''. split. reflexivity. apply filter_In. split. assumption. rewrite <- Hn'. rewrite eq_nat_dec_neq. reflexivity. apply not_eq_sym. assumption. reflexivity. rewrite <- H1 in B2. simpl in B2. rewrite <- Hn' in B2. simpl_override_in B2. subst c'. subst c0. rewrite <- H1 in H5. simpl in H5. rewrite <- Hn' in H5. simpl_override_in H5. apply Nat.lt_nge in B2. contradiction. assert (A3 := cause_pre_cause p h s3 lc l l'). depremise A3. split_all. apply step_star_app_one. exists s2. subst s1. split; assumption. assumption. assumption. apply in_app_iff in A1. simpl in A1. destruct A1 as [A1 | [A1 | A1]]; try contradiction. assert (A4 := rec_inc p h s2 [lc] s3 n'' (label_node l)). depremise A4. split. subst s1. assumption. apply step_star_one. assumption. destruct (eq_nat_dec (label_node lc) n''). destruct lc. specialize (H12 l). depremise H12. assumption. specialize (H12 l'). depremise H12. assumption. depremise H12. assumption. destruct (eq_nat_dec n'' (label_node l')). clear H5. subst n''. simpl in *. subst n0. assert (A5 := clock_self_lte_received p h s2 l'). simpl in A5. depremise A5. split_all. subst s1. assumption. assumption. assumption. depremise H12. assumption. eapply Nat.le_trans; eassumption. assert (A5: received (alg_state (node_states s2 n'')) (label_node l') = received (alg_state (node_states s3 n'')) (label_node l')). inversion H13. simpl. subst r. subst l1. subst n''. simpl. simpl_override. simpl_override. simpl. rewrite H6. subst n0. simpl_override. subst a. reflexivity. rewrite A5 in H12. depremise H12. assumption. eapply Nat.le_trans; eassumption. specialize (H12 l). depremise H12. assumption. specialize (H12 l'). depremise H12. assumption. depremise H12. assumption. assert (A5: received (alg_state (node_states s2 n'')) (label_node l') = received (alg_state (node_states s3 n'')) (label_node l')). inversion H13. simpl. subst n1. subst n''. simpl. simpl_override. simpl_override. simpl. subst a. reflexivity. rewrite A5 in H12. depremise H12. assumption. eapply Nat.le_trans; eassumption. destruct (eq_nat_dec n0 (label_node l')). apply Nat.lt_eq_cases in H5. destruct H5 as [H5 | H5]. specialize (H12 l). depremise H12. assumption. specialize (H12 l'). depremise H12. assumption. depremise H12. assumption. subst n0. assert (A5: received (alg_state (node_states s3 n'')) (label_node l') <= S (received (alg_state (node_states s2 n'')) (label_node l'))). inversion H13. subst s'1. subst s'2. subst s'3. subst s'4. subst s'5. subst c. subst n1. subst k. subst v. subst a. simpl. subst n''. simpl. simpl_override. simpl_override. simpl. assert (B1 := message_update_node_clock_eq p h s2 (message n' c' k0 v0 u n0 lp)). simpl in B1. depremise B1. split_all. subst s1. assumption. rewrite <- H1. simpl. apply in_app_iff. right. apply in_eq. destruct B1 as [B11 B12]. rewrite <- B11. subst n'. simpl_override. assert (B2 := update_sender_clock p h s2 (update_label n (label_node l') c' n0 k0 v0 s m a0) s3). simpl in B2. depremise B2. split_all. subst s1. assumption. assumption. apply I. rewrite <- H1 in B2. simpl in B2. simpl_override_in B2. simpl in B2. subst m. simpl in B2. rewrite Nat.add_comm in B2. simpl in B2. assumption. assert (A6: label_clock l' < S (received (alg_state (node_states s2 n'')) (label_node l'))). eapply Nat.lt_le_trans; eassumption. apply (proj1 (Nat.lt_succ_r _ _)) in A6. depremise H12. assumption. eapply Nat.le_trans; eassumption. assert (A5 := cause_dep p h s2 l l'). depremise A5. subst s1. split_all; assumption. destruct A5 as [A5 | A5]. clear H12. remember (update_label n n0 c n1 k v a m a0) as lc eqn: Hl. assert (B1 := msg_update_label p h s2 m). depremise B1. split. subst s1. assumption. subst lc. inversion H13. subst s2. simpl. apply in_app_iff. right. apply in_eq. simpl in B1. destruct B1 as [B11 [B12 [B13 [B14 [B15 _]]]]]. assert (B2: sender_node (msg_update m) = label_node l'). subst lc. inversion H13. simpl. rewrite <- e0. assert (C1 := message_update_node_clock_eq p h s2 (message n' c' k0 v0 u n2 lp)). simpl in C1. depremise C1. split. subst s1. assumption. subst s2. simpl. apply in_app_iff. right. apply in_eq. destruct C1 as [C1 _]. subst n'. symmetry. assumption. assert (B3: sender_clock (msg_update m) = label_clock l'). rewrite H5. subst lc. inversion H13. simpl. subst n''. simpl. simpl_override. simpl. assert (C1 := message_update_node_clock_eq p h s2 (message n' c' k0 v0 u n2 lp)). simpl in C1. depremise C1. split. subst s1. assumption. subst s2. simpl. apply in_app_iff. right. apply in_eq. destruct C1 as [C11 C12]. rewrite <- C11. rewrite H0. rewrite e0. simpl_override. reflexivity. rewrite B2 in B13. clear B2. rewrite B3 in B14. clear B3. assert (B4 := put_unique p h s2 (msg_label m) l'). depremise B4. subst s1. split_all; assumption. rewrite B4 in *; clear B4. clear B11 B12 B13 B14. rewrite B15 in A5; clear B15. assert (B5: label_clock l <= received (alg_state (node_states s2 n'')) (label_node l)). subst lc. inversion H13. simpl in *. subst n''. simpl in *. simpl_override. simpl. subst a. unfold guard_method in H17. assert (A:= fold_left_and (NId*Clock) (sender_dep u) (label_node l, label_clock l) (fun p => snd p <=? received s (fst p))). depremise A. split. assumption. subst m. simpl in *. assumption. simpl in A. bool_to_prop_in A. assumption. eapply Nat.le_trans; eassumption. destruct A5 as [l'' [A51 [A52 [A53 A54]]]]. specialize (H12 l). depremise H12. assumption. specialize (H12 l''). depremise H12. assumption. depremise H12. assumption. remember (update_label n n0 c n1 k v a m a0) as lc eqn: Hl. assert (B1 := msg_update_label p h s2 m). depremise B1. split. subst s1. assumption. subst lc. inversion H13. subst s2. simpl. apply in_app_iff. right. apply in_eq. simpl in B1. destruct B1 as [B11 [B12 [B13 [B14 [B15 _]]]]]. assert (B2: sender_node (msg_update m) = label_node l'). subst lc. inversion H13. simpl. rewrite <- e0. assert (C1 := message_update_node_clock_eq p h s2 (message n' c' k0 v0 u n2 lp)). simpl in C1. depremise C1. split. subst s1. assumption. subst s2. simpl. apply in_app_iff. right. apply in_eq. destruct C1 as [C11 C12]. subst n'. symmetry. assumption. assert (B3: sender_clock (msg_update m) = label_clock l'). rewrite H5. subst lc. inversion H13. simpl. subst n''. simpl. simpl_override. simpl. assert (C1 := message_update_node_clock_eq p h s2 (message n' c' k0 v0 u n2 lp)). simpl in C1. depremise C1. split. subst s1. assumption. subst s2. simpl. apply in_app_iff. right. apply in_eq. destruct C1 as [C11 C12]. rewrite <- C11. rewrite H0. rewrite e0. simpl_override. reflexivity. rewrite B2 in B13. clear B2. rewrite B3 in B14. clear B3. assert (B4 := put_unique p h s2 (msg_label m) l'). depremise B4. subst s1. split_all; assumption. rewrite B4 in *; clear B4. clear B11 B12 B13 B14. rewrite B15 in A53; clear B15. assert (B5: label_clock l'' <= received (alg_state (node_states s2 n'')) (label_node l'')). subst lc. inversion H13. simpl in *. subst n''. simpl in *. simpl_override. simpl. subst a. unfold guard_method in H18. assert (A:= fold_left_and (NId*Clock) (sender_dep u) (label_node l'', label_clock l'') (fun p => snd p <=? received s (fst p))). depremise A. split. assumption. subst m. simpl in *. assumption. simpl in A. bool_to_prop_in A. assumption. depremise H12. assumption. eapply Nat.le_trans; eassumption. specialize (H12 l). depremise H12. assumption. specialize (H12 l'). depremise H12. assumption. depremise H12. assumption. assert (A5: received (alg_state (node_states s2 n'')) (label_node l') = received (alg_state (node_states s3 n'')) (label_node l')). inversion H13. simpl. subst n1. subst n''. simpl. simpl_override. simpl_override. simpl. assert (B1 := message_update_node_clock_eq p h s2 (message n' c' k0 v0 u n3 lp)). simpl in B1. depremise B1. split_all. subst s1. assumption. rewrite <- H1. simpl. apply in_app_iff. right. apply in_eq. destruct B1 as [B11 B12]. rewrite <- B11. subst n'. simpl_override. subst a. reflexivity. rewrite A5 in H12. depremise H12. assumption. eapply Nat.le_trans; eassumption. specialize (H12 l). depremise H12. assumption. specialize (H12 l'). depremise H12. assumption. depremise H12. assumption. assert (A5: received (alg_state (node_states s2 n'')) (label_node l') = received (alg_state (node_states s3 n'')) (label_node l')). inversion H13. simpl. subst n1. subst n''. simpl. simpl_override. simpl_override. simpl. subst a. reflexivity. rewrite A5 in H12. depremise H12. assumption. eapply Nat.le_trans; eassumption. specialize (H12 l). depremise H12. assumption. specialize (H12 l'). depremise H12. assumption. depremise H12. assumption. assert (A5: received (alg_state (node_states s2 n'')) (label_node l') = received (alg_state (node_states s3 n'')) (label_node l')). destruct lc; inversion H13; simpl; simpl_override; simpl_override; reflexivity. rewrite A5 in H12. depremise H12. assumption. eapply Nat.le_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)