1 is not equal to zero?

Stream: new members

[Jeremy Teitelbaum]

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]

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

[Jeremy Teitelbaum]

just a natural number.

[Patrick Johnson]

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]

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

[Eric Rodriguez]

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]

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]

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

[Eric Rodriguez]

Does norm_num help Jeremy? Or dec_trivial(!)?

[Anne Baanen]

Or cases h

[Jeremy Teitelbaum]

cases h works like magic, but what did it do?

[Kevin Buzzard]

It gave you n goals, where n was the number of constructors of eq which could possibly have made such a proof.

[Kevin Buzzard]

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]

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]

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]

Is it the elaborator doing this when the cases tactic is run?

[Chris B]

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

[Kevin Buzzard]

#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]

It does look like cases farms out to no_confusion in lean 3 as well.

[Jeremy Teitelbaum]

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]

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]

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]

#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]

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]

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]

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_typeis 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]

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.