我试图在矢量上定义rev函数，它的大小嵌入其中，我不知道如何在其上定义rev函数。
下面是我的类型定义:Inductive vect {X : Type} : nat -> Type -> Type
:= Nil : vect 0 X
| Cons : forall n, X -> vect n X -> vect (S n) X
.
我在上面定义了一些有用的函数:
Fixpoint app {X : Type} {n m : nat} (v1 : vect n X) (v2 : vect m X)
: vect (n + m) X :=
match v1 with
| Nil => v2
| Cons _ x xs => Cons _ x (app xs v2)
end.
Fixpoint fold_left {X Y : Type} {n : nat} (f : Y -> X -> Y) (acc : Y) (v : vect n X)
: Y :=
match v with
| Nil => acc
| Cons _ x xs => fold_left f (f acc x) xs
end.
现在，我想定义rev。我的第一个尝试是通过fold_left，但结果是完全失败的。
Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X :=
fold_left (fun {X : Type} {k : nat} (acc : vect k X) (x : X) => x ::: acc) {{ }} v.
我不理解错误Error: The type of this term is a product while it is expected to be a sort. .
我的第二次尝试几乎是好的，但Coq看不到&;S n = (n + 1)&;我不知道怎么跟Coq说。
Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X :=
match v in (vect n X) return (vect n X) with
| Nil => Nil
| Cons _ x xs => app (rev xs) {{ x }}
end.
错误是The term "app (rev X n0 xs) {{x}}" has type "vect (n0 + 1) X" while it is expected to have type "vect (S n0) X"
如果您对coq代码有任何其他注释，请不要犹豫。
Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X := fold_left (fun {X : Type} {k : nat} (acc : vect k X) (x : X) => Cons x acc) Nil v.
fold_left的第一个显式参数必须具有?1 -> ?2 -> ?1形式的类型，即两个参数的函数，其返回类型与第一个参数相同。"product"是函数的Coq术语。您正在传递一个形式为fun (X:Type) b c d => …的术语，因此?1是Type，并且术语fun c d => …(显然具有产品类型)必须具有给定上下文的?类型，因此它必须具有Type类型，即它必须是一个排序。
如果你试图修复这个问题，你会意识到你的fold_left函数在这里不起作用:你需要在迭代过程中改变向量的长度，但是fold_left的迭代器参数在迭代过程中有一个常量类型。对于fold_left函数，如果从Nil(长度为0的向量)累加器开始，最终将得到相同类型的结果，也是长度为0的向量。
我还没有想过如何定义一个更通用的迭代器来让你定义rev，但我确信这是可能的。
关于你的第二次尝试，vect (n0 + 1) X和vect (S n0) X的问题是它们不是同一类型，因为n0 + 1不能转换为S n0。术语n0 + 1是相等的，但不可转换，并且用作类型的术语只有在可转换时才能互换。
如果两种类型相等，可以编写一个函数，将一种类型的项"强制转换"为另一种类型的项。实际上，执行此操作的通用函数是eq_rect，它是相等类型族的析构函数。可以定义一个专门的函数，将一个向量强制转换为可证明但不一定可转换的长度相等的向量。
Definition vect_eq_nat {X : Type} {m n : nat} (H : m = n) v :=
eq_rect _ (fun k => @vect X k X) v _ H.
如果eq_rect的使用没有立即突出，您可以通过策略定义这些函数。只要确保您定义的函数不仅具有正确的类型，而且具有所需的结果，并且使定义透明即可。
Definition vect_eq_nat {X : Type} {m n : nat} : m = n -> @vect X m X -> @vect X n X.
intros.
rewrite <- H.
exact X0.
Defined.
Print vect_eq_nat.
您也可以使用Program白话来混合证明和术语。
Program Definition vect_plus_comm {X : Type} {n : nat} (v : @vect X (n+1) X) : @vect X (S n) X :=
vect_eq_nat _ v.
Require Import Arith.
Require Import Omega.
Solve Obligation 0 using (intros; omega).
现在您可以使用这个辅助定义来定义rev。
Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X :=
match v in (vect n X) return (vect n X) with
| Nil => Nil
| Cons _ x xs => vect_plus_comm (app (rev xs) (Cons _ x Nil))
end.
你可以使用Program Fixpoint直接定义rev，一旦你把转换步骤到位。唯一的证明义务是S n0和n0 + 1之间的相等。
Program Fixpoint rev' {X : Type} {n : nat} (v : @vect X n X) : @vect X n X :=
match v in (vect n X) return (vect n X) with
| Nil => Nil
| Cons _ x xs => vect_eq_nat _ (app (rev' xs) (Cons _ x Nil))
end.
Solve Obligation 0 using (intros; omega).