Zulip Chat Archive

Stream: general

Topic: Surprising error when using simp


Gabriel Ebner (Jul 06 2021 at 09:50):

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 (Jul 07 2021 at 10:14):

Mario always warns of metavariables in goals.

Gabriel Ebner (Jul 07 2021 at 11:09):

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 (Jul 07 2021 at 11:12):

Just for laughs, this shows the same behaviour:

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

Daniel Selsam (Jul 07 2021 at 20:06):

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 (Jul 07 2021 at 20:18):

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

Eric Wieser (Jul 07 2021 at 21:15):

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 (Jul 07 2021 at 21:16):

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


Last updated: Dec 20 2023 at 11:08 UTC