Verified Commit 476870ac authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Ensure `Frame` instances are not tried before `frame_here`

parent ebce5b7c
Pipeline #50594 passed with stage
in 12 minutes and 52 seconds
......@@ -71,6 +71,8 @@ Coq 8.11 is no longer supported in this version of Iris.
* `iMod`/`iModIntro` show proper error messages when they fail due to mask
mismatches. To support this, the proofmode typeclass `FromModal` now takes an
additional pure precondition.
* Fix performance of `iFrame` in logics without `BiAffine` (by Paolo G.
Giarrusso, BedRock Systems).
**Changes in `bi`:**
......
......@@ -19,6 +19,12 @@ Section bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
(* Frame *)
(*
When framing [R] against itself, we leave [True] if possible (via
[frame_here_absorbing] or [frame_affinely_here_absorbing]) since it is a weaker
goal. Otherwise we leave [emp] via [frame_here].
Only if all those options fail, we start decomposing [R].
To ensure that, all other instances must have priority > 1. *)
Global Instance frame_here_absorbing p R : Absorbing R Frame p R R True | 0.
Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
Global Instance frame_here p R : Frame p R R emp | 1.
......@@ -36,7 +42,7 @@ Proof.
Qed.
Global Instance frame_here_pure_persistent a φ Q :
FromPure a Q φ Frame true ⌜φ⌝ Q emp.
FromPure a Q φ Frame true ⌜φ⌝ Q emp | 2.
Proof.
rewrite /FromPure /Frame /= => <-. rewrite right_id.
by rewrite -affinely_affinely_if intuitionistically_affinely.
......@@ -44,7 +50,7 @@ Qed.
Global Instance frame_here_pure a φ Q :
FromPure a Q φ
TCOr (TCEq a false) (BiAffine PROP)
Frame false ⌜φ⌝ Q emp.
Frame false ⌜φ⌝ Q emp | 2. (* Same prio as default. *)
Proof.
rewrite /FromPure /Frame => <- [->|?] /=.
- by rewrite right_id.
......@@ -62,13 +68,13 @@ 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' Frame p R P Q'.
Frame p R P Q MakeEmbed Q Q' Frame p R P Q' | 2. (* Same prio as default. *)
Proof.
rewrite /Frame /MakeEmbed => <- <-.
rewrite embed_sep embed_intuitionistically_if_2 => //.
Qed.
Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
Frame p ⌜φ⌝ P Q MakeEmbed Q Q' Frame p ⌜φ⌝ P Q'.
Frame p ⌜φ⌝ P Q MakeEmbed Q Q' Frame p ⌜φ⌝ P Q' | 2. (* Same prio as default. *)
Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
......@@ -102,20 +108,20 @@ 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
Frame p R ([ list] k y l, Φ k y) Q.
Frame p R ([ list] k y l, Φ k y) Q | 2. (* Same prio as default. *)
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
Frame p R ([ list] k y l, Φ k y) Q.
Frame p R ([ list] k y l, Φ k y) Q | 2. (* Same prio as default. *)
Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
Global Instance frame_big_sepL2_cons {A B} p (Φ : nat A B PROP)
R Q l1 x1 l1' l2 x2 l2' :
IsCons l1 x1 l1' IsCons l2 x2 l2'
Frame p R (Φ 0 x1 x2 [ list] k y1;y2 l1';l2', Φ (S k) y1 y2) Q
Frame p R ([ list] k y1;y2 l1;l2, Φ k y1 y2) Q.
Frame p R ([ list] k y1;y2 l1;l2, Φ k y1 y2) Q. (* Default prio > 1. *)
Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.
Global Instance frame_big_sepL2_app {A B} p (Φ : nat A B PROP)
R Q l1 l1' l1'' l2 l2' l2'' :
......@@ -127,7 +133,7 @@ Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A PROP) R Q X1 X2 :
Frame p R (([ mset] y X1, Φ y) [ mset] y X2, Φ y) Q
Frame p R ([ mset] y X1 X2, Φ y) Q.
Frame p R ([ mset] y X1 X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
Global Instance make_and_true_l P : KnownLMakeAnd True P P.
......@@ -192,7 +198,7 @@ Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
Global Instance frame_wand p R P1 P2 Q2 :
Frame p R P2 Q2 Frame p R (P1 - P2) (P1 - Q2).
Frame p R P2 Q2 Frame p R (P1 - P2) (P1 - Q2) | 2.
Proof.
rewrite /Frame=> ?. apply wand_intro_l.
by rewrite assoc (comm _ P1) -assoc wand_elim_r.
......@@ -207,7 +213,7 @@ Proof. by rewrite /MakeAffinely. Qed.
Global Instance frame_affinely p R P Q Q' :
TCOr (TCEq p true) (Affine R)
Frame p R P Q MakeAffinely Q Q' Frame p R (<affine> P) Q'.
Frame p R P Q MakeAffinely Q Q' Frame p R (<affine> P) Q'. (* Default prio > 1 *)
Proof.
rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
......@@ -230,7 +236,7 @@ Global Instance make_intuitionistically_default P :
Proof. by rewrite /MakeIntuitionistically. Qed.
Global Instance frame_intuitionistically R P Q Q' :
Frame true R P Q MakeIntuitionistically Q Q' Frame true R ( P) Q'.
Frame true R P Q MakeIntuitionistically Q Q' Frame true R ( P) Q' | 2. (* Same prio as default. *)
Proof.
rewrite /Frame /MakeIntuitionistically=> <- <- /=.
rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
......@@ -247,7 +253,7 @@ Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 10
Proof. by rewrite /MakeAbsorbingly. Qed.
Global Instance frame_absorbingly p R P Q Q' :
Frame p R P Q MakeAbsorbingly Q Q' Frame p R (<absorb> P) Q'.
Frame p R P Q MakeAbsorbingly Q Q' Frame p R (<absorb> P) Q' | 2. (* Same prio as default. *)
Proof.
rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
Qed.
......@@ -264,7 +270,7 @@ 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' Frame true R (<pers> P) Q'.
Frame true R P Q MakePersistently Q Q' Frame true R (<pers> P) Q' | 2. (* Same prio as default. *)
Proof.
rewrite /Frame /MakePersistently=> <- <- /=.
rewrite -persistently_and_intuitionistically_sep_l.
......@@ -273,20 +279,20 @@ Proof.
Qed.
Global Instance frame_exist {A} p R (Φ Ψ : A PROP) :
( a, Frame p R (Φ a) (Ψ a)) Frame p R ( x, Φ x) ( x, Ψ x).
( a, Frame p R (Φ a) (Ψ a)) Frame p R ( x, Φ x) ( x, Ψ x) | 2.
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
Global Instance frame_texist {TT : tele} p R (Φ Ψ : TT PROP) :
( x, Frame p R (Φ x) (Ψ x)) Frame p R (.. x, Φ x) (.. x, Ψ x).
( x, Frame p R (Φ x) (Ψ x)) Frame p R (.. x, Φ x) (.. x, Ψ x) | 2.
Proof. rewrite /Frame !bi_texist_exist. apply frame_exist. Qed.
Global Instance frame_forall {A} p R (Φ Ψ : A PROP) :
( a, Frame p R (Φ a) (Ψ a)) Frame p R ( x, Φ x) ( x, Ψ x).
( a, Frame p R (Φ a) (Ψ a)) Frame p R ( x, Φ x) ( x, Ψ x) | 2.
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
Global Instance frame_tforall {TT : tele} p R (Φ Ψ : TT PROP) :
( x, Frame p R (Φ x) (Ψ x)) Frame p R (.. x, Φ x) (.. x, Ψ x).
( x, Frame p R (Φ x) (Ψ x)) Frame p R (.. x, Φ x) (.. x, Ψ x) | 2.
Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
Global Instance frame_impl_persistent R P1 P2 Q2 :
Frame true R P2 Q2 Frame true R (P1 P2) (P1 Q2).
Frame true R P2 Q2 Frame true R (P1 P2) (P1 Q2) | 2.
Proof.
rewrite /Frame /= => ?. apply impl_intro_l.
by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
......@@ -294,7 +300,7 @@ Proof.
Qed.
Global Instance frame_impl R P1 P2 Q2 :
Persistent P1 Absorbing P1
Frame false R P2 Q2 Frame false R (P1 P2) (P1 Q2).
Frame false R P2 Q2 Frame false R (P1 P2) (P1 Q2). (* Default prio > 1 *)
Proof.
rewrite /Frame /==> ???. apply impl_intro_l.
rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
......@@ -305,7 +311,7 @@ Qed.
Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
!BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
p P Q (Q' : PROP') {A : ofe} (a b : A) :
Frame p (a b) P Q MakeEmbed Q Q' Frame p (a b) P Q'.
Frame p (a b) P Q MakeEmbed Q Q' Frame p (a b) P Q'. (* Default prio > 1 *)
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.
......@@ -318,24 +324,24 @@ Proof. by rewrite /MakeLaterN. Qed.
Global Instance frame_later p R R' P Q Q' :
TCNoBackTrack (MaybeIntoLaterN true 1 R' R)
Frame p R P Q MakeLaterN 1 Q Q' Frame p R' ( P) Q'.
Frame p R P Q MakeLaterN 1 Q Q' Frame p R' ( P) Q'. (* Default prio > 1 *)
Proof.
rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
by rewrite later_intuitionistically_if_2 later_sep.
Qed.
Global Instance frame_laterN p n R R' P Q Q' :
TCNoBackTrack (MaybeIntoLaterN true n R' R)
Frame p R P Q MakeLaterN n Q Q' Frame p R' (^n P) Q'.
Frame p R P Q MakeLaterN n Q Q' Frame p R' (^n P) Q'. (* Default prio > 1 *)
Proof.
rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
by rewrite laterN_intuitionistically_if_2 laterN_sep.
Qed.
Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
Frame p R P Q Frame p R (|==> P) (|==> Q).
Frame p R P Q Frame p R (|==> P) (|==> Q) | 2.
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 Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Frame p R P Q Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
......@@ -344,7 +350,7 @@ 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' Frame p R ( P) Q'.
Frame p R P Q MakeExcept0 Q Q' Frame p R ( P) Q' | 2. (* Same prio as default *)
Proof.
rewrite /Frame /MakeExcept0=><- <-.
by rewrite except_0_sep -(except_0_intro (?p R)).
......
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