dependent tuples with fin

Stream: new members

[Horatiu Cheval]

I am trying to use maps from fin n to represent dependently typed tuples. I am not sure whether this is good idea, but in any case, I got stuck at writing the following function, which should split a tuple of length (n + m) into one of length n and one of length m. The problem is, the tuples being dependent, I can't get the types to match. Any solutions to this? (I would also be happy with a recommendation on a better way to work with depend tuples, if that's the case).

import tactic

variables {α : Π {n : ℕ}, fin n → Type}
def finsplit {n m : ℕ} (f : Π i : fin (n + m), α i) : (Π i : fin n, α i) × (Π i : fin m, α i) :=
begin
  split,
  {
    intros i,
    let j : fin (n + m) := fin.cast_le (by linarith) i,
    let := f j,
    /-
    α : Π {n : ℕ}, fin n → Type,
    n m : ℕ,
    f : Π (i : fin (n + m)), α i,
    i : fin n,
    j : fin (n + m) := ⇑(fin.cast_le _) i,
    this : α j := f j
    ⊢ α i
    -/
    --this should be the result, but of course, the types don't match
  }
end

[Eric Wieser]

In a way docs#d_array is such a dependent tuple, but I don't think this function is in its API

[Eric Wieser]

Does lean even accept the type of that definition?

[Horatiu Cheval]

I get no complaints regarding the type signature. Why wouldn't it accept it?

[Horatiu Cheval]

d_array seems to have a pretty good API for fixed n, indeed not so much to relate tuples of different lengths. I think it's still better than to start from scratch.

[Eric Wieser]

Because \a is defined as indexed by fin (n+m) but you index it with fin n

[Eric Wieser]

Consider the tuples where the i'th item is a vector unit i

[Horatiu Cheval]

But those will be different \alphas, because it also takes an implicit natural argument. So the first is @\a (n +m) ... and the second is @\a n.

[Eric Wieser]

But you don't have anything to make those compatible

[Eric Wieser]

You need @\a (n + m) 0 = @\a n 0 and @\a (n + m) n = @\a m 0 etc for your definition to be possible

[Eric Wieser]

(but your explanation is correct for why there is not a type error after all)

[Horatiu Cheval]

Yeah, that's true, I didn't realize that. Thanks