NotEqualSign

Stream: general

[James Arthur]

I'm relatively new to LEAN and I'm trying to prove that $succ(x)\neq0$, I get my goal of $succ(x)\neq0$ and am a bit stuck from there. I have tried cases and induction.

[Yury G. Kudryashov]

#mwe

[James Arthur]

It's from the natural numbers game, but I assume just add the link as it suggests:

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=9

[Jeremy Avigad]

This will work:

open nat

example (n : ℕ) : succ n ≠ 0 :=
begin
  intro h,
  contradiction
end

What is going on is that the natural numbers are an inductively defined type, and Lean knows that the constructors (in this case, zero and succ) are disjoint. That is one of the things the contradiction tactic will look for.

[James Arthur]

Jeremy Avigad said:

This will work:

open nat

example (n : ℕ) : succ n ≠ 0 :=
begin
  intro h,
  contradiction
end

What is going on is that the natural numbers are an inductively defined type, and Lean knows that the constructors (in this case, zero and succ) are disjoint. That is one of the things the contradiction tactic will look for.

Thankyou, although I assume this isn't the intended solution, it works!

[Jalex Stark]

I imagine the intended solution starts like this (and may give you some extra insight into why jeremy's solution works

open nat

example (n : ℕ) : succ n ≠ 0 :=
begin
  cases n,
end

[Jason KY.]

If you don't want to use contradiction you can use the axiom zero_ne_succ

intro h,
apply zero_ne_succ a,
rwa h

[Mario Carneiro]

@Jalex Stark there is no need to cases on n as it is already a successor in the theorem

[Mario Carneiro]

intro h, cases h would be my recommendation

[Mario Carneiro]

It's also a place for my favorite trick:

example (n : ℕ) : succ n ≠ 0.

[Mario Carneiro]

the no proof proof

[Bhavik Mehta]

Can you explalin what . means? In general as well as here

[Mario Carneiro]

it's a 0-ary use of the equation compiler

[Mario Carneiro]

in general it ends a definition, which is almost always optional but not here

[James Arthur]

Thankyou all!

[Mario Carneiro]

(usually the end of a definition is signaled by the next command keyword, e.g. the def/theorem on the next line)

[Kevin Buzzard]

I love it when he comes out with those dot proofs.

[Kevin Buzzard]

It is ultimate golf.