simp not idempotent

Stream: general

[Sebastien Gouezel]

#3103 has just been merged. At the last step, I had to fix a weird build failure, as the PR was not building when merged with master. A way to fix the problem was to have two identical calls to simp in a row -- instead, I went for a single dsimp, but still I would like to understand what is going on. You can try it at home by opening current mathlib, and going to line 590 in geometry/manifold/charted_space.lean. The line reads currently

have xs : x ∈ s, by { dsimp at hx, simp [s, hx] },

Initially, it was

have xs : x ∈ s, by { simp at hx, simp [s, hx] },

which fails with current mathlib (but used to work with a mathlib from a few days ago). What is funny is that

have xs : x ∈ s, by { simp at hx, simp at hx, simp [s, hx] },

works. With pp.all, I can't spot a difference before and after the first simp at hx. I guess it has something to do with metavariables. Can someone remind me of the magical command to have even more details than pp.all?

[Gabriel Ebner]

Fun experiment: add have hx := hx and put your cursor on the second hx. There are more metavariables than you might expect.

[Gabriel Ebner]

There is also a pretty-print option to this effect:

set_option pp.instantiate_mvars false

[Sebastien Gouezel]

What! In this proof, the first line starts with

  apply G.locality (λ x hx, _),

which I thought is completely equivalent to

  apply G.locality,
  intros x hx,

It turns out that they are not equivalent: with the first one, the types of x and hx are metavariables, and in the second one they are what they have to be.

Is this normal/expected/buggy?

(Before you ask, replacing apply with refine doesn't change this behavior)

[Sebastien Gouezel]

(Without the option set_option pp.instantiate_mvars false, the types of x and hx show up fine in the proof state).