如何在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' evsness 进行案例分析,也没有产生诱导假设(IH).

谢谢.

Answer 1

这是Coq证明中的常见问题.你可以使用这个remember策略:

remember (length l) as n.

如果您正在进行归纳H,那么您可能还需要l事先进行归纳

generalize dependent l.
induction H.