Stream: general

Topic: int * real

James Arthur (Jul 01 2020 at 08:14):

I am trying to prove that for a sine function every multiple of $\pi$ is 0. This is my code thus far:

import tactic
import basic zero_lemmas
import data.real.basic
import data.complex.exponential

lemma sin_npi (n : ℤ) : sin (n * pi) = 0 :=
begin
{have H : 1 + (n-1) = n,
{ring},
rw [←H],
have H2 : (1 + (n-1)) * pi = pi + (n - 1) * pi,

sorry},

end


and get this error:

type mismatch at application
(1 + (n - 1)) * pi
term
pi
has type
ℝ
but is expected to have type
ℤ


I think it may be because I haven't imported the integers? As that was an issue before but I have tried to import:

import data.int.basic init.data.int.basic


but it still throws an error.

Johan Commelin (Jul 01 2020 at 08:15):

Lean sees 1 + (n - 1) and thinks you want to work with integers. You need to tell it explicitly that you want to view this as a real.

Johan Commelin (Jul 01 2020 at 08:16):

Telling lean to view x as a term of type Y can be done by writing (x : Y).

Johan Commelin (Jul 01 2020 at 08:17):

(This only works if someone explained to lean how to move x to this other type, this is called a coercion, or coe. Lean shows you that it coerced x by putting a tiny up-arrow before it.)

James Arthur (Jul 01 2020 at 08:20):

So I need something like this?

have H2 : ((1 + (n-1) : ℝ)) * pi = pi + (n - 1) * pi,


it works now but I fear that n is no longer an integer.

Kevin Buzzard (Jul 01 2020 at 08:20):

What do you mean "n is no longer an integer"? Things don't magically change their type. There are invisible functions in there. Look at the up arrows.

James Arthur (Jul 01 2020 at 08:23):

So even if I coerce $1 + (n-1)$ by using  ((1 + (n-1) : ℝ)) , n is still an integer just that whole statement is a real? I see the arrows, they mean that the variable is in a different field to the rest doesn't it?

Kevin Buzzard (Jul 01 2020 at 08:26):

n is an integer and this won't ever change. \u n is a real. Coerce as soon as you can. Note that \u (n+1) isn't the same as (\u n) + 1 because those are two different addition functions. Compatible, but different.

Kevin Buzzard (Jul 01 2020 at 08:27):

norm_cast will try and write everything as \u (all the maths) and push_cast will try and write everything as (all the maths applied to \u stuff)

James Arthur (Jul 01 2020 at 08:27):

OK, that's very useful to know. I have now used the  \u  in the have and produced  have H2 : (↑(1 + (n-1))) * pi = pi + (n - 1) * pi, . It now works, thanks!

Bryan Gin-ge Chen (Jul 01 2020 at 08:28):

By the way, I can't tell exactly since I don't know what's in basic and zero_lemmas, but there's something like sin_npi already proved in mathlib: src#real.sin_int_mul_pi

Patrick Massot (Jul 01 2020 at 08:29):

Elaborating on Bryan's comment: James, it's good that you tried to include the imports in the code you pasted, but they seem to refer to local files you have. The goal of this #mwe story is that people here can copy paste into their VScode and see your issue. Here we can't.

James Arthur (Jul 01 2020 at 08:33):

Sorry, I think the imports didn't explicitly import pi. I have worked everything out and moved my local imports away from the mathlib imports so that shouldn't happen again.

Last updated: May 11 2021 at 13:22 UTC