在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

难道destruct策略不应该知道证明不能是empty_subseq的形式,因为类型包含x :: xs而不是[]？

实际上,destruct不知道那么多.它只是取代了x :: xs,并xs用[]和[]在empty_subseq情况.特别是,这经常导致上下文中的信息丢失.更好的选择:

• 用inversion而不是destruct.

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