Commit fe35f4cd authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 397cb2b3
Pipeline #26247 passed with stage
in 29 minutes and 54 seconds
......@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
"coq-iris" { (= "dev.2020-04-02.2.df3450a6") | (= "dev") }
"coq-iris" { (= "dev.2020-04-04.3.9b2ad256") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -407,7 +407,7 @@ Section heap.
iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_both_valid.
move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
move: Hl=> /singleton_included_l [[q qs] [/leibniz_equiv_iff Hl Hq]].
apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
{ move: (Hv (l.1)). rewrite Hl. by intros [??]. }
assert (vl []).
......@@ -430,7 +430,7 @@ Section heap.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
move=> /Some_pair_included_total_2
......@@ -447,7 +447,7 @@ Section heap.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid.
iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
......
......@@ -100,7 +100,7 @@ Proof.
iLeft. iFrame "%". iExists _, _. iFrame.
+ iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hf")
as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
......@@ -204,7 +204,7 @@ Proof.
iExists Q. rewrite -bi.iff_refl. eauto.
+ iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
iDestruct (own_bor_valid_2 with "Hinv Hbor")
as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_both_valid.
as %[(_ & <- & INCL%option_included)%singleton_included_l _]%auth_both_valid.
by destruct INCL as [[=]|(? & ? & [=<-] &
[[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
......
......@@ -132,7 +132,7 @@ Proof.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
rewrite /lft_tok big_sepMS_singleton.
iDestruct (own_valid_2 with "HA HΛ")
as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_both_valid.
as %[[s [?%leibniz_equiv ?]]%singleton_included_l _]%auth_both_valid.
iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
{ by eapply auth_update, singleton_local_update,
(exclusive_local_update _ (Cinr ())). }
......
......@@ -13,7 +13,7 @@ Implicit Types κ : lft.
Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
{[i := (q%Qp, to_agree s)]} to_borUR B B !! i = Some s.
Proof.
rewrite singleton_included=> -[qs []]. unfold_leibniz.
rewrite singleton_included_l=> -[qs []]. unfold_leibniz.
rewrite lookup_fmap fmap_Some_equiv=> -[s' [-> ->]].
by move=> /Some_pair_included [_] /Some_included_total /to_agree_included=>->.
Qed.
......@@ -37,7 +37,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
own ilft_name ( {[κ := to_agree γs]}) - is_Some (I !! κ).
Proof.
iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
as %[[? [Hl ?]]%singleton_included _]%auth_both_valid.
as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid.
unfold to_ilftUR in *. simplify_map_eq.
destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
Qed.
......@@ -48,7 +48,7 @@ Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
Proof.
iIntros "HA HΛ".
iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_both_valid.
iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
iPureIntro. move: HA=> /singleton_included_l [qs [/leibniz_equiv_iff]].
rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
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