Skip to content

GitLab

WIP: Strong framing

Closed Robbert Krebbers requested to merge strong_frame into master

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 like iNext (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 like DO_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:

  1. Have an additional hint database strong_frame for dangerous frame instances.
  2. Extend the Frame type class with a Boolean strong.

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.

@janno @haidang @jung @jjourdan