Zulip Chat Archive

Stream: new members

Topic: Odd simp? behavior

Michael Levenkov (May 18 2022 at 04:06):

I have found some odd behavior with the simp? tactic. In certain cases, it closes the goal, but the "Try this" simp only command it suggests doesn't actually work to close the goal. A MWE is below. Is this a bug or just something strange happening on my end? On the latest version of mathlib if that matters.

import data.real.basic

example : 0 + 0 ^ 2 = 0 :=
  -- simp? suggests simp only [add_zero, eq_self_iff_true, zero_pow'],
  -- which does not close the goal
  -- squeeze_simp suggests simp only [zero_pow', ne.def, bit0_eq_zero,
  -- nat.one_ne_zero, not_false_iff], which does close the goal

Johan Commelin (May 18 2022 at 05:19):

Unfortunately simp? is buggy. squeeze_simp is slower, but much more reliable.

Johan Commelin (May 18 2022 at 05:20):

I don't know how to fix simp? and I think everybody is just hoping that in a few months we'll be using the Lean 4 version where everything will "Just Work".

Last updated: Dec 20 2023 at 11:08 UTC