Converting ordered tuple to fin n → α

Stream: new members

[Martin C. Martin]

Given def tuple (n : ℕ) := fin n → Type u, how do ai convert e.g. (5, 23, 99) to a tuple 3?

[Yakov Pechersky]

![5, 23, 99]

[Martin C. Martin]

That's not working for me. I'm in Lean 3, is that a Lean 4 construct?

[Martin C. Martin]

I get that ! expects a bool.

[Kevin Buzzard]

It's Lean 3 and it needs an import. Something like data.vector.notation or something?

[Kevin Buzzard]

import data.matrix.notation

#check ![1,2,3] -- works

[Eric Wieser]

Lean 4 has it too, with the same import

[Martin C. Martin]

Thanks, that works! My definition of tuple should be:

def tuple {α : Type*} (n : ℕ) := fin n → α

[Martin C. Martin]

.

[Eric Wieser]

You'll have an easier time if you put @[reducible] on that

[Martin C. Martin]

How do I expand the notation? For example:

import data.matrix.notation

example : ![3, 5] ≠ ![5, 3] :=
begin
  intro h,
  rw matrix.cons_val_zero at h,
  sorry
end

[Martin C. Martin]

(The rw fails saying there's no instance of matrix.vec_cons in h.)

[Eric Wieser]

That's not what the error says, it says it can't find matrix.vec_cons ?m_3 ?m_4 0

[Eric Wieser]

Which is true, h is of the form matrix.vec_cons ?m_3 ?m_4 = _ without a 0 anywhere

[Eric Wieser]

rw function.ne_iff, makes good progress on the original goal

[Martin C. Martin]

Ah, thanks!

[Eric Wieser]

And dec_trivial can just solve the original goal immediately

[Martin C. Martin]

I hadn't heard of dec_trivial before. Thanks.

[Martin C. Martin]

The type of (3, 5) is ℕ × ℕ. The type of (3, 5, 23) is ℕ × ℕ × ℕ. Is there an existing type for ℕ^n?

[Eric Wieser]

I assume you're not looking for fin n → ℕ, since that's in the title of the thread already

[Eric Wieser]

What type do you want for ℕ^0?

[Martin C. Martin]

I'm wondering what it would take to create a function from ℕ^n to fin n → ℕ.

[Martin C. Martin]

So I could say (3, 5).tup instead of ![3, 5]. The custom function from ℕ^n would probably be worse, but I just want to understand what's involved.

[Eric Wieser]

You can write your own:

@[reducible] def nprod (α : Type*) : ℕ → Type*
| 0 := unit
| 1 := α
| (n + 2) := α × nprod (n + 1)

example : (ℕ × ℕ × ℕ) = nprod ℕ 3 := rfl

but I wouldn't recommend it

[Eric Wieser]

Because now you have to deal with three different cases depending on the length of n, rather than just one or two

[Martin C. Martin]

Ok, thanks. I figured if the type didn't already exist, which it seems it doesn't, then that's probably because there are better ways to accomplish the same goal. :)

[Eric Wieser]

This seems to work slightly better as a definition:

def nprod (α : Type*) (n : ℕ) : Type* :=
begin
  cases n,
  { exact unit },
  induction n with n ih,
  { exact α },
  { exact α × ih },
end

#check ((1, 2, 3) : nprod ℕ 3)

[Eric Wieser]

And then you can write what you asked for as

def nprod.to_fin {α : Type*} : Π {n}, nprod α n → (fin n → α)
| 0 x := ![]
| 1 x := ![x]
| (n + 2) (x, xs) := matrix.vec_cons x (@nprod.to_fin (n + 1) xs)

#eval nprod.to_fin (show nprod ℕ 3, from (1, 2, 3))

[Eric Wieser]

Here's one more way

class has_to_tuple (α : Type*) (n : out_param ℕ) (β : out_param Type*) :=
( to_fun : α → fin n → β)

instance has_to_tuple.base (α : Type*) : has_to_tuple α 1 α :=
{ to_fun := λ a, ![a] }

instance has_to_tuple.prod (α β : Type*) (n : ℕ) [has_to_tuple β n α] : has_to_tuple (α × β) (n + 1) α :=
{ to_fun := λ a, matrix.vec_cons a.1 (has_to_tuple.to_fun a.2) }

#eval has_to_tuple.to_fun (1, 2, 3)  -- ![1, 2, 3]

If you never want to refer to nprod for a variable n, then this should be enough

[Martin C. Martin]

Oh interesting, I haven't used the class stuff much, and hadn't thought of it as an alternative to definition by cases. Cheers.

[Eric Wieser]

Classes are the tool you need if the thing you want to case on is the type itself