iframe alterations

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.

1. iframe does not eliminate emp (eg. in the goal P ∗ emp)
2. iframe automatically uses Iris hypotheses, but not pure hypotheses. It will not frame out P ∗ ⌜φ⌝ even if φ is a pure hypothesis you have exactly.
3. 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 default
• iframe H (including pure syntax like iframe %P) to include additional hypotheses in the set iframe uses
• iframe 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.

The issue identifies the iframe tactic as the entry point but names no files or tests. First inspect its implementation and current behavior, then settle the intended default, hypothesis-selection syntax, and whether iframe? is in scope; done requires a recorded decision and corresponding tests.