Coq 依赖类型

Question

我是 Coq 的新手，需要一些简单示例的帮助来帮助我入门。特别是我对使用依赖类型定义向量(固定大小列表)的一些操作很感兴趣。我从 Vector 包开始，并尝试实现一些额外的功能。例如，我在实现简单的“take”和“drop”函数时遇到困难，这些函数从列表中获取或删除第一个“p”元素。

Require Import Vector.

Fixpoint take {A} {n} (p:nat) (a: t A n) : p<=n -> t A p := 
   match a return ( p<=n -> t A p) with
     | cons A v (S m) => cons (hd v) (take m (tl v)) m
     | nil => fun pf => a
   end.

错误(在 nil 的情况下)是:

The term "a" has type "t A n" while it is expected to have type "t A p".

有人可以帮助我了解一些起点吗？谢谢!

Answer 1

我不明白你的做法。当参数是一个非空向量时，你总是返回一个非空向量，但是 take必须返回 nil什么时候p=0无论向量如何。

这是构建 take 的一种方法.而不是使用假设 p <= n , 我表示参数的长度 n作为数字的总和 p要采用的元素数量和尾随元素的数量 m , 这是可能的当且仅当 p <= n .这允许更简单的递归定义，因为 (S p') + m在结构上等于 S (p' + m) .请注意，区别在于要采用的元素数量:返回 nil如果取 0，返回 cons head new_tail否则。

这个版本的take函数具有所需的计算行为，因此剩下的就是定义一个具有所需证明内容的函数。我用 Program方便的功能:填写计算内容(琐碎，我只需要说我要使用m = n - p)，然后完成证明义务(简单的算术)。

Require Import Arith.
Require Import Vector.

Fixpoint take_plus {A} {m} (p:nat) : t A (p+m) -> t A p := 
   match p return t A (p+m) -> t A p with
     | 0 => fun a => nil _
     | S p' => fun a => cons A (hd a) _ (take_plus p' (tl a))
   end.
Program Definition take A n p (a : t A n) (H : p <= n) : t A p :=
          take_plus (m := n - p) p a.
Solve Obligations using auto with arith.

---

为您的newdrop : forall A n p, t A n -> p <= n -> t A (n-p) ，以下方法有效。你需要告诉 Coq 什么来帮助它 p和 n成为递归调用。

Program Fixpoint newdrop  {A} {n} p : t A n -> p <= n -> t A (n-p) :=
   match p return t A n -> p <= n -> t A (n-p) with
     | 0 => fun a H => a
     | S p' => fun a H => newdrop p' (tl a) (_ : p' <= n - 1)
   end.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.

不知道为什么Solve Obligations using omega.行不通，但单独解决每项义务是可行的。