Right now, iframe is a faithful port of Rocq's tactic. However, there are some changes we may consider making to tweak its behavior. This issue is here to consider and discuss potential tweaks to the tactic.
iframe does not eliminate emp (eg. in the goal P ∗ emp)iframe automatically uses Iris hypotheses, but not pure hypotheses. It will not frame out P ∗ ⌜φ⌝ even if φ is a pure hypothesis you have exactly.- Adding a hypothesis to
iframe actually causes it to use less facts, as it will try to solve the framing goals using only the supplied arguments
Idea for 2/3: Change the iframe syntax to be more like simp and grind
iframe can be whatever behavior we decide we want to be the defaultiframe H (including pure syntax like iframe %P) to include additional hypotheses in the set iframe usesiframe only H for the existing behavior of iframe H
I wonder even if we can implement iframe? to help squeeze internal iframe statements. Probably not a big deal since iframe operates on a much smaller scale than simp anyways.
The genesis for this suggestion was that I was using iframe, I need to add a pure hypothesis, and I found it sort of annoying to have to go through and figure out all the names of stuff iframe was picking up on, just write them all out plus supply it this one additional pure hypothesis.
Right now,
iframeis a faithful port of Rocq's tactic. However, there are some changes we may consider making to tweak its behavior. This issue is here to consider and discuss potential tweaks to the tactic.iframedoes not eliminateemp(eg. in the goalP ∗ emp)iframeautomatically uses Iris hypotheses, but not pure hypotheses. It will not frame outP ∗ ⌜φ⌝even ifφis a pure hypothesis you have exactly.iframeactually causes it to use less facts, as it will try to solve the framing goals using only the supplied argumentsIdea for 2/3: Change the
iframesyntax to be more likesimpandgrindiframecan be whatever behavior we decide we want to be the defaultiframe H(including pure syntax likeiframe %P) to include additional hypotheses in the setiframeusesiframe only Hfor the existing behavior ofiframe HI wonder even if we can implement
iframe?to help squeeze internaliframestatements. Probably not a big deal sinceiframeoperates on a much smaller scale thansimpanyways.The genesis for this suggestion was that I was using
iframe, I need to add a pure hypothesis, and I found it sort of annoying to have to go through and figure out all the names of stuffiframewas picking up on, just write them all out plus supply it this one additional pure hypothesis.