Zulip Chat Archive

Stream: general

Topic: Proof of 0 ≠ 1

Adam Kurkiewicz (Mar 22 2018 at 11:41):

Hi guys, I'm sure I've asked this before, but I can't recall/ find my previous question.

How does one prove in lean that 1 ≠ 0?

I vaguely remember there was a lemma somewhere in the library, which allowed to magically prove these things, but can't find it either!

Moses Schönfinkel (Mar 22 2018 at 11:46):

It depends! Are these natural numbers? :)

Moses Schönfinkel (Mar 22 2018 at 11:47):

example : 0 ≠ 1 := dec_trivial

Mario Carneiro (Mar 22 2018 at 11:47):

zero_ne_one

Adam Kurkiewicz (Mar 22 2018 at 11:47):

Cheers guys! Yes, I meant natural numbers

Moses Schönfinkel (Mar 22 2018 at 11:52):

Right. In general, 1 ≠ 0is 1 = 0 → false and 1 = 0 as an assumption is untrue because of no_confusion (which appears to be a source of confusion!).

Moses Schönfinkel (Mar 22 2018 at 11:54):

@Mario Carneiro what on Earth, there's a zero_ne_one_class o_O?

Mario Carneiro (Mar 22 2018 at 11:55):

I think that class is misguided, since it doesn't play well with the rest of the hierarchy. It's one of those ossified things that will eventually go away when the alg hierarchy changes

Jakob von Raumer (Mar 22 2018 at 11:57):

I guess that's because it's only true for some rings...

Mario Carneiro (Mar 22 2018 at 12:09):

The problem is that it was intended as a mixin (who cares about an arbitrary structure with two unequal elements named 0 and 1 and no other laws?) but structure mixins don't work like this anymore

Adam Kurkiewicz (Mar 22 2018 at 12:16):

Ok, reading the source, zero_ne_one effectively boils down to

example : (0  ≠  1) :=  λ h, nat.no_confusion h

Is it generally true that given any two different terms, generated by applying different constructors or constructors in different order of some_inductive_type

inductive  some_inductive_type : Type
| constructor_a : ...
| constructor_b : ...

some_inductive_type.no_confusion will be able to distinguish between them?

Mario Carneiro (Mar 22 2018 at 12:17):

yes, that's its main purpose. The other purpose is that no_confusion, acting on the same constructors, gives back equalities of the constructor arguments

Adam Kurkiewicz (Mar 22 2018 at 12:22):

Thanks @Mario Carneiro and @Moses Schönfinkel , this is very clear now.

Moses Schönfinkel (Mar 22 2018 at 12:28):

No worries. It's basically information one recovers from the fact that constructors for any given inductive type are disjoint and injective.

Kevin Buzzard (Mar 22 2018 at 12:29):

I am confused about why Mario is surprised. 0 ne 1 is an axiom in some structures e.g. integral domains, which extend rings, so we surely expect to see these silly typeclasses for the same reason we see distribs. What am I missing?

Mario Carneiro (Mar 22 2018 at 12:29):

distrib is also a silly typeclass which doesn't serve its intended purpose

Kevin Buzzard (Mar 22 2018 at 12:33):

Is this something to do with the old structure command? Are these silly typeclasses going to disappear in Lean 4 perhaps?

Moses Schönfinkel (Mar 22 2018 at 12:34):

I am certain they'll be gone by the time Lean 7 is out.

Last updated: Dec 20 2023 at 11:08 UTC