程序修复点：在“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。

（不知何故，我的印象是它被理解为“在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陈述产生的假设？

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

Answer 1

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