From fda4b19f14c48d6f19e6593c08c80992eee33d6e Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 26 Feb 2024 16:11:02 +0100
Subject: [PATCH] Move FrameNoInstantiateExist class.
---
iris/program_logic/weakestpre.v | 3 +--
iris/proofmode/class_instances_frame.v | 5 -----
iris/proofmode/classes.v | 7 +++++++
3 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index db9aaa228..81f316f5d 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -425,8 +425,7 @@ Section proofmode_classes.
Implicit Types e : expr Λ.
Global Instance frame_wp p s E e R Φ Ψ :
- (class_instances_frame.FrameNoInstantiateExist →
- ∀ v, Frame p R (Φ v) (Ψ v)) →
+ (FrameNoInstantiateExist → ∀ v, Frame p R (Φ v) (Ψ v)) →
Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}) | 2.
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR, I. Qed.
diff --git a/iris/proofmode/class_instances_frame.v b/iris/proofmode/class_instances_frame.v
index d6e5ca382..37fd6bb10 100644
--- a/iris/proofmode/class_instances_frame.v
+++ b/iris/proofmode/class_instances_frame.v
@@ -196,11 +196,6 @@ Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
Proof. rewrite /Frame /MakeOr => [[<-]] [<-] _ <-. by rewrite -sep_or_l. Qed.
-(* We want a way to disable instantiating quantifiers when we are
-framing beneath connectives like [∀], [-∗] and [→]. See iris#565. *)
-Class FrameNoInstantiateExist : Prop := frame_no_instantiate_exist : True.
-Notation FrameCanInstantiateExist := (TCUnless FrameNoInstantiateExist).
-
Global Instance frame_wand p R P1 P2 Q2 :
(FrameNoInstantiateExist → Frame p R P2 Q2) →
Frame p R (P1 -∗ P2) (P1 -∗ Q2) | 2.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index d9e4f7a88..ad8818bb7 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -397,6 +397,13 @@ For more details, see also iris!989 and the [frame_and] and [frame_or_spatial]
instances in [class_instances_frame.v] *)
Notation MaybeFrame p R P Q progress := (TCNoBackTrack (MaybeFrame' p R P Q progress)).
+(* The [iFrame] tactic is able to instantiate witnesses for existential
+quantifiers. We need a way to disable this behavior beneath connectives
+like [∀], [-∗] and [→], since it is often unwanted in these cases.
+Also see iris#565. *)
+Class FrameNoInstantiateExist : Prop := frame_no_instantiate_exist : True.
+Notation FrameCanInstantiateExist := (TCUnless FrameNoInstantiateExist).
+
Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
Global Arguments into_except_0 {_} _%I _%I {_}.
--
GitLab