Skip to content
Snippets Groups Projects
Commit 74248723 authored by Hai Dang's avatar Hai Dang
Browse files

bump gpfsl

parent 830f7de9
Branches
No related tags found
No related merge requests found
Pipeline #15030 passed
...@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"] ...@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [ depends: [
"coq-gpfsl" { (= "dev.2019-02-15.1.400540d7") | (= "dev") } "coq-gpfsl" { (= "dev.2019-02-21.1.cabd1b87") | (= "dev") }
] ]
...@@ -108,7 +108,7 @@ Lemma exists_Vs A (K : gset lft) : ...@@ -108,7 +108,7 @@ Lemma exists_Vs A (K : gset lft) :
([ set] κ K, lft_inv_alive κ (Vs κ) lft_alive_in A κ ([ set] κ K, lft_inv_alive κ (Vs κ) lft_alive_in A κ
lft_inv_dead κ (Vs κ) lft_dead_in A κ). lft_inv_dead κ (Vs κ) lft_dead_in A κ).
Proof. Proof.
induction (collection_wf K) as [K _ IH]. iIntros "HK". induction (set_wf K) as [K _ IH]. iIntros "HK".
destruct (decide (K = )) as [->|]. destruct (decide (K = )) as [->|].
{ iExists (λ _, inhabitant). repeat (iSplit; [by auto|]). by rewrite !big_sepS_empty. } { iExists (λ _, inhabitant). repeat (iSplit; [by auto|]). by rewrite !big_sepS_empty. }
destruct (minimal_exists_L () K) as (κ & HκK & Hκmin); first done. destruct (minimal_exists_L () K) as (κ & HκK & Hκmin); first done.
......
...@@ -46,13 +46,13 @@ Proof. ...@@ -46,13 +46,13 @@ Proof.
iSplitR; [iApply box_alloc|]. rewrite /own_bor. iExists γs. by iFrame. } iSplitR; [iApply box_alloc|]. rewrite /own_bor. iExists γs. by iFrame. }
iSplitR "Hinh"; last by iApply "Hinh". iSplitR "Hinh"; last by iApply "Hinh".
rewrite lft_vs_unfold. iExists bot, 0. iSplit=>//. iFrame "Hcnt Hcnt'". auto. } rewrite lft_vs_unfold. iExists bot, 0. iSplit=>//. iFrame "Hcnt Hcnt'". auto. }
set (A' := union_with (λ x _, Some x) A (to_gmap (false, bot) (dom _ κ))). set (A' := union_with (λ x _, Some x) A (gset_to_gmap (false, bot) (dom _ κ))).
iMod (own_update _ _ ( to_alftUR A' _) with "HA") as "[HA _]". iMod (own_update _ _ ( to_alftUR A' _) with "HA") as "[HA _]".
{ apply auth_update_alloc. { apply auth_update_alloc.
assert (to_alftUR A' assert (to_alftUR A'
to_gmap (Cinr (to_agree $ to_latT bot)) (dom _ κ dom _ A) to_alftUR A) as ->. gset_to_gmap (Cinr (to_agree $ to_latT bot)) (dom _ κ dom _ A) to_alftUR A) as ->.
{ intros Λ. rewrite lookup_op lookup_to_gmap !lookup_fmap lookup_union_with { intros Λ. rewrite lookup_op lookup_gset_to_gmap !lookup_fmap lookup_union_with
lookup_to_gmap. lookup_gset_to_gmap.
destruct (A !! Λ) eqn:EQ. destruct (A !! Λ) eqn:EQ.
- apply (elem_of_dom_2 (D:=gset atomic_lft)) in EQ. - apply (elem_of_dom_2 (D:=gset atomic_lft)) in EQ.
rewrite [X in _ X _]option_guard_False; last set_solver. by destruct mguard. rewrite [X in _ X _]option_guard_False; last set_solver. by destruct mguard.
...@@ -61,7 +61,7 @@ Proof. ...@@ -61,7 +61,7 @@ Proof.
+ rewrite !option_guard_True; set_solver. + rewrite !option_guard_True; set_solver.
+ rewrite !option_guard_False; set_solver. } + rewrite !option_guard_False; set_solver. }
eapply op_local_update_discrete=>HA Λ. specialize (HA Λ). eapply op_local_update_discrete=>HA Λ. specialize (HA Λ).
rewrite lookup_op lookup_to_gmap !lookup_fmap. rewrite lookup_op lookup_gset_to_gmap !lookup_fmap.
destruct (A !! Λ) eqn:EQ. destruct (A !! Λ) eqn:EQ.
- apply (elem_of_dom_2 (D:=gset atomic_lft)) in EQ. - apply (elem_of_dom_2 (D:=gset atomic_lft)) in EQ.
rewrite option_guard_False; [by destruct p as [[]?]|set_solver]. rewrite option_guard_False; [by destruct p as [[]?]|set_solver].
...@@ -74,25 +74,25 @@ Proof. ...@@ -74,25 +74,25 @@ Proof.
rewrite /own_ilft_auth /to_ilftUR fmap_insert dom_insert_L. iFrame "HI". rewrite /own_ilft_auth /to_ilftUR fmap_insert dom_insert_L. iFrame "HI".
iNext. iApply @big_sepS_insert; first by apply not_elem_of_dom. iSplitR "Hinv". iNext. iApply @big_sepS_insert; first by apply not_elem_of_dom. iSplitR "Hinv".
- destruct (lft_alive_or_dead_in A' κ) as [(Λ&?&HAΛ)|Haliveordead]. - destruct (lft_alive_or_dead_in A' κ) as [(Λ&?&HAΛ)|Haliveordead].
+ rewrite lookup_union_with lookup_to_gmap option_guard_True in HAΛ; + rewrite lookup_union_with lookup_gset_to_gmap option_guard_True in HAΛ;
[by destruct (A!!Λ)|by apply gmultiset_elem_of_dom]. [by destruct (A!!Λ)|by apply gmultiset_elem_of_dom].
+ unfold lft_inv. iExists bot. iSplit; last first. + unfold lft_inv. iExists bot. iSplit; last first.
{ destruct Haliveordead. { destruct Haliveordead.
* iLeft. by iDestruct "Hdeadandalive" as "[_ $]". * iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
* iRight. by iDestruct "Hdeadandalive" as "[$ _]". } * iRight. by iDestruct "Hdeadandalive" as "[$ _]". }
iPureIntro=>Λ?. rewrite lookup_union_with lookup_to_gmap option_guard_True; iPureIntro=>Λ?. rewrite lookup_union_with lookup_gset_to_gmap option_guard_True;
[|by apply gmultiset_elem_of_dom]. destruct (A!!Λ); apply lat_bottom_sqsubseteq. [|by apply gmultiset_elem_of_dom]. destruct (A!!Λ); apply lat_bottom_sqsubseteq.
- iApply (@big_sepS_impl with "[$Hinv]"). iIntros "!# * _ H". unfold lft_inv. - iApply (@big_sepS_impl with "[$Hinv]"). iIntros "!# * _ H". unfold lft_inv.
iDestruct "H" as () "[HV Hinv]". iExists . iSplit. iDestruct "H" as () "[HV Hinv]". iExists . iSplit.
+ iDestruct "HV" as %HV. iPureIntro. intros Λ . specialize (HV Λ ). + iDestruct "HV" as %HV. iPureIntro. intros Λ . specialize (HV Λ ).
rewrite lookup_union_with. by destruct (A !! Λ), (to_gmap _ _ !! Λ). rewrite lookup_union_with. by destruct (A !! Λ), (gset_to_gmap _ _ !! Λ).
+ iDestruct "Hinv" as "[[Hinv Hin]|[Hinv Hin]]". + iDestruct "Hinv" as "[[Hinv Hin]|[Hinv Hin]]".
* iLeft. iFrame. iDestruct "Hin" as %Hin. iPureIntro. * iLeft. iFrame. iDestruct "Hin" as %Hin. iPureIntro.
intros Λ . specialize (Hin Λ ). rewrite lookup_union_with. intros Λ . specialize (Hin Λ ). rewrite lookup_union_with.
by destruct (A !! Λ), (to_gmap _ _ !! Λ). by destruct (A !! Λ), (gset_to_gmap _ _ !! Λ).
* iRight. iFrame. iDestruct "Hin" as %(Λ & & HA). iPureIntro. * iRight. iFrame. iDestruct "Hin" as %(Λ & & HA). iPureIntro.
exists Λ. split; first done. rewrite lookup_union_with. exists Λ. split; first done. rewrite lookup_union_with.
by destruct (A !! Λ), (to_gmap _ _ !! Λ). by destruct (A !! Λ), (gset_to_gmap _ _ !! Λ).
Qed. Qed.
Lemma raw_bor_fake E κ P : Lemma raw_bor_fake E κ P :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment