Skip to content

GitLab

Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses.

Merged Robbert Krebbers requested to merge robbert/iPureIntro_affine into master

This MR makes it possible to introduce pure facts, even if the spatial context is non-empty, as long as all hypotheses in it are affine (which is trivially true when working in an affine BI).

We already had this behavior for iEmpIntro, so it makes sense to have it for iPureIntro too.

As part of this MR, I had to change the modes of the FromPure class:

Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
  from_pure : <affine>?a ⌜φ⌝ ⊢ P.
Hint Mode FromPure + - ! - : typeclass_instances.

The a argument is now an output, rather than an input. It tells one whether the spatial context needs to be affine or not.