register make_laterable as modality
Upamanyu (student at MIT) started looking into
make_laterable, which made me realize that it might be worth properly registering this as a modality so we can do
iModIntro. However, it turns out the old definition of
make_laterable is not suited for that: it does not satisfy the lemma
Lemma make_laterable_intro' Q : Laterable Q → Q -∗ make_laterable Q.
So, when doing
iModIntro on a
make_laterable, we couldn't just keep all
Laterable things in the context -- we would additionally get an extra
◇ in front of each of them. To fix that I slightly changed the definition of
make_laterable; most existing laws still hold (or become stronger), with one exception: there's now a
Lemma make_laterable_elim Q : make_laterable Q -∗ ◇ Q.
Still, I think the fact that
make_laterable_intro' now holds shows that this is the better definition. Logically atomic triples (the only in-tree user of all this) are unaffected by this change, their API surface remains the same.
I also changed
make_laterable_wand to a less surprising statement:
Lemma make_laterable_wand Q1 Q2 : make_laterable (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
Sadly, for non-affine BIs, this does not imply the old way of stating that lemma, so that lemma also has to be kept around (under a new name):
Lemma make_laterable_intuitionistic_wand Q1 Q2 : □ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
So, overall I'd say this MR makes
make_laterable much more well-behaved and better integrated into the IPM for affine BIs. Figuring out something reasonable for non-affine BIs remains future work.
When there are non-laterable things in the context,
iModIntro will add a
▷ in front of them to make them laterable. The same approach is now also used by
iAuIntro, though that requires a hack since we cannot actually use
Future plans: #424