Switching (Fin n) to a general finite type in EuclideanSpace

Stream: new members

[Michael Novak]

I worked with a curve {n : Nat} (c : ℝ → EuclideanSpace ℝ (Fin n)}), but now I want to switch to the more general {ι : Type u} [Finite ι] (c : ℝ → EuclideanSpace ℝ ι), but I get some instance problems. For example I got somewhere the error failed to synthesize the instance of type class NormedAddCommGroup (EuclideanSpace ℝ ι). How should I deal with this?

[David Loeffler]

Does assuming [Fintype ι] rather than [Finite ι] help?

(That's just a guess though. If that doesn't solve your problem, I suggest you might want to post a #mwe [Minimal Working Example] of the issues you're encountering, so other community members can see better what the problem is.)

[Michael Novak]

David Loeffler said:

Does assuming [Fintype ι] rather than [Finite ι] help?

(That's just a guess though. If that doesn't solve your problem, I suggest you might want to post a #mwe [Minimal Working Example] of the issues you're encountering, so other community members can see better what the problem is.)

It solved the problems, thank you very much! Btw, what's the difference between Finite and Fintype?

[Kevin Buzzard]

One is a Prop, one is a Type.

[Michael Novak]

Kevin Buzzard said:

One is a Prop, one is a Type.

Thanks!

[Mirek Olšák]

Sight. On one hand, people are recommending using Finite, and then someone must use Fintype due to typeclass issues...

The difference is: Fintype can be used for evaluations / computations. I don't think such usecase makes much sense for PiLp.normedAddCommGroup where the type in question is anyway ENNReal which cannot be really evaluated. However, the trouble is that the definition of a norm uses a sum, which likes Fintype more.
If we want to compute a sum over a finite type, we need not only a theoretical guarantee that the type is finite (Finite) but also an actual enumeration of its elements.

By the way, the representation uses a Finset, so the order cannot be extracted from it, but sum works because its result provably do not depend on the order.

[Mirek Olšák]

Also, any Finite can be (noncomputably) converted into Fintype using Fintype.ofFinite. But because Fintype is not a Prop, kernel doesn't see it is always unique (although it is). This means using Fintype.ofFinite too much could lead to confusing typeclass conflicts too.