Slow coercion from `Fin n` to `Fin m`

Stream: mathlib4

[Tomas Skrivan]

Coercing Fin 10 to Fin 5 is really slow. This problem could be related to the slow coercion from primes to reals, previous topic.

import Mathlib

set_option profiler true

--set_option trace.Meta.synthInstance true
example (a : Fin 10): CoeT (Fin 10) a (Fin 5) := by infer_instance

Takes roughly 350ms on my machine

The issue is the instCoeHTCT instance

instance [CoeTail β γ] [CoeHTC α β] : CoeHTCT α γ where coe a := CoeTail.coe (CoeHTC.coe a : β)

which takes forever to figure out that β should be Nat

-- slow
def isnt1 : CoeHTCT (Fin 10) (Fin 5) := by infer_instance

-- fast
def inst2 : CoeHTCT (Fin 10) (Fin 5) := by apply instCoeHTCT (β:=Nat)

While chasing down the right β there is really wild stuff going on, like trying:

apply @InfTopHomClass.toInfHomClass to InfHomClass (Fin 10) ?m.142755 ?m.142756

I do not really understand mathlib's stack of classes and instances so I have no clue what to do about this.

[Yaël Dillies]

Do not use this coercion. It's quite bad.

[Yaël Dillies]

It sens a : Fin m to ↑(a.val) : Fin n, for any m and n ≠ 0. Mathematically, that's quite bad.

[Tomas Skrivan]

I agree that I should use something else, but is that reason for this coercion to be that slow?

(I'm trying to write down simple convolution

def conv (x : Fin n → ℝ) (w : Fin m → ℝ) := fun (i : Fin n) => ∑ j, w j * x (i - j)

but maybe I should rather do something like

def conv (x : Fin n → ℝ) (w : ℤ[-m,m] → ℝ) := fun (i : Fin n) => ∑ j, w j * x (i - j)

where ℤ[-m,m] = {a : ℤ // -m ≤ a ∧ a ≤ m})

[Yaël Dillies]

It sounds like you could use ℤ →₀ ℝ?

[Tomas Skrivan]

I'm writing a program, using ℤ →₀ ℝ is not on the table as it would be too slow.

[Damiano Testa]

I am not sure if this is really serious, but there is docs#LaurentPolynomial and I think that, informally, what you are doing is equivalent to taking the zero-th coefficient of $f(t) g(t^{-1})$, with f g : LaurentPolynomial ℝ.

Ah, your actual motivation might rule this out!

[Tomas Skrivan]

You are probably right, if

g t = ∑ i : ℕ, w i * t^n
f t = ∑ i : ℕ, x i * t^n

Then I'm trying to compute the ith coeficient of the Laurent series of $f(t)g(t^{-1})$, but that does not help me to write an efficient program :)

[Martin Dvořák]

Speaking of Fin coercions, I incidentally just added this function to my code:

private def liftFin : Fin 2 → Fin 8 :=
  fun ⟨a, ha⟩ => ⟨a, (Nat.lt_trans ha (show 2 < 8 by decide))⟩

The only objective is to change (0 : Fin 2) to (0 : Fin 8) and (1 : Fin 2) to (1 : Fin 8).
Is it a bad practice? I mean the implementation (the name surely is).

[Eric Wieser]

That's docs#Fin.castLE