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

Question

我想知道是否有办法在 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，如果它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 中做同样的事情？

笔记。我问的原因是：

1. 我不想将其n人为地引入定理本身的陈述中，就像在前面链接的页面中所做的那样，恕我直言，这是不自然的。

2. 我试过了induction H.，但它似乎不起作用。Coq 无法对length l's ev-ness 进行案例分析，也没有生成归纳假设 (IH)。

谢谢。

Answer 1

这是 Coq 证明中的常见问题。您可以使用以下remember策略：

remember (length l) as n.

如果你也在做归纳H，你可能还必须l事先进行概括，方法是

generalize dependent l.
induction H.

Answer 2

根据 Curry-Howard 同构，您的上下文中的假设只是变量。您可以使用函数定义新变量。以下策略使用新变量（设置为）和证明（设置为 ）refine扩展了目标。nlength len = length leq_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