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_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 (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