Coq无法看到两种类型相同

Question

我试图在矢量上定义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代码有任何其他评论，请不要犹豫。

Answer 1

\n

Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X :=\n  fold_left (fun {X : Type} {k : nat} (acc : vect k X) (x : X) => Cons x acc) Nil v.\n

\n

\n\n

第一个显式参数fold_left必须具有 形式的类型?1 -> ?2 -> ?1，即两个参数的函数，其返回类型与第一个参数相同。[依赖] \xe2\x80\x9cproduct\xe2\x80\x9d 是函数的 Coq 术语。您传递的是 形式的术语fun (X:Type) b c d => \xe2\x80\xa6，因此?1是Type，并且该术语fun c d => \xe2\x80\xa6（显然具有产品类型）必须具有?给定上下文的类型，因此它必须具有类型Type，即它必须是一种排序。

\n\n

如果您尝试解决此问题，您会发现您的fold_left函数在这里不起作用：您需要在迭代期间改变向量的长度，但迭代器参数fold_left的类型在迭代期间保持不变。使用fold_left您拥有的函数，如果您从 Accumulator （Nil长度为 0 的向量）开始，您最终将得到相同类型的结果，同样是长度为 0 的向量。

\n\n

我还没有考虑过如何定义一个更通用的迭代器来让您定义rev，但我确信这是可能的。

\n\n\n\n

至于您的第二次尝试，vect (n0 + 1) X和 的问题vect (S n0) X是它们不是同一类型，因为n0 + 1不能转换为S n0. 这些术语n0 + 1是相等的但不可转换，并且用作类型的术语只有在可转换的情况下才可以互换。

\n\n

如果两种类型相等，您可以编写一个函数，将 \xe2\x80\x9ccasts\xe2\x80\x9d 一种类型的项转换为另一种类型的项。事实上，执行此操作的通用函数是eq_rect相等类型族的析构函数。您可能会发现它定义了一个专门的函数，将向量转换为可证明但不一定可转换的等长向量。

\n\n

Definition vect_eq_nat {X : Type} {m n : nat} (H : m = n) v :=\n  eq_rect _ (fun k => @vect X k X) v _ H.\n

\n\n

如果 的用法eq_rect不能立即脱颖而出，您可以通过策略来定义此类函数。只需确保您定义的函数不仅具有正确的类型，而且具有所需的结果，并使定义透明。

\n\n

Definition vect_eq_nat {X : Type} {m n : nat} : m = n -> @vect X m X -> @vect X n X.\nintros.\nrewrite <- H.\nexact X0.\nDefined.\nPrint vect_eq_nat.\n

\n\n

您还可以使用Program白话来混合证明和术语。

\n\n

Program Definition vect_plus_comm {X : Type} {n : nat} (v : @vect X (n+1) X) : @vect X (S n) X :=\n  vect_eq_nat _ v.\nRequire Import Arith.\nRequire Import Omega.\nSolve Obligation 0 using (intros; omega).\n

\n\n

现在您可以使用这个辅助定义来定义rev.

\n\n

Fixpoint rev {X : Type} {n : nat} (v : @vect X n X) : @vect X n X :=\n  match v in (vect n X) return (vect n X) with\n    | Nil => Nil\n    | Cons _ x xs => vect_plus_comm (app (rev xs) (Cons _ x Nil))\n  end.\n

\n\n

一旦您完成了转换步骤，您就可以直接使用Program Fixpoint来定义。rev唯一的证明义务是S n0和之间的相等性n0 + 1。

\n\n

Program Fixpoint rev' {X : Type} {n : nat} (v : @vect X n X) : @vect X n X :=\n  match v in (vect n X) return (vect n X) with\n    | Nil => Nil\n    | Cons _ x xs => vect_eq_nat _ (app (rev' xs) (Cons _ x Nil))\n  end.\nSolve Obligation 0 using (intros; omega).\n

\n