Skip to content

WIP Define persistently from the BI interface.

Joseph Tassarotti requested to merge joe/defined_pers into gen_proofmode

This is work in progress to explore the possibility of defining a persistently modality for any BI rather than including such a modality within the interface.

What is done so far is to define a class of persistable modalities. These are modalities that satisfy the properties of the persistently modality, except that:

  • The analogs of the axioms <pers> (▷ P) ⊢ ▷ (<pers> P) and commuting with existentials are dropped.
  • Commuting with foralls is replaced by <pers> P ∧ <pers> Q ⊢ <pers> (P ∧ Q)

I then show that in any BI, at least one such persistable modality exists. Next, it is shown that there exists a "largest" persistable modality as a sort of join of all the other persistable modalities -- though some care has to be taken to preserve the above conjunction rule when doing so. I then define <pers> to be this largest one. (Largest here means that if M is another persistable modality, then M P ⊢ <pers> P.) See the file bi/persistable.v.

The missing axioms may at first seem important, however, I believe that they are not needed for the functionality of the Proof Mode, per-se:

  • It is the other direction of commuting with later that is needed for the iLöb tactic, and this one is retained.
  • If one replaces cases where we had hypotheses of the form <pers> (∃ a, Ψ a) with instead <pers> (∃ a, <pers> Ψ a) then the loss of the commuting with existentials rule does not seem so bad. And, the latter form should be provable in cases where hypotheses of the old form were provable using a persistence modality that did satisfy commuting with existentials.
  • Similar arguments suggest commuting with forall is not so important either. Robbert made some preliminary explorations into the effect of dropping this axiom in the following branch: https://gitlab.mpi-sws.org/FP/iris-coq/tree/no_always_forall

I have not yet updated base_logic/ and the rest of the dependencies to see what happens.

There are a few annoyances in the way this is structured so far:

  • Robbert had originally suggested that we should still keep the flexibility for the user to plug in their particular persistence modality, even if a "greatest" modality could be defined. I agree that this may be useful, however, as it stands proving that the way I defined <pers> has the desired properties requires using some non-trivial derived facts about BI connectives. So, if we want to go this way, it might make sense to split the BI interface into a BI and a BI++, the latter being where the persistence modality is plugged in.

  • Right now, the <pers> modality is only defined for an SBI, rather than for a BI. This is for two reasons: first, the definition needs to use sbi_internal_eq, which is only exposed in the SBI interface. Arguably, sbi_internal_eq should be moved into the BI interface: after all, we already impose an OFE structure at this level and demand that various connectives be non-expansive and so on. The more serious reason that it's only defined for SBI is that, if we want the commuting with later rule, then when we define <pers> as the "largest" persistable modality, we only want to quantify over persistable modalities that themselves satisfy the commuting with later rule -- and this only makes sense to speak of in the setting of an SBI. Of course, there is a trivial SBI structure that can be associated with every BI, so perhaps it's not so bad.

  • There are some missing except_0 and Timeless instances, since the prior proofs for these relied on properties of <pers> even for connectives that had nothing to do with <pers>. I haven't yet bothered to update these proofs.

The idea of seeing if we could define a persistence modality from the BI interface directly arose in discussions with @robbertkrebbers @jung.

Edited by Joseph Tassarotti

Merge request reports