2

说我有以下内容Program Fixpoint：

From Coq Require Import List Program.
Import ListNotations.

Program Fixpoint f l {measure (length l)}: list nat :=
let f_rec := (f (tl l) ) in
match hd_error l with
| Some n => n :: f_rec
| None => []
end.

（这个例子基本上l以一种非常愚蠢的方式返回，为了有一个简单的例子）。

在这里，我对f(stored in f_rec) 进行了递归调用，该调用仅在l包含元素时使用，它确保当我使用 时f_rec，length (tl l)确实小于length l.

但是，当我想解决义务时

Next Obligation.

我没有hd_error l = Some n我需要的假设。

（不知何故，我的印象是它被理解为“就地计算f (tl l)” let in，而不是“延迟计算直到实际使用”）。

为了说明差异，如果我“内联”let ... in语句：

Program Fixpoint f l {measure (length l)}: list nat :=
match hd_error l with
| Some n => n ::  (f (tl l) )
| None => []
end.

Next Obligation.
destruct l.

这里我Heq_anonymous : Some n = hd_error []在环境中。

我的问题如下：是否有可能有我需要的假设，即有match ... with陈述生成的假设？

注意：移动let是一个解决方案，但我很想知道如果不这样做是否可行。例如，它可能在f_rec用于各种上下文的情况下很有用，以避免重复f (tl l).

4

1 回答 1

2

一个技巧是明确询问您需要的假设（我最近在Joachim Breitner的这个答案中看到了它）：

let f_rec := fun pf : length (tl l) < length l => f (tl l) in

这样，您将f_rec只能在有意义的情况下使用。

Program Fixpoint f l {measure (length l)}: list nat :=
  let f_rec := fun pf : length (tl l) < length l => f (tl l) in
  match hd_error l with
  | Some n => n :: f_rec _
  | None => []
  end.
Next Obligation. destruct l; [discriminate | auto]. Qed.
于 2017-12-20T16:30:27.533 回答