not 0 = 2

Stream: new members

[Bolton Bailey]

Very embarrased to ask this, but I've searched the documentation for an hour and cannot find an answer to this very simple question. How does one prove a fact such as \not 0 = 2 for naturals?

[Mario Carneiro]

dec_trivial will work for naturals, by norm_num works in general

[Mario Carneiro]

Or two_ne_zero' if you just want the exact theorem

[Bolton Bailey]

Great thanks. How come library_search does not seem to work for this?

[Damiano Testa]

It may have to do with the fact that the lemma is 2 \neq 0. This works:

example : 2 ≠ 0 := by library_search

as does

example : 0 ≠ 2 := by library_search

[Kevin Buzzard]

Why would a library have a proof of \not 0 = 2? Do you want it to have a proof that 2 is not 37? It's a finite library. This is the sort of thing you should prove with a calculation right?

[Mario Carneiro]

well, two is an important number

[Kevin Buzzard]

One has to stop somewhere though. Is three an important number?

My point is really that it's important to learn early on what one expects in a library and what one is expected to deal with using results in a library and tactics.

[Damiano Testa]

Just for fun. This also works:

example : 37 ≠ 0 := by library_search

[Damiano Testa]

This does look like the library of Babel...

[Damiano Testa]

I think that we can prove by induction that library_search contains the proof of all lemmas n.succ \neq 0.

[Kevin Buzzard]

Damiano Testa said:

Just for fun. This also works:

example : 37 ≠ 0 := by library_search

Oh yeah, I put that one in because I deemed it important. Wait -- what? What does by show_term {library_search} say?

[Kevin Buzzard]

Oh -- is it using succ_ne_zero?

[Damiano Testa]

Yes, this is what it says:

Try this: exact 36.succ_ne_zero

[Damiano Testa]

I guess that this means that the library is finite in the sense that you can only check out a finite number of lemmas from it, but the number of lemmas that it contains is not finite...

[Kevin Buzzard]

this is a lemma with a variable input so really it's a family of lemmas

[Damiano Testa]

Maybe we should define flat families of lemmas...

[Kevin Buzzard]

I think they might all be flat