Commit 035064c6 authored by Hai Dang's avatar Hai Dang
Browse files

Add a lemma for to_agreeM

parent b7eaa299
......@@ -169,6 +169,16 @@ Proof.
+ by eapply lookup_weaken_None.
Qed.
Lemma to_agreeM_local_update_insert_singleton m k a :
m !! k = None
(to_agreeM m, ε) ~l~> (to_agreeM (<[k := a]>m), to_agreeM ({[k := a]})).
Proof.
intros. rewrite -insert_empty.
rewrite (_: ε = to_agreeM ); last first.
{ by rewrite /to_agreeM fmap_empty. }
by apply to_agreeM_local_update_insert.
Qed.
Lemma agreeM_local_update_fork (m m' m0 : agreeMR) :
m0 m' m' m m'
(m, m0) ~l~> (m, m').
......
Supports Markdown
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