Skip to content

Draft: Add simple library for priority levels and use it for `iFrame`

Robbert Krebbers requested to merge robbert/level into master

As already discussed here: !739 (merged)

I now designed a solution that does not require to add an additional argument to the Frame class. Instead, it puts a dummy constant in the Coq context, and rules that have side-conditions on the priority level have a TC premise that checks if the level is OK. I have implemented the priority levels as a separate library that in principle could be used for other tactics too.

TODO:

  • Figure out where the priority level library should go to. I put it in iris.proofmode, but in principle it has nothing to with the proof mode.
  • Figure out syntax for iFrame and friends to give the priority level in a concise way.
  • Determine what levels we need for iFrame. I think we don't want framing for ∧, ∨, and Fractional by default. Are there more examples? What levels would be appropriate?
  • Adapt the proof scripts, I currently use at_level by lack of syntax.
Edited by Robbert Krebbers

Merge request reports