Zulip Chat Archive
Stream: general
Topic: simp 0 < 1
Sean Leather (Sep 12 2018 at 14:11):
simp can't prove 0 < 1? Or, more specifically:
@has_lt.lt.{0} nat nat.has_lt (@has_zero.zero.{0} nat nat.has_zero) (@has_one.one.{0} nat nat.has_one)
Sean Leather (Sep 12 2018 at 14:14):
No, but simp [nat.pos_iff_ne_zero'] can.
Simon Hudon (Sep 12 2018 at 14:49):
What about norm_num?
Kevin Buzzard (Sep 12 2018 at 15:23):
what about rfl?
Kevin Buzzard (Sep 12 2018 at 15:24):
by refl
Kevin Buzzard (Sep 12 2018 at 15:24):
darn it, doesn't work!
Kevin Buzzard (Sep 12 2018 at 15:26):
le_refl 1 does
Kevin Buzzard (Sep 12 2018 at 15:26):
simp proves equalities, not inequalities
Sean Leather (Sep 12 2018 at 17:16):
simpproves equalities, not inequalities
@Kevin Buzzard Not strictly true. :slight_smile:
@[simp] theorem h : 0 < 1 := le_refl 1 example : 0 < 1 := by simp
Sean Leather (Sep 12 2018 at 17:16):
The reason I wanted simp to simplify this was to use it as a terminating tactic.
Reid Barton (Sep 12 2018 at 17:23):
simpa using zero_lt_one
Sean Leather (Sep 12 2018 at 17:55):
simpa using zero_lt_one
Oh, that's more descriptive than mine. And I see that zero_lt_one is in the core library and not @[simp]. I wonder if it would be worth making it @[simp] in mathlib.
Last updated: Dec 20 2023 at 11:08 UTC