# Zulip Chat Archive

## Stream: new members

### Topic: adding one

#### Alex Kontorovich (Apr 11 2020 at 02:11):

Hi, can anyone please help make this work? Thanks!

lemma z5 (c:α)(n0:ℕ ): (( c * ↑n0 + c )=( c * ↑( n0+1) )):= begin by library_search, sorry, end

#### Mario Carneiro (Apr 11 2020 at 02:44):

wow that's some bizarre formatting. I'm guessing you took this from a type mismatch error? This isn't a MWE because you haven't provided the variable for alpha, or more importantly what typeclasses it has

#### Mario Carneiro (Apr 11 2020 at 02:45):

the name of the function mapping nat to a general type is `nat.cast`

, so you should look for theorems like `nat.cast_succ`

#### Alex Kontorovich (Apr 11 2020 at 03:22):

I still can't get it to work if I replace \alpha by \R...? Isn't this just the distributive property?

#### Kenny Lau (Apr 11 2020 at 03:26):

import tactic universes u lemma z5 {α : Type u} [semiring α] (c : α) (n0 : ℕ): (c * n0 + c : α) = c * (n0 + 1 : ℕ) := begin push_cast, rw [mul_add, mul_one] end

#### Alex Kontorovich (Apr 11 2020 at 03:34):

Ah, that's what I was missing, push_cast. Many thanks!

#### Kevin Buzzard (Apr 11 2020 at 06:46):

In general there are norm_cast and push_cast which will help with these sorts of things, but when i see my students wrestling with the fact that $\mathbf{N}$ isn't a subset of $\mathbf{Z}$ I suggest they switch completely to $\mathbf{Z}$

#### Kevin Buzzard (Apr 11 2020 at 06:46):

Ooh Chris Hughes was right, LaTeX displays correctly on the Android app now

#### Kevin Buzzard (Apr 11 2020 at 07:54):

Alex Kontorovich said:

by library_search,

@Alex Kontorovich here's why `by library_search`

won't work.

As we all soon discover, in Lean $\mathbb{N}$ is not a subset of `α`

, whatever `α`

is, because distinct types are disjoint. Lean calls the map from nat to alpha `↑`

, which is notation for a function called `coe`

("coercion"). Let's just call it $f$ and let's remember that it's a ring homomorphism (actually it's a semiring homomorphism, because $\mathbb{N}$ isn't a ring). So what you want to prove is $cf(n)+c=cf(n+1)$. This is not the kind of theorem you would have, or want, in a library.

However it's now worth breaking down why this statement is true, i.e. writing down the maths proof. It's easiest to get from the right hand side to the left hand side. First, $f(n+1)=f(n)+f(1)$. Second, $f(1)=1$. Third, $c\times(a+b)=ca+cb$. Fourth, $c\times1=c$. All of *those* will be in the library! But `library_search`

only searches for the *exact statement* which you ask it about, it does not attempt to chain statements together in a logical way, that's the sort of thing that tactics like `simp`

or `cc`

do.

If you look at Kenny's proof, you see it uses `mul_add`

, which is $c\times(a+b)=ca+cb$, and it uses `mul_one`

, which is the statement that $c\times1=c$. This reduces us to finding a way of telling Lean to use the fact that $f$ is a semiring homomorphism. But $f$ is not just a random function, it is a coercion, and the `cast`

tactics are specifically designed to "do all of the simplifications you can using a coercion". The two tactics `norm_cast`

and `push_cast`

work in different directions; the "push" tactic pushes $f$ in as far as it will go, and `norm_cast`

is the corresponding "pull" tactic, attempting to write everything as $f(?)$. See:

import tactic example {α : Type} [semiring α] (n : ℕ) : ((n + 1 : ℕ) : α) = 37 := begin -- ⊢ ↑(n + 1) = 37 push_cast, -- ⊢ ↑n + 1 = 37 norm_cast, -- ⊢ ↑(n + 1) = 37 sorry end

Both tactics know that $f(1)=1$ and $f(a+b)=f(a)+f(b)$ and are using them to move $f$ as far in and out as it will go.

#### Kevin Buzzard (Apr 11 2020 at 07:59):

In particular:

Isn't this just the distributive property?

It's four things!

Last updated: Dec 20 2023 at 11:08 UTC