标签: convoy-pattern

在一些依赖类型的语言(例如Idris)中实现向量添加是相当简单的.根据维基百科上的示例:

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

(注意Idris的整体检查器如何自动推断添加Nil和非Nil向量是逻辑上不可能的.)

我正在尝试使用自定义向量实现在Coq中实现等效功能,尽管与官方Coq库中提供的非常相似:

Set Implicit Arguments.

Inductive vector (X : Type) : nat -> Type :=
  | vnul : vector X 0 
  | vcons {n : nat} (h : X) …

我有以下问题，请查看代码。

  (* Suppose we have type A *)
  Variable A: Type.

  (* Also we have a function that returns the type (option A) *)
  Definition f_opt x: option A := ...

  (* Then, I can prove that this function always returns something: *)
  Theorem always_some: forall x, exists y, f_opt x = Some y.
  Admitted.

  (* Or, equivalently: *)
  Theorem always_not_none: forall x, f_opt x <> None.
  Admitted.

现在我想得到一个f_opt总是返回 type 值的版本A。像这样的东西：

  Definition f x: A := …