WIP: Strong framing
This MR makes an attempt at closing #71 (closed). Todo:
Syntax
I am not sure I like what we have now:
Lemma demo_17 (M : ucmraT) (P Q R : uPred M) :
P -∗ Q -∗ R -∗ (P ∗ Q ∨ R ∗ False).
Proof.
iIntros "^$ HQ HR {^$HR}".
iAssert (Q ∨ False)%I with "[^$HQ]" as "[HQ|[]]".
iFrame "^HQ".
Qed.
Note that we have syntax for framing in 1.) introduction patterns to frame introduced hypotheses on the fly 2.) The clear syntax {sel_pat}
in introduction patterns 3.) specialization patterns 4.) the frame tactic. I tried to get some form of consistency, but suggestions for improvements are very welcome.
As I mentioned in #71 (closed):
It would be nice to have a "do more" modifier that we can also in other places.
For example, we have
iIntros "!>"
to introduce a modality. In #48 (closed) it is proposed to make the modality introduction behave likeiNext
(i.e. also strip modalities from the context). This will probably be costly, so in that case we may to keep!>
letting introduce a modality, but have something likeDO_MORE!>
to also strip the modalities from all hypotheses.
The ^
token plays that role.
Approach
As I wrote in #71 (closed) this can be implemented in at least two ways:
- Have an additional hint database
strong_frame
for dangerous frame instances. - Extend the
Frame
type class with a Booleanstrong
.
In this MR I went for (1) because it requires the least modifications. One has to be a bit careful about not introducing overlapping instances (and hence unneeded backtracking on failures) when using the typeclass_instances
and strong_frame
hint database together, but I think I managed.
Documentation
The new MaybeFrame
type class and strong_frame
hint database should be documented. Also ProofMode.md
should be modified.