Zulip Chat Archive

Stream: general

Topic: n + 1 = 1 -> n = 0


view this post on Zulip Valéry Croizier (Jun 28 2020 at 15:17):

Hi, Lean and Zulip newbie there, not sure where to post exactly. Stuck on this calculation. How to prove it?

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 15:19):

Welcome! Is this what you want:

example (n : ) : n+1 = 1  n = 0 := nat.succ.inj

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 15:20):

In general you can find lemmas from the library with library_search:

import tactic

example (n : ) : n+1 = 1  n = 0 := by library_search

view this post on Zulip Valéry Croizier (Jun 28 2020 at 15:22):

Is this a reference to succ_inj in nat/lemmas ?

view this post on Zulip Johan Commelin (Jun 28 2020 at 15:22):

@Valéry Croizier To explain why nat.succ.inj proves this: n + 1 = succ n by definition, and 1 = succ 0, by definition.

view this post on Zulip Valéry Croizier (Jun 28 2020 at 15:23):

My Lean doesn't know library_search :(

view this post on Zulip Johan Commelin (Jun 28 2020 at 15:23):

Did you import tactic?

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 15:23):

I think nat.succ_inj was renamed to nat.succ.inj recently, so it may depend on what version of Lean you're using.

view this post on Zulip Valéry Croizier (Jun 28 2020 at 15:23):

I use VSCode and elan on WSL2.

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 15:24):

See #install for instructions on installing the latest version of Lean along with mathlib.

view this post on Zulip Valéry Croizier (Jun 28 2020 at 15:25):

My install is just a few days old. leanpkg.toml says leanprover-community/lean:3.16.4.

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 15:26):

Then example (n : ℕ) : n+1 = 1 → n = 0 := nat.succ.inj should work...

view this post on Zulip Valéry Croizier (Jun 28 2020 at 15:26):

Anyway, nat.succ.inj works, so thank you very much for you help.

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 15:27):

I recommend figuring out how to install mathlib so you can use library_search and other tactic goodies though. Let us know if you have any trouble.

view this post on Zulip Valéry Croizier (Jun 28 2020 at 15:35):

OK, library_search missed some imports mentioned in the doc. Nice. :slight_smile:


Last updated: May 11 2021 at 12:15 UTC