From 4793ab79c824dd8eeef2de7e5229191ab8116721 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 2 Feb 2018 11:54:50 +0100 Subject: [PATCH] Support framing under implications. We already supported framing under wands. --- theories/proofmode/class_instances.v | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v index 214b3dc3b..df0bcffb5 100644 --- a/theories/proofmode/class_instances.v +++ b/theories/proofmode/class_instances.v @@ -615,6 +615,20 @@ Proof. by rewrite assoc (comm _ P1) -assoc wand_elim_r. Qed. +Global Instance frame_impl_persistent R P1 P2 Q2 : + Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2). +Proof. + rewrite /Frame /==> ?. apply impl_intro_l. + by rewrite -and_sep_l assoc (comm _ P1) -assoc impl_elim_r and_sep_l. +Qed. +Global Instance frame_impl R P1 P2 Q2 : + Persistent P1 → + Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2). +Proof. + rewrite /Frame /==> ??. apply impl_intro_l. + by rewrite and_sep_l assoc (comm _ P1) -assoc -(and_sep_l P1) impl_elim_r. +Qed. + Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP. Global Instance make_later_true : MakeLater True True. Proof. by rewrite /MakeLater later_True. Qed. -- GitLab