proposition: Lemma get_from_map: forall (s s': State)(l: Label), (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 iv := m k in let ivn := inst_val_nid (entry_val iv) in let ivc := inst_val_clock (entry_val iv) in (n' = ivn /\ c' = ivc).
proof: Proof. intros. open_conjs. inversion H0. simpl in *. rewrite <- H3 in H. unfold label_is_get in H. contradiction. simpl in *. subst n'. subst c'. subst ivn. subst ivc. rewrite <- H3. simpl. subst n'0. subst c'0. subst u. subst iv. subst m. subst s. subst k. subst n. rewrite <- H3. simpl. simpl_override. simpl. split; reflexivity. simpl in *. rewrite <- H4 in H. unfold label_is_get in H. contradiction. simpl in *. subv_in l H. contradiction. Qed.
imports: Coq(FunctionalExtensionality List Bool Program.Basics) Coq(Arith Arith.Peano_dec Arith.Compare_dec) Chapar(Predefs extralib KVStore)