coq - 如何在 Coq 中引入一个新变量？

Question

我想知道是否有办法在 Coq 定理的证明过程中引入一个全新的变量？
有关完整示例，请考虑以下属性 from here关于列表长度的均匀性。

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如果它的 length是偶数，那么 ev_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. ，但似乎不起作用。 Coq 无法对 length l 进行案例分析的 ev -ness，并且没有产生诱导假设(IH)。

谢谢。

Answer 1

这是 Coq 证明中的常见问题。您可以使用 remember战术:

remember (length l) as n.

如果您在 H 上进行归纳同样，您可能还需要对 l 进行概括。事先，通过做

generalize dependent l.
induction H.