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

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 的类型，即有两个参数的函数，其返回类型与第一个参数相同。 [相关]“产品”是 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).