coq - 在 Coq 中证明 `forall x xs ys, subseq (x::xs) ys -> subseq xs ys`

Question

我有以下定义

Inductive subseq : list nat -> list nat -> Prop :=
| empty_subseq : subseq [] []
| add_right : forall y xs ys, subseq xs ys -> subseq xs (y::ys)
| add_both : forall x y xs ys, subseq xs ys -> subseq (x::xs) (y::ys)
.

使用这个，我想证明以下引理

Lemma del_l_preserves_subseq : forall x xs ys, subseq (x :: xs) ys -> subseq xs ys.

所以，我试着看 subseq (x :: xs) ys 的证明通过做 destruct H .

Proof.
  intros. induction H.

3 subgoals (ID 209)

  x : nat
  xs : list nat
  ============================
  subseq xs [ ]

subgoal 2 (ID 216) is:
 subseq xs (y :: ys)
subgoal 3 (ID 222) is:
 subseq xs (y :: ys)

为什么第一个子目标要我证明 subseq xs [] ?不应该是 destruct战术知道证明不能是形式 empty_subseq因为类型包含 x :: xs而不是 [] ?

一般来说，我如何证明我试图证明的引理？

Answer 1

Shouldn't the destruct tactic know that the proof cannot be of the form empty_subseq since the type contains x :: xs and not []?

事实上， destruct不知道那么多。它只是取代 x :: xs和 xs与 []和 []在 empty_subseq案件。特别是，这经常导致上下文中的信息丢失。更好的选择:

使用 inversion而不是 destruct .

使用 remember确保 subseq 的两个类型索引是 destruct 之前的变量. ( remember (x :: xs) as xxs in H. ) 这种更明确的目标管理也适用于 induction .