fintype instances for matrix notation

Stream: general

[Eric Wieser]

This doesn't work:

import data.fintype.basic

def holor {n : ℕ} (α : Type*) (ds : fin n → Type*) [∀ i, fintype (ds i)] := (Π i, ds i) → α

#check holor ℕ ![fin 2, fin 3, fin 4]

failed to synthesize type class instance for
⊢ Π (i : fin 1.succ.succ), fintype (![fin 2, fin 3, fin 4] i)

What can I do to teach lean how to find this instance?

[Alexander Bentkamp]

Why not like this?

def holor {n : ℕ} (α : Type*) (ds : fin n → ℕ) := (Π i, fin (ds i)) → α

[Kenny Lau]

wow we're stretching the limits of the vector notation aren't we

[Eric Wieser]

This works:

instance fintype_base {α : Type*} [fintype α] (i) : fintype (matrix.vec_cons α ![] i) :=
begin
  rw matrix.cons_val_fin_one,
  apply_instance,
end

instance fintype_step {α : Type*} {n : ℕ} {β : fin n → Type*} [fintype α] [∀ i, fintype (β i)] (i) : fintype (matrix.vec_cons α β i) :=
begin
  apply i.induction_on,
  { rw matrix.cons_val_zero, apply_instance },
  { intros i h, rw matrix.cons_val_succ, apply_instance}
end

[Eric Wieser]

@Alexander Bentkamp; There's no problem with that, but you'll note that docs#matrix allows arbitrary finite indices

[Eric Wieser]

Eg I can have a matrix whose columns are the (discrete) phases of the moon, and whose rows are the primary colors

[Alexander Bentkamp]

Ok, I see.

[Eric Wieser]

I'm saddened to find that this is not legal:

instance one_arg_base {α : Type*} {cls : Type* → Type*} [c : cls α] (i) : cls (matrix.vec_cons α ![] i)

[Yakov Pechersky]

Just making sure that you're aware of the holor part of library, which deals well with arbitrary type-level indexes. docs#holor

[Eric Wieser]

Except it doesn't - it uses integer indices

[Eric Wieser]

That's where this thread started from