proposition: Lemma proc_order_clock: forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(l l': Label)(n: NId), (step_star (init p) h s /\ prec h l l' /\ label_node l = label_node l') -> (let c := dep (label_post_state l) n in let c' := dep (label_post_state l') n in c <= c' /\ ((label_node l' = n /\ label_is_put l') -> c < c')).
proof: Proof. intros. destruct H as [H1 [H2 H3]]. assert (L := prec_exec p h s l l'). depremise L. split; assumption. destruct L as [h1 L]. destruct L as [s1 L]. destruct L as [s' L]. destruct L as [h2 L]. destruct L as [s'' L]. destruct L as [s2 L]. destruct L as [h3 [L1 [L3 [L4 [L5 L2]]]]]. assert (M1 := step_star_clock_nondec p (h1 ++ [l]) h2 s' s'' (label_node l)). simpl in M1. depremise M1. split. apply step_star_app_one. exists s1. split; assumption. assumption. specialize (M1 n). subst c. subst c'. assert (N1 := label_poststate_state s1 s' l L3). assert (N2 := label_poststate_state s'' s2 l' L5). rewrite N1; clear N1. rewrite N2; clear N2. assert (L: dep (alg_state (node_states s'' (label_node l))) n <= dep (alg_state (node_states s2 (label_node l'))) n /\ (label_node l' = n /\ label_is_put l' -> dep (alg_state (node_states s'' (label_node l))) n < dep (alg_state (node_states s2 (label_node l'))) n)). clear M1. rewrite H3 in *. inversion L5. simpl. simpl_override. simpl. simpl_override. simpl. destruct (eq_nat_dec n n0). simpl_override. assert (A:= dep_leq_rec p (h1 ++ l :: h2) s'' n0). simpl in A. depremise A. apply step_star_app. exists s1. split. assumption. apply step_star_end. exists s'. split; assumption. specialize (A n0). rewrite <- H0 in A. simpl in A. simpl_override_in A. simpl in A. depremise A. assert (B := label_node_in_nids p (h1 ++ [l] ++ h2 ++ [l']) s2 l'). depremise B. split. apply step_star_app. exists s1. split. assumption. apply step_star_app. exists s'. split. apply step_star_one. assumption. apply step_star_app_one. exists s''. split; assumption. apply in_app_iff. right. apply in_app_iff. right. apply in_app_iff. right. apply in_eq. simpl in B. subst l'. subst l0. simpl in B. assumption. split. rewrite Nat.add_comm. simpl. subst n. apply le_S. assumption. intro. rewrite Nat.add_comm. simpl. subst n. apply Nat.lt_succ_r. assumption. simpl_override. split. apply Nat.le_refl. intros. destruct H6. exfalso. apply n1. symmetry; assumption. simpl. simpl_override. simpl. simpl_override. simpl. split. destruct (eq_nat_dec (entry_node (store s0 k)) n). simpl_override. rewrite e0. apply Nat.le_max_l. simpl_override. apply Nat.le_refl. intros. destruct H6. contradiction. simpl. split. simpl_override. simpl. simpl_override. simpl. apply Nat.le_max_l. intro. open_conjs. contradiction. simpl. simpl_override. simpl_override. split. apply Nat.le_refl. intros. open_conjs. contradiction. destruct L as [N1 N2]. split. rewrite <- H3 in *; clear H3. eapply Nat.le_trans; eassumption. clear N1. intros. depremise N2. assumption. clear H. eapply Nat.le_lt_trans; eassumption. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)