Coq：为什么重写定理中的引理会创建两个子目标？

Question

我正在尝试证明我的非零函数分布在列表的连接上。

我是这样写的带过滤器的nonzeros'：

Definition nonzeros' (l : list nat) : list nat := filter (fun x => match x with | O => false | _ => true end) l.

我已经证明了这 2 个引理：

Lemma nonzeros'_remove_0 :
  forall (a b: list nat),
  nonzeros' (0 :: b) = nonzeros' b.
Proof.
  intros a b.
  unfold nonzeros'.
  simpl. 
  reflexivity.
Qed.

Lemma nonzeros'_not_remove_Sn :
  forall (a b: list nat) (n : nat),
  nonzeros' (S n :: b) = S n :: nonzeros' b.
Proof.
  intros a b n.
  unfold nonzeros'.
  simpl. 
  reflexivity.
Qed.

现在我必须通过 concat 证明分布：

Lemma nonzero'_distribution_over_concat :
  forall (a b : list nat),
  nonzeros' (concat a b) = concat (nonzeros' a) (nonzeros' b).

为了证明这一点，我做了以下事情：

Proof.
  intros a b.
  induction a as [| h t IHa].
  - 
    simpl. 
    reflexivity.
  - 
    simpl.
    destruct h.
    + rewrite nonzeros'_remove_0. rewrite nonzeros'_remove_0. rewrite IHa. reflexivity.

问题是后招

rewrite nonzeros'_remove_0.

Coq 创建 2 个子目标：

______________________________________(1/2)
nonzeros' (concat t b) = concat (nonzeros' (0 :: t)) (nonzeros' b)
______________________________________(2/2)
list nat

第二个子目标是意外的。为什么会出现？

Answer 1

引理有一个未使用的参数a : list nat:

Lemma nonzeros'_remove_0 :
  forall (a b: list nat),
  nonzeros' (0 :: b) = nonzeros' b.

因此，要应用该引理，您需要提供这样一个列表，并且除了通过额外目标询问您之外，没有办法告诉您它应该是哪个列表。还可以开发自动化以在此处做出任意选择，但更好的解决方法是首先从引理中删除未使用的参数。

Lemma nonzeros'_remove_0 :
  forall (b: list nat),
  nonzeros' (0 :: b) = nonzeros' b.

Coq：为什么重写定理中的引理会创建两个子目标？

Coq: Why rewrite of lemma in theorem create two subgoal?

coq

coq-tactic