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).
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.