Skip to content

Renaming and notations for modalities gen_proofmode

Robbert Krebbers requested to merge robbert/big_rename into gen_proofmode

This MR implements the following renaming/new notations:

  • <subj> P : subjectively (renamed + new notation)
  • <obj> P : objectively (renamed + new notation)
  • <pers> P : persistently (new notation)
  • <affine> P : affinely (new notation)
  • <absorb> P : absorbingly (new notation)

The following change still needs to be done, and I propose to do it in a separate MR:

  • □ P : intuitionistically a.k.a affinely persistently

This change requires more effort and discussion. In particular, currently this modality is just a notation for the <affine> <pers> ..., but I think it should become a Definition:

Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
  (<affi> <pers> P)%I.

It being a definition reflects that fact that it will have a proper name. This will obviously break some stuff, and will require more work than just running a sed script, hence my proposal to do that in a separate MR.

Since pretty much any commit to gen_proofmode will break this MR, I propose to merge it ASAP.

Merge request reports