Skip to content
Snippets Groups Projects
Commit d7934c50 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Proof mode instances for eliminating plain basic updates.

parent 4ac0be9f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/class_instances.v
+ 6
− 0
View file @ d7934c50
...@@ -815,6 +815,12 @@ Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. Qed. ...@@ -815,6 +815,12 @@ Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. Qed.
Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q). Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed. Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q. Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
Proof. Proof.
intros. rewrite /ElimModal (except_0_intro (_ -∗ _)). intros. rewrite /ElimModal (except_0_intro (_ -∗ _)).
......
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