Commit cd9c189a authored by Dan Frumin's avatar Dan Frumin

Get rid of two admits

parent c5ec5ddf
...@@ -296,9 +296,13 @@ Section flock. ...@@ -296,9 +296,13 @@ Section flock.
{ remember (fa !! i) as fai. destruct fai as [[π ρ']|]; last done. { remember (fa !! i) as fai. destruct fai as [[π ρ']|]; last done.
symmetry in Heqfai. symmetry in Heqfai.
rewrite (big_sepM_lookup _ fa i (π, ρ')) //. rewrite (big_sepM_lookup _ fa i (π, ρ')) //.
(* TODO: RK, please look at this! *)
iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz. iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz.
exfalso. revert Hbaz. rewrite -auth_frag_op /=. exfalso. revert Hbaz.
admit. } rewrite -auth_frag_op /=. intros Hbaz%auth_own_valid.
revert Hbaz. simpl. rewrite op_singleton pair_op /=.
rewrite singleton_valid. intros [Hlol _]. simpl in *.
eapply exclusive_l ; eauto. apply _. }
assert (fp !! i = Some ρ) as Hbaz. assert (fp !! i = Some ρ) as Hbaz.
{ apply lookup_union_Some in Hfoo; last done. { apply lookup_union_Some in Hfoo; last done.
destruct Hfoo as [? | Hfoo]; first done. destruct Hfoo as [? | Hfoo]; first done.
...@@ -347,7 +351,7 @@ Section flock. ...@@ -347,7 +351,7 @@ Section flock.
+ iPureIntro. by apply map_disjoint_delete_l. + iPureIntro. by apply map_disjoint_delete_l.
+ rewrite /from_active fmap_empty /= right_id. + rewrite /from_active fmap_empty /= right_id.
by rewrite to_props_map_delete. by rewrite to_props_map_delete.
Admitted. Qed.
Lemma newflock_spec : Lemma newflock_spec :
{{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}. {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
...@@ -417,7 +421,11 @@ Section flock. ...@@ -417,7 +421,11 @@ Section flock.
iMod ("Hcl" with "[Haactive Hi Hlocked Haprops Htokens Hstate]") as "_". iMod ("Hcl" with "[Haactive Hi Hlocked Haprops Htokens Hstate]") as "_".
{ iNext. iExists Locked,{[i := (π, ρ)]},(delete i fp). { iNext. iExists Locked,{[i := (π, ρ)]},(delete i fp).
iFrame. iSplitR ; [ | iSplitL "Haprops"]. iFrame. iSplitR ; [ | iSplitL "Haprops"].
- admit. - iPureIntro.
rewrite /from_active map_fmap_singleton /=.
(* TODO: RK, please look at this *)
admit.
- rewrite /from_active map_fmap_singleton /=. - rewrite /from_active map_fmap_singleton /=.
rewrite -insert_union_singleton_r. rewrite -insert_union_singleton_r.
2: { apply lookup_delete. } 2: { apply lookup_delete. }
...@@ -494,7 +502,10 @@ Section flock. ...@@ -494,7 +502,10 @@ Section flock.
apply map_disjoint_empty_r. apply map_disjoint_empty_r.
- iFrame. rewrite /from_active fmap_empty right_id /=. - iFrame. rewrite /from_active fmap_empty right_id /=.
rewrite map_fmap_singleton. rewrite map_fmap_singleton.
assert (fp !! i = None). admit. (* follows from ##ₘ *) assert (fp !! i = None).
{ eapply map_disjoint_Some_r; first eassumption.
rewrite /from_active !map_fmap_singleton.
by rewrite lookup_singleton. }
rewrite -insert_union_singleton_r // /=. iFrame. rewrite -insert_union_singleton_r // /=. iFrame.
rewrite /all_tokens big_sepM_insert //. rewrite /all_tokens big_sepM_insert //.
iFrame. iFrame.
...@@ -502,7 +513,7 @@ Section flock. ...@@ -502,7 +513,7 @@ Section flock.
iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]"). iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
iModIntro. iNext. iIntros "_". iApply "HΦ". iModIntro. iNext. iIntros "_". iApply "HΦ".
by iFrame. by iFrame.
Admitted. Qed.
(** LULZ *) (** LULZ *)
......
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