Handle both `emp` and `True` as context
The generalized proofmode for a linear logic should be able to handle both True
and emp
as the context, ideally both in a somewhat canonical way. However, if both spatial and persistent context are empty, that can only be either emp
or True
; the other one will need a different representation. Right now, it is emp
, so the only way to represent True
is to have it explicitly in the spatial context -- which seems pretty funny. This is related to the problem with plainly and empty contexts (https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/98#note_22868).
In particular, if the goal is valid P
, what should iStartProof
do? (And, for that matter, what does it do currently?) The goal is True |- P
, so the behavior from Iris (having both contexts empty) will not work.
Some options:
- Make "both contexts are empty" mean
True
, arguing thatTrue
is somehow more fundamental thanemp
. That clarifies whatiStartProof
should do, but now, how shouldemp
be represented? Maybe the empty spatial context isTrue
, but when non-empty, we just*
together what we have, soemp
is represented by some"H": emp
in the spatial context? That seems like a strange discontinuitiy though. It means if we "use up" the last spatial assertion, we have to synthesize anemp
into the context -- not very pleasant. - Somehow "deeply embed" this information. For example, the spatial context could be optional (
option list PROP
); when absent, it interprets toTrue
, otherwise to the iterated*
. This is also awkward in some circumstances, e.g. when the spatial context is currently missing and the goal isP -* Q
and we doiIntros
-- now aTrue
has to be synthesized into the spatial context. So maybe the better way to "deeply embed" this is to have some boolean indicating whether the context is "precise" or whether there is a* True
around? Seems really ugly, but this time I cannot come up with a situation where we have to synthesize an assertion.
How is this currently handled in the IPM for Iron?