Need help understanding behaviour of Fin

Stream: new members

[Kevin Cheung]

I am a bit puzzled by what's happening in the code below:

import Mathlib.Data.Fin.Basic
-- import Mathlib.Data.Real.Sqrt

def z := (5 : Fin 3) -- Why does this work?
#check z -- This shows z : Fin 3.

def f (n : Fin 5) := n * 2
#reduce f (9 : ℤ) -- This gives a type error.

The error for the last line:

application type mismatch
  f 9
argument
  9
has type
  ℤ : Type
but is expected to have type
  Fin 5 : Type

Interestingly, if I replace the import with import Mathlib.Data.Real.Sqrt, there is no error anywhere. If anyone could shed some light on what's happening, it'll be greatly appreciated.

[Mario Carneiro]

Fin 3 has an OfNat instance in core, meaning that (5 : Fin 3) compiles (it wraps BTW), but there is no NatCast instance and IntCast doesn't even exist in core, so

#check fun n : Nat => (n : Fin 3)
#check fun n : Int => (n : Fin 3)

do not compile. Mathlib adds instances of these classes for any ring, and Fin 3 is a ring, so after importing enough of mathlib it does compile (it wraps)

[Kevin Cheung]

I see. Is there a way for disable this kind of casting (i.e. disallowing wrapping)?

[Kevin Cheung]

Should one use Finset.range 3 instead of Fin 3?

[Mario Carneiro]

In principle yes. The reason the OfNat A n class takes n as a parameter is so that you can specify separately that a type has only certain numbers, so you could make (3 : MyFin 5) compile and (5 : MyFin 3) not. But I don't think you can get rid of the existing instance on Fin itself without using attribute [-instance], which isn't a very long term solution since it's file-local

[Mario Carneiro]

Kevin Cheung said:

Should one use Finset.range 3 instead of Fin 3?

These have different types (one is a Finset and the other is a type), they aren't directly interchangeable. Maybe it would help to elaborate on what you need this for?

[Kevin Cheung]

I am wondering how to formulate something that involves

$$a_0,\ldots,a_n$$

wonder if it's better to use Finset.range or Fin for the indexing.

[Kevin Cheung]

For example,

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Sqrt

theorem my_cauchy_schwarz (n : ℕ) (a : Fin n → ℝ) (b : Fin n → ℝ) :
    (∑ i : Fin n, (a i) * (b i) ) ≤ Real.sqrt (∑ i : Fin n, (a i) ^ 2) * Real.sqrt (∑ i : Fin n, (b i) ^ 2) := by sorry

[Mario Carneiro]

that's actually still not enough information. The translation of sequences in traditional mathematics can be quite varied depending on what else is going on in the statement; often the conclusion is to use arbitrary finite indexing sets, sets of values or in some cases completely reformulating the statement (e.g. using filters)

[Mario Carneiro]

In your my_cauchy_schwarz example, I would be inclined to use an arbitrary sum over a Finset there

[Kevin Cheung]

Mario Carneiro said:

In your my_cauchy_schwarz example, I would be inclined to use an arbitrary sum over a Finset there

What would that look like, if you don't mind giving more details?

[Mario Carneiro]

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Sqrt

open BigOperators

theorem my_cauchy_schwarz (s : Finset α) (a : α → ℝ) (b : α → ℝ) :
    (∑ i in s, (a i) * (b i) ) ≤ Real.sqrt (∑ i in s, (a i) ^ 2) * Real.sqrt (∑ i in s, (b i) ^ 2) := by sorry

[Mario Carneiro]

this directly specializes to the statement you gave:

theorem my_cauchy_schwarz' (n : ℕ) (a : Fin n → ℝ) (b : Fin n → ℝ) :
    (∑ i : Fin n, (a i) * (b i) ) ≤ Real.sqrt (∑ i : Fin n, (a i) ^ 2) * Real.sqrt (∑ i : Fin n, (b i) ^ 2) :=
  my_cauchy_schwarz ..

[Kevin Cheung]

Interesting. Thank you.

[Kevin Cheung]

I always get confused between Finset.range and Fin.

[Mario Carneiro]

Finset A is a finite subset of elements of A. Finset.range n : Finset Nat is the collection of all numbers less than n, as a Finset of natural numbers. Fin n is an abstract type with n elements, which can be naturally embedded in Nat using the .val function

[Kevin Cheung]

Thank you for the explanation.

[Yaël Dillies]

Here is the mathlib statement for reference: docs#sum_mul_le_sqrt_mul_sqrt

[Kevin Cheung]

Mario Carneiro said:

this directly specializes to the statement you gave:

theorem my_cauchy_schwarz' (n : ℕ) (a : Fin n → ℝ) (b : Fin n → ℝ) :
    (∑ i : Fin n, (a i) * (b i) ) ≤ Real.sqrt (∑ i : Fin n, (a i) ^ 2) * Real.sqrt (∑ i : Fin n, (b i) ^ 2) :=
  my_cauchy_schwarz ..

What does .. in my_cauchy_schwarz .. do?

[Adam Topaz]

The .. means "put as many _ as needed"

[Kevin Cheung]

Hmm. In this case, I had to put four _ but my_cauchy_schwarz seems to take three arguments. Is one of them implicit here?

[Adam Topaz]

I only had to put 3:

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Sqrt

open BigOperators

theorem my_cauchy_schwarz (s : Finset α) (a : α → ℝ) (b : α → ℝ) :
    (∑ i in s, (a i) * (b i) ) ≤ Real.sqrt (∑ i in s, (a i) ^ 2) * Real.sqrt (∑ i in s, (b i) ^ 2) := by sorry

theorem my_cauchy_schwarz' (n : ℕ) (a : Fin n → ℝ) (b : Fin n → ℝ) :
    (∑ i : Fin n, (a i) * (b i) ) ≤ Real.sqrt (∑ i : Fin n, (a i) ^ 2) * Real.sqrt (∑ i : Fin n, (b i) ^ 2) :=
  my_cauchy_schwarz _ _ _

[Kevin Cheung]

There is some magic that I still don't understand. If we have s : Finset α, how does ∑ i in s get specialized into ∑ i : Fin n?

[Adam Topaz]

s gets specialized to \top : Finset (Fin n)

[Yaël Dillies]

∑ i : Fin n is notation for ∑ i in (univ : Finset (Fin n))

[Adam Topaz]

right, univ not top.

[Yaël Dillies]

Same thing soon (hopefully) :smile: :fingers_crossed:

[Kevin Cheung]

Adam Topaz said:

I only had to put 3:

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Sqrt

open BigOperators

theorem my_cauchy_schwarz (s : Finset α) (a : α → ℝ) (b : α → ℝ) :
    (∑ i in s, (a i) * (b i) ) ≤ Real.sqrt (∑ i in s, (a i) ^ 2) * Real.sqrt (∑ i in s, (b i) ^ 2) := by sorry

theorem my_cauchy_schwarz' (n : ℕ) (a : Fin n → ℝ) (b : Fin n → ℝ) :
    (∑ i : Fin n, (a i) * (b i) ) ≤ Real.sqrt (∑ i : Fin n, (a i) ^ 2) * Real.sqrt (∑ i : Fin n, (b i) ^ 2) :=
  my_cauchy_schwarz _ _ _

I see why. I had autoimplicit = false and declared α explicitly.

[Kevin Cheung]

Yaël Dillies said:

Same thing soon (hopefully) :smile: :fingers_crossed:

There is a difference between univ and top?

[Yaël Dillies]

They are definitionally equal (so Finset.univ = ⊤ can be proved by rfl), however they are not syntactically equal (so you can't use a lemma about one to rewrite the other)

[Kevin Cheung]

I see.