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
  • Issues
  • #213
Closed
Open
Issue created Oct 04, 2018 by Robbert Krebbers@robbertkrebbersMaintainer

Moving hypotheses from the intuitionistic to the spatial context

Right now, there appears to be no decent way to move hypotheses from the intuitionistic context to the spatial context.

I thought this should never be needed, but I was proved wrong. As @jtassaro shows in (https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/171/diffs#d026f8137ab7b7e373742e0df76ccf325011a5cf_53_89), this is sometimes needed before doing an induction.

I suppose we could make a tactic for this (and a corresponding introduction pattern like -# pat), but I'm not sure I like that very much. Also, in the case of a generic BI, there is probably the choice of having an <affine> modality or not.

As an alternative, if we believe this only ever occurs when doing induction, we could extend the syntax of the forall argument of iInduction to allow moving hypotheses from the intuitionistic to the spatial context.

Edited Nov 01, 2019 by Ralf Jung
Assignee
Assign to
Time tracking