Как объединить векторы, определенные как функции из конечных типов - PullRequest
Новая
       6

Как объединить векторы, определенные как функции из конечных типов

3 голосов
/ 01 ноября 2019

Я определил векторные типы для типа A, используя функции как fin n -> A. Я не могу придумать способ объединения векторов без прохождения индуктивных векторов.

Я использую определение конечных множеств: 

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

Затем я определяю векторы размером kкак функции fin k -> A.

Как я могу объединить такие векторы? 

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

Я пробовал сопоставление с образцом на n, но, похоже, тогда не признается, что i имеет тип fin m, тогда в случае 0.

Я думаю, это хорошо известное определение, но я не смог найти этот вариант векторов. Возможно, переход от этого типа к векторам в библиотеке Coq, объединение там, а затем возвращение - это вариант, но я хотел бы иметь более прямой подход.

1 Ответ

1 голос
/ 01 ноября 2019

Ключ в том, чтобы написать оператор анализа случая, чтобы решить, находится ли вход в составную функцию на стороне n или на стороне m: 

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.
...