Commit ee50bc2e authored by Dan Frumin's avatar Dan Frumin

Fix monad.v

parent 69a792f0
......@@ -73,7 +73,7 @@ Section a_wp.
iIntros (w) "[Hwp Hunfl]". wp_let. by iApply "Hwp".
Qed.
Lemma awp_run (v : val) R Φ :
Lemma awp_run (v : val) R Φ `{Timeless _ R} :
R - awp v R (λ w, R - Φ w) -
WP a_run v {{ Φ }}.
Proof.
......@@ -82,14 +82,14 @@ Section a_wp.
iApply set_newset_spec. done.
iNext. iIntros (v0) "%".
wp_alloc env as "H". wp_let.
wp_apply (newlock_cancel_spec (env_inv #env R)%I with "[H HR]").
wp_apply (newlock_cancel_spec amonadN (env_inv #env R)%I with "[H HR]").
iFrame. iExists . iExists env, v0. iFrame. done.
iIntros (k γ') "Hlock". wp_let. rewrite- wp_fupd.
iApply (wp_wand with "[Hwp Hlock]").
unfold awp. iApply ("Hwp" with "Hlock").
iIntros (w) "[HΦ Hlock]".
iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
iApply (wp_wand with "[Hwp Hunfl]").
unfold awp. by iApply ("Hwp" with "Hlock").
iIntros (w) "[HΦ Hunfl]".
iApply "HΦ".
iMod (cancel_lock with "Hlock") as "[HEnv HR]". done.
iMod (cancel_lock with "Hlock Hunfl") as "[HEnv HR]". done.
Qed.
......
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