The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
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.af5e50e7with Coq 8.11.1.