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,这可能是iff 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),以下方法有效.你需要帮助勒柯克告诉它什么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.不起作用,但单独解决每项义务的工作.