Zulip Chat Archive

Stream: new members

Topic: int.succ_ne_self

Scott Morrison (Jul 21 2019 at 08:09):

Do we have
lemma int.succ_ne_self {x : ℤ} : x + 1 ≠ x := ...
?

Scott Morrison (Jul 21 2019 at 08:39):

Hopefully there is something less hideous than

lemma int.succ_ne_self {x : ℤ} : x + 1 ≠ x :=
begin
  intro h,
  replace h := congr_arg (λ n : ℤ, n - x) h,
  dsimp at h,
  rw [add_assoc, add_comm, neg_add_cancel_right, add_right_neg] at h,
  exact one_ne_zero h
end

Chris Hughes (Jul 21 2019 at 08:46):

(ne_of_lt (lt_add_one x)).symm

Mario Carneiro (Jul 21 2019 at 08:50):

ne_of_gt (lt_add_one x)

Kevin Buzzard (Jul 21 2019 at 12:16):

@Scott Morrison maybe you could expand library_search a bit ;-)

Jesse Michael Han (Jul 21 2019 at 12:54):

if you're feeling particularly lazy, λ _, by omega

Kevin Buzzard (Jul 21 2019 at 13:09):

Finally the correct answer :-)

Kevin Buzzard (Jul 21 2019 at 13:09):

Very nice

Kenny Lau (Jul 21 2019 at 13:10):

import tactic.linarith

lemma int.succ_ne_self {x : ℤ} : x + 1 ≠ x :=
λ H, by linarith

Kevin Buzzard (Jul 21 2019 at 13:28):

A new winner :-)

Kevin Buzzard (Jul 21 2019 at 13:28):

Oh no wait it's longer

Mario Carneiro (Jul 21 2019 at 22:09):

clearly we need to rename linarith to liathen

Kevin Buzzard (Jul 21 2019 at 22:10):

We should just have a tactic "schoolkid" which tries them all one after the other, and then just tell people that the other tactics are deprecated

Mario Carneiro (Jul 21 2019 at 22:11):

but then it should be called sk or else it won't win the golfing competitions

Marc Huisinga (Jul 21 2019 at 22:49):

for single symbol names i propose :work_in_progress: (\construction) for "will fix the bad perf of this later" or :biohazard: (\biohazard) for "run lean at own risk and always place pc in spent fuel pool for cooling beforehand"

Jesse Michael Han (Jul 21 2019 at 23:36):

while in vietnam, floris and i came up with this:

local notation `⟨╯°□°⟩╯︵┻━┻` := sorry

Last updated: Dec 20 2023 at 11:08 UTC