adding one

Stream: new members

[Alex Kontorovich]

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]

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]

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]

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

[Kenny Lau]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

In particular:

Isn't this just the distributive property?

It's four things!