Commit 02221014 authored by Ralf Jung's avatar Ralf Jung

update dependencies, fix for step_fupd notation change

parent 7820a415
Pipeline #31799 failed with stage
in 19 minutes and 2 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-06-11.0.11f9d567") | (= "dev") }
"coq-iris" { (= "dev.2020-07-03.0.d44afeed") | (= "dev") }
]
......@@ -63,7 +63,7 @@ Qed.
Lemma iron_wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
(|={E,E'}=>^n WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}.
(|={E}[E']=>^n WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}.
Proof.
rewrite iron_wp_eq /=. iStartProof (iProp _). iIntros (Hstep ? π1) "H".
iIntros (π2) "Hp". iApply (wp_pure_step_fupd _ _ E'); first done.
......
......@@ -97,7 +97,7 @@ Qed.
Lemma iron_wp_step_fupd s E1 E2 e P Φ :
TCEq (to_val e) None E2 E1
(|={E1,E2}=> P) - WP e @ s; E2 {{ v, P ={E1}= Φ v }} - WP e @ s; 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'] /=".
......@@ -172,14 +172,14 @@ Proof. iIntros "[H ?]". iApply (iron_wp_strong_mono with "H"); auto with iFrame.
Lemma iron_wp_frame_step_l s E1 E2 e Φ R :
TCEq (to_val e) None E2 E1
(|={E1,E2}=> R) WP e @ s; E2 {{ Φ }} WP e @ s; E1 {{ v, R Φ v }}.
(|={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 :
TCEq (to_val e) None E2 E1
WP e @ s; E2 {{ Φ }} (|={E1,E2}=> R) WP e @ s; E1 {{ v, Φ v R }}.
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.
......
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