Skip to content

Draft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the pattern

Robbert Krebbers requested to merge robbert/iIntro_iDestruct_fresh into master

See https://mattermost.mpi-sws.org/iris/pl/samjaqqz8jb7fqepbcefxm47io where @jung wrote:

We have another behavior change from the ltac2 MR:

Lemma test_iDestruct1_pure (Φ: nat → PROP) :
  (∃ y z:nat, Φ y) -∗ ∃ x, Φ x.
Proof.
  iDestruct 1 as (? y) "H".

this now fails because the ? gets name y and then the later y says that the name is already used. it used to work fine, presumably because intros ? y actually does some form of lookahead and avoids picking the name y when a later pattern uses that name?

This MR fixes this issue. Thanks to @snyke7 for the Ltac2 hackery.

Reasons for WIP:

  • iIntros "(% & %y & ?)" still fails on the same example. The problem is that we do not collect names from the Iris intro pattern. This should be simple to fix.
  • We need to figure out where to put and how to name the Ltac2 stuff.

Merge request reports