如何在 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.

Answer 2

根据 Curry-Howard 同构，您上下文中的假设只是变量。您可以使用函数定义新变量。以下 refine 策略使用新变量 n（设置为 length l）和证明 e n = length l（设置为eq_refl).

Lemma ev_length__ev_list': forall X (l : list X), ev (length l) -> ev_list l.
Proof.
  intros X l H.
  refine ((fun n (e:n = length l) => _) (length l) eq_refl).
  (* proof *)
Admitted.

Answer 3

如果你只想为你的归纳添加一个新变量，你可以直接使用

induction (length l) eqn:H0

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

How to introduce a new variable in Coq?

coq

coq-tactic