finite product of 1s is 1 - without range

Stream: new members

[Thomas Preu]

I'm working with finite sequences as below and want to prove (trivial) things about their product. I have seen proofs by induction for finite sums, but these sums were defined in terms of ranges. I naively tried to apply the same results in my context, but did not have any luck (there really was no reason that it works, I just desperately tried).

import Mathlib

example {m : ℕ} (oneSeq: Fin m → ℝ := (fun i ↦ 1)):
  1 = ∏ i in (Finset.univ), oneSeq i := by
    induction' m with n ih
    · simp
    · rw[Finset.prod_range_succ oneSeq n]

How would you deal with finite products of this form?

[Aaron Liu]

oh you can't prove this

[Aaron Liu]

there's no constraints on what oneSeq could be

[Aaron Liu]

the statement you've written says that every finite product of reals is one, which is false

[Aaron Liu]

the version for structure fields is on the common pitfalls page here

[Kenny Lau]

@Thomas Preu you need to define oneSeq on its own before the example

[Kenny Lau]

you can't define new things in the middle of stating a theorem

[Thomas Preu]

If I instead write

variable (m : ℕ)
def oneSeq: Fin m → ℝ := (fun i ↦ 1)
example {m : ℕ}:
  1 = ∏ i in (Finset.univ), oneSeq i := by
    induction' m with n ih
    · simp
    · rw[Finset.prod_range_succ oneSeq n]

then I get type mismatch errors and an error about what looks to me something along the lines that the naturals are not finite (which is clearly correct).
What other ways are there to set up such a statement, conditioned on not using range but Fin n?

[Kenny Lau]

that's not the error i get, you might be using an old version of mathlib

[Kenny Lau]

anyway after doing the translation

[Kenny Lau]

this is one of the common pitfalls

[Kenny Lau]

when you do variable (m : Nat), since you used round brackets, it's now an explicit argument, meaning that you have to input the value of m every time you call oneSeq

[Kenny Lau]

there's a way to see this from the error message

[Kenny Lau]

the error message says:

Type mismatch
  oneSeq i
has type
  Fin i → ℝ
but is expected to have type
  ℕ

[Kenny Lau]

see how you're expecting i to take the place of the Fin m argument, but somehow it still shows up, meaning that the Fin m argument has not been provided, meaning that the i is actually providing the argument before that, which is m

[Kenny Lau]

@Thomas Preu let me be clearer, you expect oneSeq to only take one input, but it actually takes two inputs, because m is the first argument it needs

[Kenny Lau]

Kenny Lau said:

the common pitfalls

the pitfall here is to think that "variable" means a commonly assumed thing that always sit in the background, whereas what it actually does is:

import Mathlib

variable (m : ℕ)
def oneSeq : Fin m → ℝ := (fun i ↦ 1)

/- is equivalent to: -/

def oneSeq (m : ℕ) : Fin m → ℝ := (fun i ↦ 1)

[Kenny Lau]

it never sits in the background, variable is just a way so that you don't have to type the common assumptions every time you type a new theorem, but it's still part of every new theorem/definition you type afterwards

[Thomas Preu]

Thanks for explaining, makes more sense now.
So if I try this

variable (m : ℕ)
def oneSeq: Fin m → ℝ := (fun i ↦ 1)
example {l : ℕ}:
  1 = ∏ i in (Finset.univ), oneSeq l i := by
    induction' l with n ih
    · simp
    · rw[Finset.prod_range_succ (oneSeq (l + 1)) n]

is it more reasonable?
And if so, what is the right way to argue about products defined using Fin instead of ranges?

[Kenny Lau]

Thomas Preu said:

Fin instead of ranges

the reason range is commonly used is that dependent types are bad...

[Kenny Lau]

using range allows you to focus on one function Nat -> A

[Kenny Lau]

imagine what the induction lemma would have to look like if you use Fin n

[Kenny Lau]

you need to write a product over Fin (m+1) in terms of a product over Fin m

[Kenny Lau]

which means that the statement itself will already involve two functions, one with type Fin (m+1) -> A and one with type Fin m -> A

[Kenny Lau]

in any case, the lemma exists and is called Fin.prod_univ_succ

[Kenny Lau]

and Fin.prod_univ_castSucc

[Kenny Lau]

these two variants exist for the two different ways you can extract a function Fin m -> A out of a function Fin (m+1) -> A

[Kenny Lau]

i.e. you either remove the first element in the vector, or the last element in the vector

[Kenny Lau]

![1,2,3,4,5] becomes either ![1,2,3,4] or ![2,3,4,5]

[Kenny Lau]

you'll notice that the function you get will particularly not be oneSeq m.

[Kenny Lau]

instead it will be some modification of oneSeq (m+1)

[Kenny Lau]

I hope this alone demonstrates to you the point of working with range instead of Fin.

[Aaron Liu]

Kenny Lau said:

you'll notice that the function you get will particularly not be oneSeq m.

It's a constant function so it will be defeq