Commit 7f8b110d authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris + remove iAlways uses.

parent 02221014
Pipeline #32666 passed with stage
in 21 minutes and 20 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2020-07-03.0.d44afeed") | (= "dev") }
"coq-iris" { (= "dev.2020-07-21.2.e989ad6b") | (= "dev") }
]
......@@ -41,21 +41,21 @@ Section spec.
iIntros (Φ) "_ HΦ".
wp_lam.
wp_apply (new_channel_spec N Ψ); eauto.
{ iIntros (u); iAlways; iIntros (Φ') "HΨ HΦ'".
{ iIntros (u); iModIntro; iIntros (Φ') "HΨ HΦ'".
wp_lam.
iDestruct "HΨ" as (vs) "Hlist"; eauto.
wp_apply (delete_all_spec Ψ' u _ vs with "[] [Hlist]"); eauto.
{ iIntros (u'); iAlways; iIntros (Φ'') "HΨ' HΦ'".
{ iIntros (u'); iModIntro; iIntros (Φ'') "HΨ' HΦ'".
wp_lam. by iApply "HΦ'". } }
iIntros (px py γ) "[Hex Hey]".
wp_let. wp_proj. wp_let. wp_proj. wp_let.
wp_apply (par_spec (λ _, emp%I) (λ _, emp%I) with "[Hex] [Hey]").
- wp_lam. wp_lam.
wp_apply (mkList_spec Ψ' 5%nat); auto.
{ iAlways; iIntros (m); by iExists _. }
{ iModIntro; iIntros (m); by iExists _. }
iIntros (l1) "Hl1". wp_let.
wp_apply (mkList_spec Ψ' 10%nat); auto.
{ iAlways; iIntros (m); by iExists _. }
{ iModIntro; iIntros (m); by iExists _. }
iIntros (l2) "Hl2". wp_let.
wp_apply (send_x_spec N Ψ γ px l1 with "[Hex Hl1]").
{ iFrame. iExists (mkList_ref 5); eauto. }
......@@ -68,7 +68,7 @@ Section spec.
wp_apply (close_x_spec with "Hex"); eauto.
- do 2 wp_let.
wp_apply (mkList_spec Ψ' 5%nat); auto.
{ iAlways; iIntros (m); by iExists _. }
{ iModIntro; iIntros (m); by iExists _. }
iIntros (l3) "Hl3". wp_let.
wp_apply (send_y_spec N Ψ γ py l3 with "[Hey Hl3]").
......@@ -79,7 +79,7 @@ Section spec.
wp_let.
iDestruct "HΨ'" as (vs) "Hlist".
wp_apply (delete_all_spec Ψ' x _ vs with "[] [Hlist]"); eauto.
{ iIntros (u'); iAlways; iIntros (Φ'') "HΨ' HΦ'".
{ iIntros (u'); iModIntro; iIntros (Φ'') "HΨ' HΦ'".
wp_lam. by iApply "HΦ'". }
iIntros (v) "_". wp_let.
wp_apply (close_y_spec with "Hey"). by iIntros "_ /=".
......
......@@ -249,10 +249,11 @@ Global Instance into_wand_impl'_fracPred p q P Q PP QQ π :
IntoWand' p q ((P → Q) π) PP QQ → IntoWand p q ((P → Q) π) PP QQ | 100.
Proof. done. Qed. *)
(* [π] is the default name for the fraction *)
Global Instance from_forall_fracPred_at_wand R P Q Φ Ψ π :
FromWand R P Q
( π', MakeFracPredAt π' P (Φ π')) ( π', MakeFracPredAt π' Q (Ψ π'))
FromForall (R π) (λ π', Φ π' - Ψ (π π'))%I.
FromForall (R π) (λ π', Φ π' - Ψ (π π'))%I (to_ident_name π).
Proof.
rewrite /FromWand /FromForall /MakeFracPredAt=> <- H1 H2.
rewrite fracPred_at_wand. do 2 f_equiv. by rewrite H1 H2.
......@@ -310,8 +311,9 @@ Proof.
by rewrite fracPred_at_exist.
Qed. *)
Global Instance from_forall_fracPred_at {A} P (Φ : A fracPred) (Ψ : A PROP) π :
FromForall P Φ ( a, MakeFracPredAt π (Φ a) (Ψ a)) FromForall (P π) Ψ.
Global Instance from_forall_fracPred_at {A} P (Φ : A fracPred) (Ψ : A PROP) π name :
FromForall P Φ name ( a, MakeFracPredAt π (Φ a) (Ψ a))
FromForall (P π) Ψ name.
Proof.
rewrite /FromForall /MakeFracPredAt=><- H. setoid_rewrite <- H.
by rewrite fracPred_at_forall.
......
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