recurrence on fermat numbers

Stream: new members

[Peter Ross]

Hello I am new to Lean, and I would like help with proving a recurrence on the fermat numbers, which in latex is

\prod_{k=0}^{n-1} F_k = F_n-2

I tried to write it in Lean as

-- define a fermat number
def fermat_number (p : ℕ ) := 2^2^p +1
-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ ) : ∏ fermat_number x in range(n-1) = fermat_number n - 2 := begin
  sorry,
end

but the error said "unexpected token". I don't know how to solve this because I am new to using Lean, so I would appreciate it if anyone would help me.

[Ruben Van de Velde]

You're looking for something more like ∏ x in range(n-1), fermat_number x = fermat_number n - 2

[Eric Rodriguez]

you'll want open_locale big_operators too

[Yaël Dillies]

And range n instead of range (n - 1) most likely.

[Eric Rodriguez]

(natural number subtraction is annoying in Lean)

[Ruben Van de Velde]

import tactic

open_locale big_operators

-- define a fermat number
def fermat_number (p : ℕ) := 2^2^p +1

-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ) : ∏ x in finset.range n, fermat_number x = fermat_number n - 2 :=
begin
  sorry,
end

[Stuart Presnell]

To avoid the subtraction would it be better to write this?

lemma fermat_recurrence (n: ℕ) : ∏ x in finset.range (n+2), fermat_number x = fermat_number n :=
begin
  sorry,
end

[Kevin Buzzard]

Nonono, the brackets aren't there. It's (fermat_number n) +2

[Kevin Buzzard]

The formalisation is fine with the subtraction because the Fermat numbers are all >= 3.

[Kevin Buzzard]

I think that the correct way to avoid nat subtraction is not to use nat:

import tactic

open_locale big_operators

-- define a Fermat number as an integer
def fermat_number (p : ℕ) := (2 : ℤ) ^ 2 ^ p + 1

open finset

-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ) : ∏ x in range n, fermat_number x = fermat_number n - 2 :=
begin
  sorry,
end

[Ruben Van de Velde]

It appears to be true in lean:

import tactic

open_locale big_operators

-- define a fermat number
def fermat_number (p : ℕ) := 2^2^p +1

-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ) : ∏ x in finset.range n, fermat_number x = fermat_number n - 2 :=
begin
  simp only [fermat_number],
  induction n with n ih,
  { simp },
  { simp only [nat.succ_eq_add_one, finset.prod_range_succ, nat.succ_sub_succ_eq_sub,
      finset.prod_congr, ih],
    rw [mul_comm, ←nat.sq_sub_sq, pow_succ' _ n, pow_mul, one_pow], }
end

[Kevin Buzzard]

The proof is simpler if you use integers.

import tactic

open_locale big_operators

-- define a Fermat number as an integer
def fermat_number (p : ℕ) := (2 : ℤ) ^ 2 ^ p + 1

open finset

-- prove the recurrence on the Fermat numbers
lemma fermat_recurrence (n: ℕ) : ∏ x in range n, fermat_number x = fermat_number n - 2 :=
begin
  simp only [fermat_number], -- replace `fermat_number` by its definition
  induction n with d hd, -- induction on n
  { simp }, -- base case is easy
  { -- inductive step: use prod to n = prod to n-1 * n'th term and inductive hypo,
    rw [finset.prod_range_succ, hd],
    -- and then just tidy up
    ring_exp }
end

[Ruben Van de Velde]

Isn't it always :)

[Kevin Buzzard]

Furthermore I would argue that the moment you use subtraction you're saying "I am assuming subtraction makes sense hence I am assuming these things are integers". I would argue that the integer version is a more correct way of translating into Lean the meaning of the original question, as well as being easier to work with.