coq – 依赖类型：向量向量

我是依赖类型的新手(尽管他们有很大的不同,我正在尝试Idris和Coq).

我试图表达以下类型：给定类型T和k nats n1,n2,… nk的序列,由k个k序列组成的类型,其长度分别为n1,… nk.

即,k个矢量的矢量,其长度由参数给出.
这可能吗？

您可以使用异构列表执行此操作,如下所示.

Require Vector.
Require Import List.
Import ListNotations.

Inductive hlist {A : Type} (B : A -> Type) : list A -> Type :=
| hnil : hlist B []
| hcons : forall a l,B a -> hlist B l -> hlist B (a :: l).

DeFinition vector_of_vectors (T : Type) (l : list nat) : Type :=
  hlist (Vector.t T) l.

然后,如果l是您的长度列表,则类型vector_of_vectors将使用您描述的类型.

例如,我们可以构造一个vector_of_vectors bool的元素[2; 0; 1]：

Section example.
  DeFinition ls : list nat := [2; 0; 1].

  DeFinition v : vector_of_vectors bool ls :=
    hcons [false; true]
          (hcons []
                 (hcons [true] hnil)).
End example.

此示例对您可以设置的向量使用一些符号：

Arguments hnil {_ _}.
Arguments hcons {_ _ _ _} _ _.

Arguments Vector.nil {_}.
Arguments Vector.cons {_} _ {_} _.

Delimit Scope vector with vector.
Bind Scope vector with Vector.t.
Notation "[ ]" := (@Vector.nil _) : vector.
Notation "a :: v" := (@Vector.cons _ a _ v) : vector.
Notation " [ x ] " := (Vector.cons x Vector.nil) : vector.
Notation " [ x ; y ; .. ; z ] " :=  (Vector.cons x (Vector.cons y .. (Vector.cons z Vector.nil) ..)) : vector.

Open Scope vector.