Commit 23ae69a1 authored by Dan Frumin's avatar Dan Frumin

Get rid of the final admit

parent 1dd902a7
......@@ -8,5 +8,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris-c-monad"]
depends: [
"coq-iris" { (= "dev.2018-11-01.3.19aae59a") | (= "dev") }
"coq-iris" { (= "dev.2018-11-06.0.c6e8c5d5") | (= "dev") }
]
......@@ -767,12 +767,9 @@ Section flock.
snd <$> f <$> I ≼ snd <$> g <$> fp
= to_agree o res_name <$> I ≼ to_agree <$> fp *)
assert (((snd <$> (f <$> I)) : gmapUR prop_id (agreeR lock_res_nameC)) (snd <$> (g <$> fp))) as Hbar.
{ (* TODO DOESN"T WORK SAD *)
(* Check (gmap_fmap_mono snd (f <$> I) (g <$> fp)). *)
admit.
(* eapply cmra_morphism_monotone; last exact: Hfoo. *)
(* apply gmap_fmap_cmra_morphism. apply _. *)
}
{ apply gmap_fmap_mono; eauto.
- move=> [? ?] [? ?] [? ?] //.
- intros [? ?] [? ?] [? ?]%prod_included. done. }
rewrite -!map_fmap_compose in Hbar.
assert ((to_agree res_name <$> I) to_agree <$> fp) as Hbaz by exact: Hbar.
rewrite map_fmap_compose in Hbaz.
......@@ -834,7 +831,7 @@ Section flock.
iFrame. iSplit; eauto.
rewrite big_sepM_fmap.
iApply (big_sepM_own_frag with "Hemp HI").
Admitted.
Qed.
Lemma release_cancel_spec' γ lk I :
{{{ is_flock γ lk flocked γ I }}}
......
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