Coqで定理の証明中にまったく新しい変数を導入する方法があるかどうか疑問に思っていましたか?
完全な例として、リストの長さの均一性に関する次のプロパティをここから検討してください。
Inductive ev_list {X:Type}: list X -> Prop :=
| el_nil : ev_list []
| el_cc : forall x y l, ev_list l -> ev_list (x :: y :: l).
ここで、任意のリストが偶数の場合、次lのことが成り立つことを証明したいと思います。lengthev_list l
Lemma ev_length__ev_list': forall X (l : list X), ev (length l) -> ev_list l.
Proof.
intros X l H.
与える：
1 subgoals
X : Type
l : list X
H : ev (length l)
______________________________________(1/1)
ev_list l
nここで、新しい自由変数と仮説を「定義」したいと思いますn = length l。手書きの数学では、これができると思いますn。しかし、Coqで同じことをする方法はありますか?
ノート。私が尋ねる理由は次のとおりです。
前にリンクされたページで行われているように、これを定理自体のステートメントに人為的に導入したくありませんが
n、これは不自然です。しようとしました
induction H.が、うまくいかないようです。length lCoq は'sネスのケース分析を行うことができずev、帰納仮説 (IH) は生成されませんでした。
ありがとう。