From 2cfaecf6dab2e05bcf4644df9e03abec8033de05 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 3 Mar 2018 19:57:27 +0100
Subject: [PATCH] Get rid of KnownFrame and iFrame automatically instantiating
evars.
---
theories/program_logic/total_weakestpre.v | 4 +-
theories/program_logic/weakestpre.v | 4 +-
theories/proofmode/class_instances.v | 135 ++++++++++------------
theories/proofmode/classes.v | 14 +--
theories/proofmode/monpred.v | 8 +-
theories/tests/proofmode.v | 10 +-
6 files changed, 77 insertions(+), 98 deletions(-)
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index b188a5b34..6afeb5a3b 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -378,8 +378,8 @@ Section proofmode_classes.
Global Instance frame_twp p s E e R Φ Ψ :
(∀ v, Frame p R (Φ v) (Ψ v)) →
- KnownFrame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
- Proof. rewrite /KnownFrame /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
+ Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
+ Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
Proof. by rewrite /IsExcept0 -{2}fupd_twp -except_0_fupd -fupd_intro. Qed.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index a9cb74349..4564bb371 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -372,8 +372,8 @@ Section proofmode_classes.
Global Instance frame_wp p s E e R Φ Ψ :
(∀ v, Frame p R (Φ v) (Ψ v)) →
- KnownFrame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
- Proof. rewrite /KnownFrame /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
+ Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
+ Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f1fe44239..81beeec8d 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -716,25 +716,25 @@ Proof.
Qed.
(* Frame *)
-Global Instance frame_here_absorbing p R : Absorbing R → KnownFrame p R R True | 0.
-Proof. intros. by rewrite /KnownFrame /Frame affinely_persistently_if_elim sep_elim_l. Qed.
-Global Instance frame_here p R : KnownFrame p R R emp | 1.
-Proof. intros. by rewrite /KnownFrame /Frame affinely_persistently_if_elim sep_elim_l. Qed.
+Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
+Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
+Global Instance frame_here p R : Frame p R R emp | 1.
+Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
Global Instance frame_affinely_here_absorbing p R :
- Absorbing R → KnownFrame p (bi_affinely R) R True | 0.
+ Absorbing R → Frame p (bi_affinely R) R True | 0.
Proof.
- intros. rewrite /KnownFrame /Frame affinely_persistently_if_elim affinely_elim.
+ intros. rewrite /Frame affinely_persistently_if_elim affinely_elim.
apply sep_elim_l, _.
Qed.
-Global Instance frame_affinely_here p R : KnownFrame p (bi_affinely R) R emp | 1.
+Global Instance frame_affinely_here p R : Frame p (bi_affinely R) R emp | 1.
Proof.
- intros. rewrite /KnownFrame /Frame affinely_persistently_if_elim affinely_elim.
+ intros. rewrite /Frame affinely_persistently_if_elim affinely_elim.
apply sep_elim_l, _.
Qed.
-Global Instance frame_here_pure p φ Q : FromPure false Q φ → KnownFrame p ⌜φ⌠Q True.
+Global Instance frame_here_pure p φ Q : FromPure false Q φ → Frame p ⌜φ⌠Q True.
Proof.
- rewrite /FromPure /KnownFrame /Frame=> <-.
+ rewrite /FromPure /Frame=> <-.
by rewrite affinely_persistently_if_elim sep_elim_l.
Qed.
@@ -749,16 +749,14 @@ Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
Proof. by rewrite /MakeEmbed. Qed.
Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
- Frame p R P Q → MakeEmbed Q Q' → KnownFrame p ⎡R⎤ ⎡P⎤ Q'.
+ Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
Proof.
- rewrite /KnownFrame /Frame /MakeEmbed => <- <-.
+ rewrite /Frame /MakeEmbed => <- <-.
rewrite embed_sep embed_affinely_if embed_persistently_if => //.
Qed.
Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
- Frame p ⌜φ⌠P Q → MakeEmbed Q Q' → KnownFrame p ⌜φ⌠⎡P⎤ Q'.
-Proof.
- rewrite /KnownFrame /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q).
-Qed.
+ Frame p ⌜φ⌠P Q → MakeEmbed Q Q' → Frame p ⌜φ⌠⎡P⎤ Q'.
+Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
Proof. apply left_id, _. Qed.
@@ -777,31 +775,31 @@ Proof. by rewrite /MakeSep. Qed.
Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
Frame true R P1 Q1 → MaybeFrame true R P2 Q2 progress → MakeSep Q1 Q2 Q' →
- KnownFrame true R (P1 ∗ P2) Q' | 9.
+ Frame true R (P1 ∗ P2) Q' | 9.
Proof.
- rewrite /KnownFrame /Frame /MaybeFrame /MakeSep /= => <- <- <-.
+ rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
rewrite {1}(affinely_persistently_sep_dup R). solve_sep_entails.
Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
- Frame false R P1 Q → MakeSep Q P2 Q' → KnownFrame false R (P1 ∗ P2) Q' | 9.
-Proof. rewrite /KnownFrame /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
+ Frame false R P1 Q → MakeSep Q P2 Q' → Frame false R (P1 ∗ P2) Q' | 9.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
Global Instance frame_sep_r p R P1 P2 Q Q' :
- Frame p R P2 Q → MakeSep P1 Q Q' → KnownFrame p R (P1 ∗ P2) Q' | 10.
+ Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
Proof.
- rewrite /KnownFrame /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
+ rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc.
Qed.
Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
IsCons l x l' →
Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
- KnownFrame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
-Proof. rewrite /IsCons=>->. by rewrite /KnownFrame /Frame big_sepL_cons. Qed.
+ Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
IsApp l l1 l2 →
Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
[∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
- KnownFrame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
-Proof. rewrite /IsApp=>->. by rewrite /KnownFrame /Frame big_opL_app. Qed.
+ Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+Proof. rewrite /IsApp=>->. by rewrite /Frame big_opL_app. Qed.
Global Instance make_and_true_l P : KnownLMakeAnd True P P.
Proof. apply left_id, _. Qed.
@@ -823,9 +821,9 @@ Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
MaybeFrame p R P2 Q2 progress2 →
TCEq (progress1 || progress2) true →
MakeAnd Q1 Q2 Q' →
- KnownFrame p R (P1 ∧ P2) Q' | 9.
+ Frame p R (P1 ∧ P2) Q' | 9.
Proof.
- rewrite /MaybeFrame /KnownFrame /Frame /MakeAnd => <- <- _ <-. apply and_intro;
+ rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-. apply and_intro;
[rewrite and_elim_l|rewrite and_elim_r]; done.
Qed.
@@ -843,9 +841,9 @@ Proof. by rewrite /MakeOr. Qed.
(* We could in principle write the instance [frame_or_spatial] by a bunch of
instances, i.e. (omitting the parameter [p = false]):
- Frame R P1 Q1 → Frame R P2 Q2 → KnownFrame R (P1 ∨ P2) (Q1 ∨ Q2)
- Frame R P1 True → KnownFrame R (P1 ∨ P2) P2
- Frame R P2 True → KnownFrame R (P1 ∨ P2) P1
+ Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
+ Frame R P1 True → Frame R (P1 ∨ P2) P2
+ Frame R P2 True → Frame R (P1 ∨ P2) P1
The problem here is that Coq will try to infer [Frame R P1 ?] and [Frame R P2 ?]
multiple times, whereas the current solution makes sure that said inference
@@ -859,19 +857,19 @@ Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
(TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
(TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
MakeOr Q1 Q2 Q →
- KnownFrame false R (P1 ∨ P2) Q | 9.
-Proof. rewrite /KnownFrame /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
+ Frame false R (P1 ∨ P2) Q | 9.
+Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
MaybeFrame true R P1 Q1 progress1 → MaybeFrame true R P2 Q2 progress2 →
TCEq (progress1 || progress2) true →
- MakeOr Q1 Q2 Q → KnownFrame true R (P1 ∨ P2) Q | 9.
-Proof. rewrite /KnownFrame /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
+ MakeOr Q1 Q2 Q → Frame true R (P1 ∨ P2) Q | 9.
+Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
Global Instance frame_wand p R P1 P2 Q2 :
- Frame p R P2 Q2 → KnownFrame p R (P1 -∗ P2) (P1 -∗ Q2).
+ Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2).
Proof.
- rewrite /KnownFrame /Frame=> ?. apply wand_intro_l.
+ rewrite /Frame=> ?. apply wand_intro_l.
by rewrite assoc (comm _ P1) -assoc wand_elim_r.
Qed.
@@ -883,9 +881,9 @@ Global Instance make_affinely_default P : MakeAffinely P (bi_affinely P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
Global Instance frame_affinely R P Q Q' :
- Frame true R P Q → MakeAffinely Q Q' → KnownFrame true R (bi_affinely P) Q'.
+ Frame true R P Q → MakeAffinely Q Q' → Frame true R (bi_affinely P) Q'.
Proof.
- rewrite /KnownFrame /Frame /MakeAffinely=> <- <- /=.
+ rewrite /Frame /MakeAffinely=> <- <- /=.
by rewrite -{1}affinely_idemp affinely_sep_2.
Qed.
@@ -901,9 +899,9 @@ Global Instance make_absorbingly_default P : MakeAbsorbingly P (bi_absorbingly P
Proof. by rewrite /MakeAbsorbingly. Qed.
Global Instance frame_absorbingly p R P Q Q' :
- Frame p R P Q → MakeAbsorbingly Q Q' → KnownFrame p R (bi_absorbingly P) Q'.
+ Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (bi_absorbingly P) Q'.
Proof.
- rewrite /KnownFrame /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
+ rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
Qed.
Global Instance make_persistently_true : @KnownMakePersistently PROP True True.
@@ -918,45 +916,38 @@ Global Instance make_persistently_default P :
Proof. by rewrite /MakePersistently. Qed.
Global Instance frame_persistently R P Q Q' :
- Frame true R P Q → MakePersistently Q Q' → KnownFrame true R (bi_persistently P) Q'.
+ Frame true R P Q → MakePersistently Q Q' → Frame true R (bi_persistently P) Q'.
Proof.
- rewrite /KnownFrame /Frame /MakePersistently=> <- <- /=.
+ rewrite /Frame /MakePersistently=> <- <- /=.
rewrite -persistently_and_affinely_sep_l.
by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_affinely
persistently_idemp.
Qed.
Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
- (∀ a, Frame p R (Φ a) (Ψ a)) → KnownFrame p R (∃ x, Φ x) (∃ x, Ψ x).
-Proof. rewrite /KnownFrame /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
+ (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
- (∀ a, Frame p R (Φ a) (Ψ a)) → KnownFrame p R (∀ x, Φ x) (∀ x, Ψ x).
-Proof. rewrite /KnownFrame /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+ (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
Global Instance frame_impl_persistent R P1 P2 Q2 :
- Frame true R P2 Q2 → KnownFrame true R (P1 → P2) (P1 → Q2).
+ Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
Proof.
- rewrite /KnownFrame /Frame /= => ?. apply impl_intro_l.
+ rewrite /Frame /= => ?. apply impl_intro_l.
by rewrite -persistently_and_affinely_sep_l assoc (comm _ P1) -assoc impl_elim_r
persistently_and_affinely_sep_l.
Qed.
Global Instance frame_impl R P1 P2 Q2 :
Persistent P1 → Absorbing P1 →
- Frame false R P2 Q2 → KnownFrame false R (P1 → P2) (P1 → Q2).
+ Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2).
Proof.
- rewrite /KnownFrame /Frame /==> ???. apply impl_intro_l.
+ rewrite /Frame /==> ???. apply impl_intro_l.
rewrite {1}(persistent P1) persistently_and_affinely_sep_l assoc.
rewrite (comm _ (â–¡ P1)%I) -assoc -persistently_and_affinely_sep_l.
rewrite persistently_elim impl_elim_r //.
Qed.
-(* In the case nothing else suceeded, then we try to instantiate the
- evar [P] with [R ∗ Q]. This only does so in non-persistent mode:
- The idea is that persistent assumptions will still be available
- when [P] will be used, so there is no need to keep it in [P]. *)
-Global Instance frame_sep_instantiate R Q : Frame false R (R ∗ Q) Q | 100.
-Proof. by rewrite /Frame. Qed.
-
(* IntoEmbed *)
Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
IntoEmbed ⎡P⎤ P.
@@ -1054,7 +1045,7 @@ Global Instance into_wand_later p q R P Q :
IntoWand p q R P Q → IntoWand p q (▷ R) (▷ P) (▷ Q).
Proof.
rewrite /IntoWand /= => HR.
- by rewrite !later_affinely_persistently_if_2 -later_wand HR.
+ by rewrite !later_affinely_persistently_if_2 -later_wand HR.
Qed.
Global Instance into_wand_later_args p q R P Q :
IntoWand p q R P Q → IntoWand' p q R (▷ P) (▷ Q).
@@ -1067,7 +1058,7 @@ Global Instance into_wand_laterN n p q R P Q :
IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
Proof.
rewrite /IntoWand /= => HR.
- by rewrite !laterN_affinely_persistently_if_2 -laterN_wand HR.
+ by rewrite !laterN_affinely_persistently_if_2 -laterN_wand HR.
Qed.
Global Instance into_wand_laterN_args n p q R P Q :
IntoWand p q R P Q → IntoWand' p q R (▷^n P) (▷^n Q).
@@ -1506,8 +1497,8 @@ Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
(* Frame *)
Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP')
{A : ofeT} (a b : A) :
- Frame p (a ≡ b) P Q → MakeEmbed Q Q' → KnownFrame p (a ≡ b) ⎡P⎤ Q'.
-Proof. rewrite /KnownFrame /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
+ Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
+Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
@@ -1520,25 +1511,25 @@ Proof. by rewrite /MakeLaterN. Qed.
Global Instance frame_later p R R' P Q Q' :
NoBackTrack (MaybeIntoLaterN true 1 R' R) →
- Frame p R P Q → MakeLaterN 1 Q Q' → KnownFrame p R' (▷ P) Q'.
+ Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'.
Proof.
- rewrite /KnownFrame /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
+ rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
by rewrite later_affinely_persistently_if_2 later_sep.
Qed.
Global Instance frame_laterN p n R R' P Q Q' :
NoBackTrack (MaybeIntoLaterN true n R' R) →
- Frame p R P Q → MakeLaterN n Q Q' → KnownFrame p R' (▷^n P) Q'.
+ Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
Proof.
- rewrite /KnownFrame /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
+ rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
by rewrite laterN_affinely_persistently_if_2 laterN_sep.
Qed.
Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
- Frame p R P Q → KnownFrame p R (|==> P) (|==> Q).
-Proof. rewrite /KnownFrame /Frame=><-. by rewrite bupd_frame_l. Qed.
+ Frame p R P Q → Frame p R (|==> P) (|==> Q).
+Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
- Frame p R P Q → KnownFrame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
-Proof. rewrite /KnownFrame /Frame=><-. by rewrite fupd_frame_l. Qed.
+ Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
@@ -1546,9 +1537,9 @@ Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
Proof. by rewrite /MakeExcept0. Qed.
Global Instance frame_except_0 p R P Q Q' :
- Frame p R P Q → MakeExcept0 Q Q' → KnownFrame p R (◇ P) Q'.
+ Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
Proof.
- rewrite /KnownFrame /Frame /MakeExcept0=><- <-.
+ rewrite /Frame /MakeExcept0=><- <-.
by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 119c45711..255c7bce9 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -254,19 +254,7 @@ Proof. done. Qed.
Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
-(* [P] has - hint mode even though it is morally an input. In the case
- P is an evar, it will be instantiated with [R * ?P'], where [?P']
- is a new evar. This mechanism should be the only instance able to
- instanciate [P] when it is an evar. *)
-Hint Mode Frame + + ! - - : typeclass_instances.
-
-(* [KnownFrame] is like [Frame], but with an [Hint Mode] that make
- sure we do not instantiate [P]. *)
-Class KnownFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
- known_frame :> Frame p R P Q.
-Arguments KnownFrame {_} _ _%I _%I _%I.
-Arguments known_frame {_ _} _%I _%I _%I {_}.
-Hint Mode KnownFrame + + ! ! - : typeclass_instances.
+Hint Mode Frame + + ! ! - : typeclass_instances.
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 179150e90..d6b37072c 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -332,16 +332,16 @@ Qed.
search, and hence performance issues. *)
Global Instance frame_monPred_at p P Q ð“ R i j :
IsBiIndexRel i j → Frame p R P Q → MakeMonPredAt j Q ð“ →
- KnownFrame p (R i) (P j) ð“ .
+ Frame p (R i) (P j) ð“ .
Proof.
- rewrite /KnownFrame /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if
+ rewrite /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if
/IsBiIndexRel=> Hij <- <-.
destruct p; by rewrite Hij monPred_at_sep ?monPred_at_affinely ?monPred_at_persistently.
Qed.
Global Instance frame_monPred_at_embed i p P Q ð“ ð“¡ :
- Frame p ⎡ð“¡âŽ¤ P Q → MakeMonPredAt i Q ð“ → KnownFrame p ð“¡ (P i) ð“ .
+ Frame p ⎡ð“¡âŽ¤ P Q → MakeMonPredAt i Q ð“ → Frame p ð“¡ (P i) ð“ .
Proof.
- rewrite /KnownFrame /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if=> <- <-.
+ rewrite /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if=> <- <-.
destruct p; by rewrite monPred_at_sep ?monPred_at_affinely
?monPred_at_persistently monPred_at_embed.
Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index e013d4e38..329ec130b 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -370,15 +370,15 @@ Proof.
Qed.
Lemma iFrame_with_evar_r P Q :
- ∃ R, (P -∗ Q -∗ P ∗ R) ∧ R = (Q ∗ emp)%I.
+ ∃ R, (P -∗ Q -∗ P ∗ R) ∧ R = Q.
Proof.
- eexists. split. iIntros "HP HQ". iFrame. iEmpIntro. done.
+ eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
Qed.
Lemma iFrame_with_evar_l P Q :
- ∃ R, (P -∗ Q -∗ R ∗ P) ∧ R = (Q ∗ emp)%I.
+ ∃ R, (P -∗ Q -∗ R ∗ P) ∧ R = Q.
Proof.
- eexists. split. iIntros "HP HQ". iFrame "HQ".
- iSplitR. iEmpIntro. done. done.
+ eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
+ by iSplitR "HP". done.
Qed.
Lemma iFrame_with_evar_persistent P Q :
∃ R, (P -∗ □ Q -∗ P ∗ R ∗ Q) ∧ R = emp%I.
--
GitLab