Zulip Chat Archive

Stream: new members

Topic: not 0 = 2


view this post on Zulip Bolton Bailey (Jan 13 2021 at 13:21):

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?

view this post on Zulip Mario Carneiro (Jan 13 2021 at 13:21):

dec_trivial will work for naturals, by norm_num works in general

view this post on Zulip Mario Carneiro (Jan 13 2021 at 13:22):

Or two_ne_zero' if you just want the exact theorem

view this post on Zulip Bolton Bailey (Jan 13 2021 at 13:26):

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

view this post on Zulip Damiano Testa (Jan 13 2021 at 13:28):

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

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 13:43):

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?

view this post on Zulip Mario Carneiro (Jan 13 2021 at 13:51):

well, two is an important number

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 13:55):

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.

view this post on Zulip Damiano Testa (Jan 13 2021 at 13:56):

Just for fun. This also works:

example : 37  0 := by library_search

view this post on Zulip Damiano Testa (Jan 13 2021 at 13:56):

This does look like the library of Babel...

view this post on Zulip Damiano Testa (Jan 13 2021 at 13:58):

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

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 14:05):

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?

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 14:05):

Oh -- is it using succ_ne_zero?

view this post on Zulip Damiano Testa (Jan 13 2021 at 14:13):

Yes, this is what it says:

Try this: exact 36.succ_ne_zero

view this post on Zulip Damiano Testa (Jan 13 2021 at 14:16):

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...

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 14:18):

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

view this post on Zulip Damiano Testa (Jan 13 2021 at 14:21):

Maybe we should define flat families of lemmas...

view this post on Zulip Kevin Buzzard (Jan 13 2021 at 15:06):

I think they might all be flat


Last updated: May 08 2021 at 03:17 UTC