Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 20
    • Merge requests 20
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !241

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

  • Review changes

  • Download
  • Patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/iPureIntro_affine into master May 06, 2019
  • Overview 4
  • Commits 2
  • Pipelines 0
  • Changes 9

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.

Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/iPureIntro_affine