Commit 998bdedf authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Get rid of KnownFrame and iFrame automatically instantiating evars.

parent 35ca0d9b
......@@ -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 /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.
......
......@@ -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 /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.
......
This diff is collapsed.
......@@ -253,19 +253,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
......
......@@ -342,16 +342,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 /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 /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.
......
......@@ -371,15 +371,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.
......
Markdown is supported
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