Programm Fixpoint: rekursiven Aufruf in `let` und Hypothese der Verpflichtung

Question

Sagen wir, ich habe folgendes 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. 

(Dieses Beispiel im Grunde gibt l in einem sehr dumme Art, im Interesse einer einfachen des Habens Beispiel).

Hier, ich habe einen rekursiven Aufruf an f (gespeichert in f_rec), die nur verwendet wird, wenn l ein Element enthält, das dafür sorgt, dass, wenn I f_rec verwenden, length (tl l) ist in der Tat kleiner als length l.

Allerdings, wenn ich die Verpflichtung

Next Obligation. 

ich hd_error l = Some n nicht die Hypothese lösen haben wollen, die ich brauche.

(Irgendwie habe ich den Eindruck, dass es als "f (tl l) am Ort let in compute" verstanden wird, und nicht "die Berechnung verzögern, bis es tatsächlich verwendet wird").

---

den Unterschied zu verdeutlichen, wenn ich "inline" die let ... in Aussage:

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. 

Hier habe ich Heq_anonymous : Some n = hd_error [] in der Umwelt.

---

Meine Frage ist folgende: ist es möglich, die Hypothese zu haben ich brauche, das heißt die Hypothese von der match ... with Anweisung erzeugt haben?

N.B .: Das Verschieben der let ist eine Lösung, aber ich bin gespannt, ob dies möglich ist, ohne dies zu tun. Zum Beispiel könnte es in dem Fall f_rec nützlich sein, in verschiedenen Kontexten verwendet, um zu vermeiden, f (tl l) duplizieren.

Answer 1

Ein Trick ist explizit für die Hypothese zu fragen, was Sie brauchen (ich sah es vor kurzem in this answer von Joachim Breitner):

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

Auf diese Weise kann f_rec in der Lage, nur zu verwenden, wenn es Sinn macht.

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.