Commit d881c0ba authored by Hai Dang's avatar Hai Dang

clean up

parent c3402c2b
......@@ -546,125 +546,3 @@ Proof. by rewrite lookup_insert. Qed.
Lemma res_tag_lookup_ne (k: tag_kind) (h: heaplet) (t t': ptr_id) (NEQ: t' t) :
(res_tag t k h).(rtm) !! t' None.
Proof. by rewrite lookup_insert_ne. Qed.
(** res_mapsto *)
(*
Lemma res_loc_lookup l n t :
(res_loc l n t).(rlm) !! t Some (Excl $ locs_seq l n).
Proof. rewrite /= lookup_fmap lookup_insert //. Qed.
Lemma res_mapsto_llookup l v t :
(res_mapsto l v t).(rlm) !! t Some (Excl $ locs_seq l (length v)).
Proof. rewrite lookup_op res_loc_lookup //. Qed.
Lemma res_mapsto_llookup_ne l v t t1 :
t1 t (res_mapsto l v t).(rlm) !! t1 = None.
Proof.
intros. rewrite /res_mapsto /= /to_lmUR right_id_L lookup_fmap lookup_insert_ne //.
Qed.
Lemma res_mapsto_llookup_eq l v t t1 ls1 :
(res_mapsto l v t).(rlm) !! t1 Some (Excl ls1)
t1 = t ls1 = locs_seq l (length v).
Proof.
case (decide (t1 = t)) => ?; [subst t1|].
- rewrite res_mapsto_llookup. intros. by simplify_eq.
- rewrite res_mapsto_llookup_ne //. by inversion 1.
Qed.
Lemma res_mapsto_tlookup l v (t: ptr_id) :
(res_mapsto l v t).(rtm) !! t
Some (to_tgkR tkUnique, to_agree <$> (write_hpl l v )).
Proof. by rewrite lookup_op /= lookup_empty left_id lookup_insert. Qed.
Lemma res_mapsto_tlookup_ne l v (t t': ptr_id) (NEQ: t' t) :
(res_mapsto l v t).(rtm) !! t' None.
Proof. by rewrite lookup_op /= lookup_empty left_id lookup_insert_ne. Qed.
(** allocating locals *)
Lemma res_loc_alloc_local_update (lm: lmapUR) (t: ptr_id) ls :
lm !! t = None
(lm, ε) ~l~> (lm (to_lmUR {[t := ls]}), (to_lmUR {[t := ls]})).
Proof.
intros FRESH.
rewrite /to_lmUR fmap_insert fmap_empty insert_empty
(cmra_comm _ {[t := _]}) -insert_singleton_op //.
by apply alloc_local_update.
Qed.
Lemma res_mapsto_alloc_local_update r l v t:
r.(rtm) !! t = None r.(rlm) !! t = None
(r, ε) ~l~> (r res_mapsto l v t, res_mapsto l v t).
Proof.
intros FRESH1 FRESH2. destruct r as [[tm cm] lm].
rewrite /res_mapsto (cmra_comm (res_loc _ _ _)).
etrans.
- by apply (res_tag_alloc_local_update _ t tkUnique (write_hpl l v )).
- rewrite !pair_op !right_id left_id /=.
by apply prod_local_update_2, res_loc_alloc_local_update.
Qed.
(** deallocating locals *)
Lemma res_loc_dealloc_local_update (lm: lmapUR) t ls:
lm !! t = None
(lm (to_lmUR {[t := ls]}), to_lmUR {[t := ls]}) ~l~> (lm, ε).
Proof.
intros ?.
rewrite /to_lmUR fmap_insert fmap_empty insert_empty
(cmra_comm _ {[t := _]}) -insert_singleton_op; [|done].
etrans.
- eapply (delete_local_update_cancelable _ _ t); [|by rewrite lookup_insert..].
apply _.
- rewrite 2!delete_insert_delete delete_empty delete_notin //.
Qed.
Lemma res_mapsto_res_tag (r: resUR) l v t k' h'
(NONE1: r.(rlm) !! t = None)
(NONE2: r.(rtm) !! t = None):
(r res_mapsto l v t, res_mapsto l v t) ~l~>
(r res_tag t k' h', res_tag t k' h').
Proof.
rewrite /res_mapsto. destruct r as [[tm cm] lm].
rewrite (cmra_comm (res_loc _ _ _)) cmra_assoc. etrans.
- apply prod_local_update_2. rewrite /= right_id left_id.
by apply res_loc_dealloc_local_update.
- rewrite !pair_op /= !right_id.
apply prod_local_update_1, prod_local_update_1. rewrite /=.
by apply (res_tag_uniq_insert_local_update_inner _ _ k').
Qed.
(** updating locals *)
Lemma res_mapsto_1_insert_local_update (r: resUR) (l: loc) s1 s2 (t: ptr_id)
(NONE: r.(rtm) !! t = None) :
(r res_mapsto l [s1] t, res_mapsto l [s1] t) ~l~>
(r res_mapsto l [s2] t, res_mapsto l [s2] t).
Proof.
intros. rewrite /res_mapsto cmra_assoc. etrans.
- eapply res_tag_1_insert_local_update_r.
by rewrite lookup_op NONE /= lookup_empty right_id_L.
- rewrite -(cmra_assoc r) 2!(cmra_comm (res_loc _ _ _)) 2!cmra_assoc
/= insert_empty //.
Qed.
Lemma res_mapsto_tdom l v t:
dom (gset nat) (res_mapsto l v t).(rtm) {[t]}.
Proof.
intros t1.
rewrite elem_of_dom /res_mapsto lookup_op /= left_id elem_of_singleton.
case (decide (t1 = t)) => ?.
- subst t1. rewrite lookup_insert. naive_solver.
- rewrite lookup_insert_ne // lookup_empty. split; [by destruct 1|done].
Qed.
Lemma res_mapsto_ldom l v t:
dom (gset nat) (res_mapsto l v t).(rlm) {[t]}.
Proof.
intros t1.
rewrite elem_of_dom /res_mapsto lookup_op /= right_id elem_of_singleton
/to_lmUR lookup_fmap.
case (decide (t1 = t)) => ?.
- subst t1. rewrite lookup_insert. naive_solver.
- rewrite lookup_insert_ne // lookup_empty. split; [by destruct 1|done].
Qed. *)
......@@ -313,7 +313,7 @@ Proof using Type*.
eapply (Forall_lookup_1 _ _ _ _ H Hlk).
+ eapply (Forall_lookup_1 _ _ _ _ Hwf2 Hlk).
+ eauto.
Qed.
Admitted.
End sem.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment