# Zulip Chat Archive

## Stream: new members

### Topic: 1 is not equal to zero?

#### Jeremy Teitelbaum (Dec 31 2021 at 14:12):

I seem to have backed myself into a corner and cannot for the life of me figure out how to prove that 1 is not = to zero. Any hints?

#### Eric Rodriguez (Dec 31 2021 at 14:15):

some variation of docs#one_ne_zero; what type is `1`

?

#### Jeremy Teitelbaum (Dec 31 2021 at 14:20):

just a natural number.

#### Patrick Johnson (Dec 31 2021 at 14:20):

For natural numbers, it can be proved using docs#nat.succ_ne_zero.

```
example : (1 : ℕ) ≠ 0 := succ_ne_zero 0
```

But it is not true in general:

```
inductive T
| mk : T
instance : has_zero T := ⟨T.mk⟩
instance : has_one T := ⟨T.mk⟩
example : (1 : T) = 0 := rfl
```

#### Patrick Johnson (Dec 31 2021 at 14:21):

If you omit the type signature, you can't prove it.

#### Eric Rodriguez (Dec 31 2021 at 14:23):

fun fact: this is also a valid proof of `1 ≠ 0`

:

```
lemma one_ne_zero : (1 : nat) ≠ 0.
```

(you can `#print`

it to see what magic is going on here, and Kevin has a blog post on it)

#### Jeremy Teitelbaum (Dec 31 2021 at 14:25):

The actual situation I'm in is the following:

```
1 goal
h: 1 = 2
⊢ false
```

So I really want to prove 1 not = to 2. More generally I am experimenting with proving very concrete things like

```
def one_list := list.nil.cons 1
lemma two: ¬(one_list = (one_list.cons 2)) := sorry
```

and finding it surprisingly complicated.

#### Yaël Dillies (Dec 31 2021 at 14:25):

The `.`

is the most mystifying proof I've ever seen. I love it :stuck_out_tongue_closed_eyes:

#### Eric Rodriguez (Dec 31 2021 at 14:27):

Does `norm_num`

help Jeremy? Or `dec_trivial(!)`

?

#### Anne Baanen (Dec 31 2021 at 14:29):

Or `cases h`

#### Jeremy Teitelbaum (Dec 31 2021 at 14:33):

`cases h`

works like magic, but what did it do?

#### Kevin Buzzard (Dec 31 2021 at 14:38):

It gave you n goals, where n was the number of constructors of `eq`

which could possibly have made such a proof.

#### Kevin Buzzard (Dec 31 2021 at 14:40):

```
def one_list := list.nil.cons 1
def one_list' := [1] -- why not just use the notation for this?
example : one_list = one_list' := rfl
lemma two: ¬(one_list = (one_list.cons 2)) := dec_trivial
```

#### Kevin Buzzard (Dec 31 2021 at 14:45):

When `nat`

is constructed, Lean's elaborator knows that it can assume that constructors are injective and that distinct constructors give different terms. If you do `cases h`

when `h : 1 = 2`

then Lean thinks "well the only constructor for `eq`

is `eq.refl x : x = x`

so both `1`

and `2`

have to be equal to `x`

. Now `1 := succ zero`

and `2 := succ (succ zero)`

so for `x`

to exist, `succ (succ zero)`

and `succ zero`

have to be equal, but I know that succ is injective so this means `succ zero`

has to equal `zero`

but again I know this can't be true because zero isn't succ of anything, so this case can't happen"

#### Chris B (Dec 31 2021 at 14:46):

Under the hood, there are these auto-generated `no_confusion`

declarations that give you (or the `cases`

tactic) lower level access to the fact that constructors are injective and disjoint.

#### Kevin Buzzard (Dec 31 2021 at 14:46):

Is it the elaborator doing this when the `cases`

tactic is run?

#### Chris B (Dec 31 2021 at 14:47):

In Lean 4 it is, there might be c++ magic in Lean 3.

#### Kevin Buzzard (Dec 31 2021 at 14:48):

```
#check @nat.no_confusion
```

gives some statement which is hard to understand (it involves another type called `nat.no_confusion_type`

-- it was only when Chris Hughes and I sat down to figure out what was going on that I began to understand it and then wrote the blog post linked to above). If you right click on it, you might be surprised where you end up: the point is that this lemma is generated automatically by Lean when `nat`

is defined.

#### Chris B (Dec 31 2021 at 14:50):

It does look like `cases`

farms out to `no_confusion`

in lean 3 as well.

#### Jeremy Teitelbaum (Dec 31 2021 at 14:54):

I guess I didn't realize that "constructors are injective" and that "distinct constructors give different terms" were built in. So in the

inductive definition of the natural numbers, the injectivity of `succ`

is automatic?

Is there a section of TPIL I can read to understand more about the process you describe below?

Kevin Buzzard said:

When

`nat`

is constructed, Lean's elaborator knows that it can assume that constructors are injective and that distinct constructors give different terms. If you do`cases h`

when`h : 1 = 2`

then Lean thinks "well the only constructor for`eq`

is`eq.refl x : x = x`

so both`1`

and`2`

have to be equal to`x`

. Now`1 := succ zero`

and`2 := succ (succ zero)`

so for`x`

to exist,`succ (succ zero)`

and`succ zero`

have to be equal, but I know that succ is injective so this means`succ zero`

has to equal`zero`

but again I know this can't be true because zero isn't succ of anything, so this case can't happen"

#### Kevin Buzzard (Dec 31 2021 at 14:54):

They're not built in per se, they're proved automatically and added. You can `#print nat.no_confusion`

to see the proof that Lean automatically generated.

#### Kevin Buzzard (Dec 31 2021 at 14:55):

```
inductive foo
| bar : foo
| baz : foo → foo
#print foo.no_confusion -- you can see the term proof
#print prefix foo -- all the other goodies
```

#### Kevin Buzzard (Dec 31 2021 at 14:56):

`#print prefix foo`

shows you all the things Lean makes automatically when the user builds the inductive type `foo`

. The only things in that list without a definition are `foo`

, `foo.bar`

, `foo.baz`

and `foo.rec`

.

#### Kevin Buzzard (Dec 31 2021 at 15:01):

```
inductive foo
| bar : foo
| baz : foo → foo
namespace foo
example (x : foo) : ¬ bar = baz x :=
λ h, foo.no_confusion h
example (x : foo) : ¬ bar = baz x.
example (x y : foo) : baz x = baz y → x = y :=
λ h, foo.no_confusion h id
end foo
```

#### Kevin Buzzard (Dec 31 2021 at 15:05):

The dot thing is just an Easter egg, it's rarely useful in practice to mathematicians. It's all well and good having this fabulous equation compiler, but the equation compiler is a tool which works wonders on inductive types with more than one constructor, and we in practice hardly ever use these. Things like `group G`

, the type of group structures on a type `G`

, are strictly speaking inductive types, but they only have one constructor (the only way to make a group structure on G is to give the multiplication, identity, inverse, and proofs of the axioms). So you don't ever see this `no_confusion`

stuff in practice when you're e.g. in #FLT regular trying to prove FLT for regular primes.

#### Chris B (Dec 31 2021 at 15:09):

Jeremy Teitelbaum said:

I guess I didn't realize that "constructors are injective" and that "distinct constructors give different terms" were built in. So in the

inductive definition of the natural numbers, the injectivity of`succ`

is automatic?Is there a section of TPIL I can read to understand more about the process you describe below?

The type signature for `no_confusion_type`

is intimidating, but the underlying idea is pretty intuitive. You tell it some `p`

that you want, and give it a proof `h : a = b`

, and it looks at what `a`

and `b`

are.

For `0 = 0`

, you get nothing, since it's a trivial proof. For `S x = 0`

and `0 = S y`

, you immediately get a witness of `p`

, since your `h`

is a proof of false. For `S x = S y`

, you get back a term that will give you `p`

if it can be derived from `x = y`

.

#### Kevin Buzzard (Dec 31 2021 at 15:24):

Is there a section of TPIL I can read to understand more about the process you describe below?

I just picked it up by asking questions on here. I don't need a detailed understanding of this phenomenon to do the kind of mathematics I want to do so I didn't understand the details any more carefully. Someone like @Mario Carneiro will be able to tell you how everything works in Lean 3.

Last updated: Dec 20 2023 at 11:08 UTC