Beginner question: inequality

Stream: new members

[Chu-Wee Lim]

Hi. What is the preferred way to prove something like: 0 ≠ 1? Right now I'm using:

example : 0 ≠ 1 :=
begin
intro h, injection h
end

I'm asking because there seems to be multiple ways of doing the same thing in Lean. Some may introduce me to some new tactics.

[Johan Commelin]

@Chu-Wee Lim This very much depends on what 0 and 1 are. Are the natural numbers or integers or real numbers?

[Alex J. Best]

There are many ways, if I saw this or something similar I'd write example : 0 \ne 1 := dec_trivial to use the fact naturals are decidable, however this lemma is in core (so you can apply it...) but the core proof is here https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/library/init/data/nat/lemmas.lean#L47

[Chu-Wee Lim]

In my code above, natural numbers.

[Johan Commelin]

The proof of this fact is usually called zero_ne_one. Here is mathlibs proof for real numbers: https://github.com/leanprover-community/mathlib/blob/b5b40c749f2f581778e5d72907eca1aa663962b1/src/data/real/cau_seq_completion.lean#L120

[Rob Lewis]

The generic way to do it is the norm_num tactic.

[Andrew Ashworth]

i can never remember the name of lemmas unless i look it up. for stuff like this that is straightforward, you can use example : 0 ≠ 1 := λ h, nat.no_confusion h

[Mario Carneiro]

Aha, this lets me use my trick for the shortest proof ever:

example : 0 ≠ 1.

[Johan Commelin]

That's the way Kevin would have wanted to prove 1 ≠ 2 on his example sheets on quadratic equations...

[Andrew Ashworth]

that makes my lean server crash when I apply it to arbitrary lemmas

[Bryan Gin-ge Chen]

Can you give a MWE of the crash? It might be something fixable in 3.5.0c.

[Chu-Wee Lim]

Aha, this lets me use my trick for the shortest proof ever:

example : 0 ≠ 1.

How does this work? I've never seen the period in Lean before.

[Keeley Hoek]

The period is sometimes required to terminate a statement if it is ambiguous whether the statement ends there or not (lean will otherwise proceed parsing, probably encounter the lemma beginning the next statement, interpret the result as a function application and throw an error)

[Keeley Hoek]

As for why it works... :shrug: Maybe lean tries dec_trivial if you omit the definition of an example?

[Keeley Hoek]

Ah, got it

[Keeley Hoek]

Not is just shorthand for a map to false, so we are just defining a function to false using an empty inductive definition (the match-like syntax)

[Rob Lewis]

0 ≠ 1 expands to 0 = 1 → false. In general, you can define functions (or prove implications) using the equation compiler, e.g.

example (A B : Prop) : A → B
| ha := _

The equation compiler is more powerful than this example. If the variables are coming from an inductive type (A), you can destruct them using this syntax.

example (A B : Prop) : (A ∨ B) → false
| (or.inl ha) := _
| (or.inr hb) := _

0 = 1 is an inductive proposition. There's only one way to prove an equality, refl a : a = a. But this can never be applied to prove 0 = 1, since they're built with different constructors for nat. The equation compiler figures out that this case is impossible, so you're left with zero applicable cases for the pattern match.

[Wojciech Nawrocki]

Adding a newline after example : 0 ≠ 1. seems to crash the Lean 3.5.0 (nightly-2019-10-01) server. I'll try to MWE later.

[Bryan Gin-ge Chen]

Happens to me in 3.4.2 as well, but I can't get it to trigger from the command-line.