Handle both `emp` and `True` as context
The generalized proofmode for a linear logic should be able to handle both
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
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.
- Make "both contexts are empty" mean
True, arguing that
Trueis somehow more fundamental than
emp. That clarifies what
iStartProofshould do, but now, how should
empbe represented? Maybe the empty spatial context is
True, but when non-empty, we just
*together what we have, so
empis represented by some
"H": empin 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
empinto 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 -* Qand we do
iIntros-- now a
Truehas 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
* Truearound? 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?