proposition: Lemma get_from_map: forall p h s s' l, (step_star (init p) h s /\ label_is_get l /\ step s l s') -> let k := label_key l in let n' := label_orig_node l in let c' := label_clock l in let n := label_node l in let m := store (alg_state ((node_states s) n)) in let d := dep (label_post_state l) in let iv := entry_val (m k) in let ivn := inst_val_nid iv in let ivc := inst_val_clock iv in (n' = ivn /\ c' = ivc /\ (n' <> init_nid -> In (n', c') d)).
proof: Proof. intros. open_conjs. inversion H1. simpl in *. subst l0. rewrite <- H4 in H0. unfold label_is_get in H0. contradiction. simpl in *. subst n'. subst c'. subst ivn. subst ivc. rewrite <- H4. simpl. subst n'0. subst c'0. subst u. subst iv. subst m. subst d. subst s. subst s'. subst k. subst n. rewrite <- H4. simpl. simpl_override. simpl. split_all. reflexivity. reflexivity. intros. assert (A := inst_entry_eq p h (state (override nss n0 (node_state (get _ k0 p0) s0 c)) ms e) n0 k0). simpl in A. depremise A. assumption. simpl_override_in A. simpl in A. destruct A as [A1 A2]. rewrite A1. rewrite A2. destruct (inst_val_nid (entry_val (store s0 k0)) <>? init_nid) eqn: Hn. apply in_eq. bool_to_prop_in Hn. contradiction. simpl in *. rewrite <- H5 in H0. unfold label_is_get in H0. contradiction. simpl in *. subv_in l H0. contradiction. Qed.
imports: Coq(FunctionalExtensionality List Bool) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Coq(Program.Basics) Chapar(Predefs extralib KVStore)