程序固定点：“let”中的递归调用和义务假设

Question

假设我有以下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 的递归调用（存储在f_rec 中），它仅在l 包含一个元素时使用，它确保当我使用f_rec 时，length (tl l) 确实小于length l.

但是，当我想解决义务时

Next Obligation.

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

（不知怎的，我的印象是“在let in处计算f (tl l)”，而不是“延迟计算直到实际使用”）。

---

为了说明区别，如果我“内联”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)。

Answer 1

一个技巧是明确地询问你需要的假设（我最近在this answerJoachim 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.