Skip to content

Show that for non-step indexed BIs, <pers> can trivially be inhabited.

Robbert Krebbers requested to merge robbert/bi_persistently_mixin into master

See my comment in !843 (closed):

I just realized that there might be a different approach to support BIs without persistence modality. You can define <pers> P := ⌜ emp ⊢ P ⌝ and prove all the laws if:

  • The BI is discrete, that is P ≡{n}≡ Q → P ≡ Q
  • The BI enjoys the existential property: emp ⊢ ∃ x, Φ x implies ∃ x, emp ⊢ Φ x

In fact, I even realized I have done this in my course, where I let my students build a classical separation logic, and use that to instantiate the proof mode in my subsequent lectures.

Merge request reports