From e5c51505a1e8f1943d0b9d029d6ddb62df63fe4e Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Thu, 15 Sep 2016 22:26:04 +0200 Subject: [PATCH] Make iFrame able to strip a later from a framed hypothesis when framing under a later. --- algebra/upred.v | 1 + proofmode/class_instances.v | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/algebra/upred.v b/algebra/upred.v index b4b5abe28..18e438efb 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -1472,6 +1472,7 @@ Qed. Theorem soundness : ¬ (True ⊢ False). Proof. exact (adequacy False 0). Qed. + End uPred_logic. (* Hint DB for the logic *) diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v index 68ce0feef..3e0504e93 100644 --- a/proofmode/class_instances.v +++ b/proofmode/class_instances.v @@ -269,10 +269,10 @@ Proof. by rewrite /MakeLater later_True. Qed. Global Instance make_later_default P : MakeLater P (▷ P) | 100. Proof. done. Qed. -Global Instance frame_later R P Q Q' : - Frame R P Q → MakeLater Q Q' → Frame R (▷ P) Q'. +Global Instance frame_later R R' P Q Q' : + Frame R P Q → MakeLater Q Q' → IntoLater R' R → Frame R' (▷ P) Q'. Proof. - rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R). + rewrite /Frame /MakeLater /IntoLater=><- <- ->. by rewrite later_sep. Qed. Class MakeExceptLast (P Q : uPred M) := make_except_last : ◇ P ⊣⊢ Q. -- GitLab