Commit 4417beb8 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Partly revert a9880321 and 9ae19ed5.

Also, higher cost for [elim_modal_bupd_fupd], so that it is not taken in place of [elim_modal_fupd_fupd] in spec patterns.
parent a9880321
Pipeline #3189 passed with stage
in 10 minutes and 40 seconds
...@@ -176,12 +176,12 @@ Section proofmode_classes. ...@@ -176,12 +176,12 @@ Section proofmode_classes.
Proof. rewrite /IntoModal. apply fupd_intro. Qed. Proof. rewrite /IntoModal. apply fupd_intro. Qed.
Global Instance elim_modal_bupd_fupd E1 E2 P Q : Global Instance elim_modal_bupd_fupd E1 E2 P Q :
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q). ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Proof. Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans. by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed. Qed.
Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q : Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 10. ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed. Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes. End proofmode_classes.
...@@ -221,12 +221,4 @@ Proof. ...@@ -221,12 +221,4 @@ Proof.
iMod (fupd_intro_mask') as "HM2"; first done. iModIntro. iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
iNext. iMod "HM2". iMod "HP". iMod "HM1". done. iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
Qed. Qed.
Global Instance elim_modal_step_fupd E1 E2 E3 E4 P Q :
ElimModal (|={E1,E2}=>|={E2,E3}=> P) P
(|={E1,E2}=>|={E2,E4}=> Q) (|={E3,E4}=> Q).
Proof.
iIntros "[A B]". iMod "A". iModIntro. iNext. iMod "A". by iApply "B".
Qed.
End step_fupd. End step_fupd.
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