Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
I
Iris
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 116
    • Issues 116
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 19
    • Merge Requests 19
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • Iris
  • Issues
  • #265

Closed
Open
Opened Sep 06, 2019 by Jonas Kastberg@jihgfeeContributor

Add an "iStopProof" tactic

There is currently no tactic to escape the IPM. This make it so that pre-existing tactics that have been developed for the logic can no longer be used, once you are in the proof mode. This is applicable assuming that someone migrates to IPM from an existing development, and want to keep being able to use their tactics, in-between progress made with IPM.

A WIP solution is as follows:

Lemma stop_proof {PROP : bi} c (P : PROP) :
  P ->
  environments.envs_entails
    {|
      environments.env_intuitionistic := environments.Enil;
      environments.env_spatial := environments.Enil;
      environments.env_counter := c |} P.
Proof. rewrite environments.envs_entails_eq. iIntros. iApply H. Qed.
Ltac iStopProof := apply stop_proof.
Ltac iStopProof' := iRevert "#∗"; iStopProof.
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: iris/iris#265