GitLab

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?