How to concatenate vectors defined as functions from finite types

Question

I've defined vector types on a type A by using functions as fin n -> A. I cannot come up with a way for concatenating the vectors without going through inductive vectors.

The definition of finite sets I am using is

Fixpoint fin (k : nat) : Type :=
  match k with
  | 0 => False
  | S k => option (fin k)
  end.

Then I define vectors of size k as functions fin k -> A.

How can I concatenate such vectors?

concat {A : Type} (n m : nat) (v1 : fin n -> A) (v2 : fin m -> A) (i : fin (n + m)) : A

I've tried pattern matching on n, but it doesn't seem to acknowledge then that i is of type fin m then in the 0 case.

I guess this is a well-known definition, but I couldn't find this variant of vectors. Maybe moving from this type to vectors in Coq's library, concatenate there, and then come back, is an option, but I would like to have a more direct approach.

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2019-11-01T19:26:48

The key is to write a case analysis operator to decide whether the input to the concatenated function is on the n side or the m side:

Fixpoint fin n :=
  match n with
  | 0 => Empty_set
  | S n => option (fin n)
  end.

Fixpoint case_fin n m : fin (n + m) -> fin n + fin m :=
  match n return fin (n + m) -> fin n + fin m with
  | 0 => fun i => inr i
  | S n => fun i =>
             match i with
             | None => inl None
             | Some j => match case_fin n m j with
                         | inl j => inl (Some j)
                         | inr j => inr j
                         end
             end
  end.

Fixpoint concat {A} n m (f : fin n -> A) (g : fin m -> A) (i : fin (n + m)) : A :=
  match case_fin n m i with
  | inl i => f i
  | inr i => g i
  end.

How to concatenate vectors defined as functions from finite types

1 Answers