Skip to content

GitLab

Open
Created by Paolo G. Giarrusso@BlaisorbladeContributor

simpl breaks error checking of `iNext (S i)`

I'd expect iNext (S i) to introduce exactly S i later, and fail otherwise. However, after e.g. simpl turns ▷^(S i) P into ▷ ▷^i P, that will sometimes introduce one later, as shown below.

From iris.proofmode Require Import tactics.

Lemma foo i {PROP} P : P ⊢@{PROP} ▷^(S i) P.
Proof.
  iIntros "H".
  Fail iNext 2.
  iNext (S i).
  Fail iNext i.
  Fail iNext.
  iExact "H".
  Restart.

  iIntros "H /=".
  Fail iNext 2.
  iNext (S i).
  iNext i. (* !!! *)
  Abort.

Iris version

$ opam show coq-iris -f version
dev.2020-05-24.2.af5e50e7

with Coq 8.11.1.

Edited by Paolo G. Giarrusso