Surprising error when using simp

Stream: general

[Gabriel Ebner]

import data.nat.basic
import data.nat.pow

example (n : ℕ) : 3 ∣ (2 ^ (2 * n + 1) + 1) :=
begin
  transitivity,
  swap,
  simp
  -- goals accomplished 🎉
end

[Kevin Buzzard]

Mario always warns of metavariables in goals.

[Gabriel Ebner]

Yes, I believe that's indeed what's going wrong here. simp assigns the metavariable to 1, but doesn't propagate this assignment. And refl can then afterwards assign the same metavariable to 0.

[Damiano Testa]

Just for laughs, this shows the same behaviour:

example : 0 ∣ 2 :=
begin
  transitivity,
  swap,
  simp,
  -- goals accomplished 🎉
end

[Daniel Selsam]

It looks like it just forgets to update the tactic state's mctx: https://github.com/leanprover-community/lean/blob/master/src/library/tactic/simplify.cpp#L1262

[Daniel Selsam]

^ or forgets to not assign regular metavariables, depending on your point of view

[Eric Wieser]

This reminds me of when I tried a patch to preserve metavariables resolved by conv, but if I tried to preserve them in the lean code I got a segfault from the C++

[Eric Wieser]

Maybe it wasn't a segfault; the reversion PR was https://github.com/leanprover-community/lean/pull/485/files