Introduce a connective `ilocked` to stop `iNext` and `iFrame`.
This MR introduces a connective called ilocked
that can be used to stop iNext
and iFrame
from unfolding definitions.
To demonstrate why this is useful, consider:
Definition foo : uPred M := (▷ something_big ∧ and_even_bigger)%I
Whenever we have a premise H : foo
, the tactic iNext
will unfold the definition of foo
, which is not always desired. To avoid this behavior, we often seal-off the body of foo
, which is quite a drastic measure, as we need to unseal whenever we want to do anything with a foo
. This is especially cumbersome for auxiliary definitions where sealing doesn't also give a performance gain.
The ilocked
connective in the MR proves a more lightweight solution. When a definition is flagged using ilocked
, the tactics iNext
and iFrame
will not unfold it, but all other tactics, like iDestruct
, iSplit
and iLeft
will.
Definition foo : uPred M := ilocked (▷ something_big ∧ and_even_bigger)%I
It works in a rather simple way, the connective ilocked
is defined Typeclasses Opaque
so that it will not be unfolded by type class search.
Definition ilocked {A} (x : A) : A := x.
Typeclasses Opaque ilocked.
Arguments ilocked {_} _ /.
To make sure that other tactics will unfold it, we define a bunch of instances like:
Instance into_pure_ilocked {M} (P : uPred M) φ :
IntoPure P φ → IntoPure (ilocked P) φ := id.
Instance from_pure_ilocked {M} (P : uPred M) φ :
FromPure P φ → FromPure (ilocked P) φ := id.
Instance from_and_ilocked {M} p (P Q1 Q2 : uPred M) :
FromAnd p P Q1 Q2 → FromAnd p (ilocked P) Q1 Q2 | 100 := id.
Instance into_and_ilocked {M} p (P Q1 Q2 : uPred M) :
IntoAnd p P Q1 Q2 → IntoAnd p (ilocked P) Q1 Q2 := id.
Instance from_or_ilocked {M} (P Q1 Q2 : uPred M) :
FromOr P Q1 Q2 → FromOr (ilocked P) Q1 Q2 := id.
TODO
-
Figure out where to put this stuff. -
What would be a better name for the connective? -
We currently do not have instances for PersistentP
andTimelessP
forilocked
. Should we add those? Are other instances missing?