Program Fixpoint: recursive call in `let` and hypothesis of the obligation

Question

Say I have the following 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.

(This example basically returns l in a very stupid way, for the sake of having a simple example).

Here, I have a recursive call to f (stored in f_rec) which is only used if l contains an element, which ensures that when I use f_rec, length (tl l) is indeed smaller than length l.

However, when I want to solve the obligation

Next Obligation.

I don't have the hypothesis hd_error l = Some n which I need.

(Somehow, I have the impression that it is understood as "compute f (tl l) at the let in place", and not "delay the computation until it is actually used").

---

To illustrate the difference, if I "inline" the let ... in statement:

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.

Here I have Heq_anonymous : Some n = hd_error [] in the environment.

---

My question is the following: is it possible to have the hypothesis I need, i.e. to have the hypothesis generated by the match ... with statement ?

N.B.: Moving the let is a solution, but I am curious to know whether this is possible without doing so. For instance, it might be useful in the case f_rec is used in various contexts, to avoid duplicating f (tl l).

Answer 1

One trick is to explicitly ask for the hypothesis you need (I recently saw it in this answer by Joachim Breitner):

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

This way you will be able to use f_rec only when it makes sense.

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.