Commit d9a60dbe authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (TCEq change in WP step rules).

parent 35f41dcb
Pipeline #25046 passed with stage
in 19 minutes and 29 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-02-14.2.a3cea59c") | (= "dev") }
"coq-iris" { (= "dev.2020-02-26.0.a0e0e916") | (= "dev") }
]
......@@ -96,12 +96,12 @@ Proof.
Qed.
Lemma iron_wp_step_fupd s E1 E2 e P Φ :
to_val e = None E2 E1
TCEq (to_val e) None E2 E1
(|={E1,E2}=> P) - WP e @ s; E2 {{ v, P ={E1}= Φ v }} - WP e @ s; E1 {{ Φ }}.
Proof.
rewrite iron_wp_eq. iStartProof (iProp _); iIntros (?? π1) "HP".
iIntros (π2) "H"; iIntros (π3) "[Hp Hp'] /=".
iApply (wp_step_fupd with "[HP Hp]"); [done|done| | ].
iApply (wp_step_fupd with "[HP Hp]"); [done| | ].
- iMod ("HP" with "Hp") as (π4 π5 Hπ) "[Hp H]". iIntros "!> !>".
iSpecialize ("H" with "Hp"). rewrite <-Hπ. iApply "H".
- iSpecialize ("H" with "Hp'"). iApply (wp_wand with "H"); iIntros (v).
......@@ -171,24 +171,24 @@ Lemma iron_wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{
Proof. iIntros "[H ?]". iApply (iron_wp_strong_mono with "H"); auto with iFrame. Qed.
Lemma iron_wp_frame_step_l s E1 E2 e Φ R :
to_val e = None E2 E1
TCEq (to_val e) None E2 E1
(|={E1,E2}=> R) WP e @ s; E2 {{ Φ }} WP e @ s; E1 {{ v, R Φ v }}.
Proof.
iIntros (??) "[Hu Hwp]". iApply (iron_wp_step_fupd with "Hu"); try done.
iApply (iron_wp_mono with "Hwp"). by iIntros (?) "$$ !>".
Qed.
Lemma iron_wp_frame_step_r s E1 E2 e Φ R :
to_val e = None E2 E1
TCEq (to_val e) None E2 E1
WP e @ s; E2 {{ Φ }} (|={E1,E2}=> R) WP e @ s; E1 {{ v, Φ v R }}.
Proof.
rewrite [(WP _ @ _; _ {{ _ }} _)%I]comm; setoid_rewrite (comm _ _ R).
apply iron_wp_frame_step_l.
Qed.
Lemma iron_wp_frame_step_l' s E e Φ R :
to_val e = None R WP e @ s; E {{ Φ }} WP e @ s; E {{ v, R Φ v }}.
TCEq (to_val e) None R WP e @ s; E {{ Φ }} WP e @ s; E {{ v, R Φ v }}.
Proof. iIntros (?) "[??]". iApply (iron_wp_frame_step_l s E E); try iFrame; eauto. Qed.
Lemma iron_wp_frame_step_r' s E e Φ R :
to_val e = None WP e @ s; E {{ Φ }} R WP e @ s; E {{ v, Φ v R }}.
TCEq (to_val e) None WP e @ s; E {{ Φ }} R WP e @ s; E {{ v, Φ v R }}.
Proof. iIntros (?) "[??]". iApply (iron_wp_frame_step_r s E E); try iFrame; eauto. Qed.
Lemma iron_wp_wand s E e Φ Ψ :
......
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