From fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 4 Apr 2020 10:47:47 +0200
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/lang/heap.v | 6 +++---
theories/lifetime/model/accessors.v | 4 ++--
theories/lifetime/model/creation.v | 2 +-
theories/lifetime/model/primitive.v | 6 +++---
5 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/opam b/opam
index a7596e47..aa6cda0d 100644
--- a/opam
+++ b/opam
@@ -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}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 4abef3c1..2cc7ebc3 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -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''.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 7a17291d..82e47fa9 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -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.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 5e3902e6..622f63e9 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -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 ())). }
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index b4f16f1c..56fc8a6f 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -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.
--
GitLab