私は次のものを持っているとしましょう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場合にのみ使用されます。lf_reclength (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ステートメントによって仮説を生成することは可能ですか?
注: を移動することletは解決策ですが、移動せずにこれが可能かどうか知りたいです。たとえば、f_recがさまざまなコンテキストで使用されている場合に、重複を避けるために役立つ場合がありf (tl l)ます。