GitLab

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.