Zulip Chat Archive

Stream: new members

Topic: adding one


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Alex Kontorovich (Apr 11 2020 at 03:34):

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

view this post on Zulip 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 N\mathbf{N} isn't a subset of Z\mathbf{Z} I suggest they switch completely to Z\mathbf{Z}

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 06:46):

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

view this post on Zulip 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 N\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 ff and let's remember that it's a ring homomorphism (actually it's a semiring homomorphism, because N\mathbb{N} isn't a ring). So what you want to prove is cf(n)+c=cf(n+1)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)f(n+1)=f(n)+f(1). Second, f(1)=1f(1)=1. Third, c×(a+b)=ca+cbc\times(a+b)=ca+cb. Fourth, c×1=cc\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×(a+b)=ca+cbc\times(a+b)=ca+cb, and it uses mul_one, which is the statement that c×1=cc\times1=c. This reduces us to finding a way of telling Lean to use the fact that ff is a semiring homomorphism. But ff 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 ff in as far as it will go, and norm_cast is the corresponding "pull" tactic, attempting to write everything as f(?)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)=1f(1)=1 and f(a+b)=f(a)+f(b)f(a+b)=f(a)+f(b) and are using them to move ff as far in and out as it will go.

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 07:59):

In particular:

Isn't this just the distributive property?

It's four things!


Last updated: May 14 2021 at 00:42 UTC