# 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 that`True`

is somehow more fundamental than`emp`

. That clarifies what`iStartProof`

should do, but now, how should`emp`

be represented? Maybe the empty spatial context is`True`

, but when non-empty, we just`*`

together what we have, so`emp`

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 an`emp`

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 to`True`

, otherwise to the iterated`*`

. This is also awkward in some circumstances, e.g. when the spatial context is currently missing and the goal is`P -* Q`

and we do`iIntros`

-- now a`True`

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?