Commit 09663be3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Make iFrame able to accumulate assertions in an evar.

This requires changing the Hint Mode of the [Frame] type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of [Frame] to intantiate this evar themselves, we create a new type class [KnwonFrame], which corresponds to the old behavior.
parent 56f80319
......@@ -255,7 +255,7 @@ Proof.
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iExists γ', (Q' P')%I. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed.
......
......@@ -98,7 +98,7 @@ Section proofs.
( P cinv_own γ p) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
iApply (Helim with "[- $H2]"); first done.
iApply Helim; [done|]. iSplitR "H2"; [|done].
iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
......
......@@ -101,7 +101,7 @@ Global Instance elim_inv_inv E N P Q Q' :
ElimInv (N E) (inv N P) True ( P) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
iApply (Helim with "[$H2]"); first done.
iApply (Helim with "[H2]"); [done|]. iSplitR "H2"; [|done].
iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
Qed.
......
......@@ -118,7 +118,7 @@ Section proofs.
( P na_own p (F∖↑N)) ( P na_own p (F∖↑N) ={E}= na_own p F) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
iApply (Helim with "[- $H2]"); first done.
iApply Helim; [done|]. iSplitR "H2"; [|done].
iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
......
......@@ -377,8 +377,9 @@ Section proofmode_classes.
Implicit Types Φ : val Λ iProp Σ.
Global Instance frame_twp p s E e R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v)) Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
( 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.
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.
......
......@@ -371,8 +371,9 @@ Section proofmode_classes.
Implicit Types Φ : val Λ iProp Σ.
Global Instance frame_wp p s E e R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v)) Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Ψ }}).
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
( 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.
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,7 +253,19 @@ 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 {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.
(* [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.
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
......@@ -262,7 +274,7 @@ Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : ?p R Q P.
Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
Hint Mode MaybeFrame + + ! ! - - : typeclass_instances.
Hint Mode MaybeFrame + + ! - - - : typeclass_instances.
Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
Frame p R P Q MaybeFrame p R P Q true.
......
......@@ -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 𝓠
Frame p (R i) (P j) 𝓠.
KnownFrame p (R i) (P j) 𝓠.
Proof.
rewrite /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if
rewrite /KnownFrame /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 𝓠 Frame p 𝓡 (P i) 𝓠.
Frame p ⎡𝓡⎤ P Q MakeMonPredAt i Q 𝓠 KnownFrame p 𝓡 (P i) 𝓠.
Proof.
rewrite /Frame /MakeMonPredAt /bi_affinely_if /bi_persistently_if=> <- <-.
rewrite /KnownFrame /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,13 +371,20 @@ Proof.
Qed.
Lemma iFrame_with_evar_r P Q :
P - Q - R, P R.
R, (P - Q - P R) R = (Q emp)%I.
Proof.
iIntros "HP HQ". iExists _. iFrame. iApply "HQ".
eexists. split. iIntros "HP HQ". iFrame. iEmpIntro. done.
Qed.
Lemma iFrame_with_evar_l P Q :
P - Q - R, R P.
R, (P - Q - R P) R = (Q emp)%I.
Proof.
iIntros "HP HQ". iExists _. iFrame. iApply "HQ".
eexists. split. iIntros "HP HQ". iFrame "HQ".
iSplitR. iEmpIntro. done. done.
Qed.
Lemma iFrame_with_evar_persistent P Q :
R, (P - Q - P R Q) R = emp%I.
Proof.
eexists. split. iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro. done.
Qed.
End tests.
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