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.
l: list nat
f: forall l0 : list nat,
length l0 < length l -> list nat
length (tl l) < length l

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.
l: list nat
f: forall l0 : list nat,
length l0 < length l -> list nat
n: nat
Heq_anonymous: Some n = hd_error l
length (tl l) < length l
  destruct l.
f: forall l : list nat,
length l < length [] -> list nat
n: nat
Heq_anonymous: Some n = hd_error []
length (tl []) < length []
n0: nat
l: list nat
f: forall l0 : list nat,
length l0 < length (n0 :: l) -> list nat
n: nat
Heq_anonymous: Some n = hd_error (n0 :: l)
length (tl (n0 :: l)) < length (n0 :: 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

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.
l: list nat
f: forall l0 : list nat,
length l0 < length l -> list nat
n: nat
Heq_anonymous: Some n = hd_error l
length (tl l) < length l destruct l; [discriminate | auto]. Qed.