Внедрение векторов в Coq

Question

Внедрение векторов в некоторых зависимых языках (например, Idris) довольно просто. Согласно example on Wikipedia:

import Data.Vect 

%default total 

pairAdd : Num a => Vect n a -> Vect n a -> Vect n a 
pairAdd Nil  Nil  = Nil 
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys 

(Обратите внимание, как Идрис совокупности проверка автоматически делает вывод, что добавление Nil и не- Nil векторов представляет собой логическая невозможность.)

Я пытаюсь реализовать эквивалентную функциональность в Coq , используя реализацию пользовательского вектора, хотя и очень похожий на тот, представленном в официальном Coq libraries:

Set Implicit Arguments. 

Inductive vector (X : Type) : nat -> Type := 
    | vnul : vector X 0 
    | vcons {n : nat} (h : X) (v : vector X n) : vector X (S n). 
    Arguments vnul [X]. 

Fixpoint vpadd {n : nat} (v1 v2 : vector nat n) : vector nat n := 
    match v1 with 
    | vnul => vnul 
    | vcons _ x1 v1' => 
    match v2 with 
    | vnul => False_rect _ _ 
    | vcons _ x2 v2' => vcons (x1 + x2) (vpadd v1' v2') 
    end 
    end. 

Когда Coq пытается проверить vpadd, он дает следующее сообщение об ошибке:

Error: 
In environment 
vpadd : forall n : nat, vector nat n -> vector nat n -> vector nat n 
[... other types] 
n0 : nat 
v1' : vector nat n0 
n1 : nat 
v2' : vector nat n1 
The term "v2'" has type "vector nat n1" while it is expected to have type "vector nat n0". 

Обратите внимание, что я использую False_rect указать невозможно случай, в противном случае проверка совокупности не будет проходить. Тем не менее, по какой-то причине контролером типа не удается объединить n0 с n1.

Что я делаю неправильно?

Answer 1

Невозможно реализовать эту функцию так легко в простом Coq: вам необходимо переписать свою функцию, используя диаграмму конвоев . Недавно было опубликовано сообщение similar question. Идея заключается в том, что вы должны сделать свой match вернуть функцию для того, чтобы распространить соотношение между показателями:

Set Implicit Arguments. 

Inductive vector (X : Type) : nat -> Type := 
    | vnul : vector X 0 
    | vcons {n : nat} (h : X) (v : vector X n) : vector X (S n). 
    Arguments vnul [X]. 

Definition vhd (X : Type) n (v : vector X (S n)) : X := 
    match v with 
    | vcons _ h _ => h 
    end. 

Definition vtl (X : Type) n (v : vector X (S n)) : vector X n := 
    match v with 
    | vcons _ _ tl => tl 
    end. 

Fixpoint vpadd {n : nat} (v1 v2 : vector nat n) : vector nat n := 
    match v1 in vector _ n return vector nat n -> vector nat n with 
    | vnul =>   fun _ => vnul 
    | vcons _ x1 v1' => fun v2 => vcons (x1 + vhd v2) (vpadd v1' (vtl v2)) 
    end v2.