Commit de6dd885 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (`iPoseProof` changes).

parent a20140b8
Pipeline #21423 canceled with stage
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-11-11.0.60647cc2") | (= "dev") }
"coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -36,7 +36,7 @@ Section proof.
{{{ RET #(); bagE γ x ({[v]} X) }}}.
Proof.
iIntros (Φ) "Hbag HΦ".
iApply (pushBag_spec b N (bagE γ x X)%I (bagE γ x ({[v]} X))%I with "[] [Hbag]"); eauto.
iApply (pushBag_spec b N (bagE γ x X)%I (bagE γ x ({[v]} X))%I γ with "[] [Hbag]"); eauto.
{ iAlways. iIntros (Y) "[Hb1 Hb2]".
iDestruct "Hb2" as "[#Hbag Hb2]".
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
......
......@@ -101,7 +101,7 @@ Section hocap_logatom.
Proof.
iIntros "Hstack". iIntros (Φ) "HΦ".
iApply (push_spec with "Hstack").
iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
iApply (make_laterable_intro with "[] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
iMod (stack_content_update with "Hfrag Hauth") as "[Hfrag $]".
......@@ -117,7 +117,7 @@ Section hocap_logatom.
Proof.
iIntros "Hstack". iIntros (Φ) "HΦ".
iApply (pop_spec with "Hstack").
iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
iApply (make_laterable_intro with "[] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
destruct l;
......
......@@ -307,7 +307,6 @@ Section logrel.
destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
* iMod (interp_ref_pointsto_neq with "Hl1 []")
as "[Hl1 %]"; simpl; eauto.
{ by iExists (_, _); iFrame "#". }
by iFrame.
* iMod (interp_ref_pointsto_neq with "Hl1 []")
as "[Hl1 %]"; simpl; eauto.
......@@ -323,7 +322,6 @@ Section logrel.
* destruct (decide (l2 = l3)); destruct (decide (l2' = l3')); subst.
-- iMod (interp_ref_pointsto_neq with "Hl1 []")
as "[Hl1 %]"; simpl; eauto.
{ by iExists (_, _); iFrame "#". }
by iFrame.
-- iMod (interp_ref_pointsto_neq with "Hl1 []")
as "[Hl1 %]"; simpl; eauto.
......@@ -339,8 +337,7 @@ Section logrel.
-- destruct (decide (l1 = l3)); destruct (decide (l1' = l3')); subst.
++ iMod (interp_ref_pointsto_neq with "Hl1 []")
as "[Hl1 %]"; simpl; eauto.
{ by iExists (_, _); iFrame "#". }
by iFrame.
by iFrame.
++ iMod (interp_ref_pointsto_neq with "Hl1 []")
as "[Hl1 %]"; simpl; eauto.
{ by iExists (_, _); iFrame "#". }
......
......@@ -138,14 +138,14 @@ Section types_properties.
Γ !! x = Some A
env_ltyped Γ vs - v, vs !! x = Some v A v.
Proof.
iIntros (HΓx) "HΓ".
iDestruct (big_sepM2_lookup_1 with "HΓ") as (v ?) "H"; eauto.
iIntros (HΓx) "HΓ". rewrite /env_ltyped.
by iApply (big_sepM2_lookup_1 with "HΓ").
Qed.
Lemma env_ltyped_insert Γ vs x A v :
A v - env_ltyped Γ vs -
env_ltyped (binder_insert x A Γ) (binder_insert x v vs).
Proof.
destruct x as [|x]=> /=; first by auto.
destruct x as [|x]=> /=; first by auto. rewrite /env_ltyped.
iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
Qed.
......
......@@ -336,20 +336,14 @@ Section Helpers.
destruct u as [u1 u2]. iApply (par_spec with "[Hx11 K1] [Hx12 K2]").
(* symbolically executing the left part of the par. *)
wp_lam; repeat wp_proj.
assert ((child_to_val u1) = NONEV
( l : loc,
(child_to_val u1) = SOMEV #l l dom (gset _) g)) as Hlf.
iApply ("IH" $! (child_to_val u1) with "[%] K1 Hx11").
{ destruct u1 as [l1|]; [right |by left].
exists l1; split; trivial. eapply (Hgmx l); rewrite // /get_left Hgl; auto. }
iApply ("IH" with "[#] [K1] [Hx11]"); auto.
(* symbolically executing the left part of the par. *)
wp_lam; repeat wp_proj.
assert ((child_to_val u2) = NONEV
( l : loc,
(child_to_val u2) = SOMEV #l l dom (gset _) g)) as Hrh.
iApply ("IH" with "[%] K2 Hx12"); auto.
{ destruct u2 as [l2|]; [right |by left].
exists l2; split; trivial. eapply (Hgmx l); rewrite // /get_right Hgl; auto. }
iApply ("IH" with "[#] [K2] [Hx12]"); auto.
(* continuing after both children are processed *)
iNext.
iIntros (vl vr) "([Hvl K1] & Hvr & K2 & K2')".
......
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