在 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.

所以，我尝试通过 destruct H.

查看 subseq (x :: xs) ys 的证明

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并不知道那么多。它只是在 empty_subseq 的情况下用 [] 和 [] 替换了 x :: xs 和 xs。特别是，这经常导致上下文中的信息丢失。更好的选择：

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

Answer 2

丽瑶的回答其实很有用。这是引理的证明。

Lemma del_l_preserves_subseq : forall x xs ys, subseq (x :: xs) ys -> subseq xs ys.
Proof.
  intros x xs ys.
  induction ys as [|y ys'].
  - intros. inversion H. (* Inversion will detect that no constructor matches the type of H *)
  - intros. inversion H. (* Inversion will automatically discharge the first case *)
    + (* When [subseq (x :: xs) ys'] holds *)
      apply IHys' in H2. now apply add_right.
    + (* When [subseq xs ys'] holds *)
      now apply add_right.
Qed

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

Proving `forall x xs ys, subseq (x :: xs) ys -> subseq xs ys` in Coq

coq

proof

theorem-proving