Commit fda5c51c authored by Ralf Jung's avatar Ralf Jung
Browse files

proof tuning

parent 4e1bdcc7
...@@ -38,7 +38,7 @@ Lemma wp_lift_pure_head_step {E E' Φ} e1 : ...@@ -38,7 +38,7 @@ Lemma wp_lift_pure_head_step {E E' Φ} e1 :
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof using Hinh. Proof using Hinh.
iIntros (??) "H". iApply wp_lift_pure_step; eauto. iIntros (??) "H". iApply wp_lift_pure_step; eauto.
iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro. iMod "H". iModIntro. iNext. iMod "H". iModIntro.
iIntros (????). iApply "H". eauto. iIntros (????). iApply "H". eauto.
Qed. Qed.
......
...@@ -30,11 +30,11 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 : ...@@ -30,11 +30,11 @@ Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
Proof. Proof.
iIntros (Hsafe Hstep) "H". iApply wp_lift_step. iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
{ eapply reducible_not_val, (Hsafe inhabitant). } { eapply reducible_not_val, (Hsafe inhabitant). }
iIntros (σ1) "Hσ". iMod "H" as "H". iIntros (σ1) "Hσ". iMod "H".
iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver. iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?). iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
destruct (Hstep σ1 e2 σ2 efs); auto; subst. destruct (Hstep σ1 e2 σ2 efs); auto; subst.
iMod "Hclose" as "_". iFrame "Hσ". iMod "H" as "H". iApply "H"; auto. iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
Qed. Qed.
(* Atomic steps don't need any mask-changing business here, one can (* Atomic steps don't need any mask-changing business here, one can
...@@ -66,7 +66,7 @@ Proof. ...@@ -66,7 +66,7 @@ Proof.
iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done. iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
{ by intros; eapply Hpuredet. } { by intros; eapply Hpuredet. }
(* TODO: Can we make this nicer? iNext for fupd, for example, could help. *) (* TODO: Can we make this nicer? iNext for fupd, for example, could help. *)
iMod "H" as "H". iModIntro. iNext. iMod "H" as "H". iModIntro. iMod "H". iModIntro. iNext. iMod "H". iModIntro.
by iIntros (e' efs' σ (_&->&->)%Hpuredet). by iIntros (e' efs' σ (_&->&->)%Hpuredet).
Qed. Qed.
End lifting. End lifting.
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