证明一个被斩首的子序列是同一个序列的子序列

Question

我正在做一个练习，我想出了一个要证明的命题，但我被卡住了。希望有人开导我的思想。

我正在定义一个定义子序列关系的归纳命题，其中第一个列表中的元素需要按顺序出现在第二个列表中，但不一定连续出现。

这是我的定义：

Inductive subseq : list nat -> list nat -> Prop :=
  | emptyseq : forall l, subseq [] l
  | matchh   : forall h l1 l2, subseq l1 l2 -> subseq (h :: l1) (h :: l2)
  | nmatchh  : forall h l1 l2, subseq l1 l2 -> subseq l1 (h :: l2).

以及我要证明的定理：

Theorem subseq_shrink : forall h l1 l2,
  subseq (h :: l1) l2 -> subseq l1 l2.

基本上它说如果头部被砍掉，列表仍然是子序列。很直观，不是吗？但是，我卡住了。

以下是我证明的一部分：

Proof.
  intros h l1 l2 H. generalize dependent h. induction l1.
  - intros. apply emptyseq.
  - intros h H.

证据看起来并不好。

1 subgoals
x : nat
l1 : list nat
l2 : list nat
IHl1 : forall h : nat, subseq (h :: l1) l2 -> subseq l1 l2
h : nat
H : subseq (h :: x :: l1) l2
______________________________________(1/1)
subseq (x :: l1) l2

这让我看起来很无能。我在某处犯错了吗？我错过了哪一部分来陷入这个简单的定理？

Answer 1

您可以在 subseq 推导中使用归纳法。请注意下面的 remember：我们需要它，因为 Coq 使用类型族索引的方式。我认为它在《软件基础》一书中的某处有所描述。尝试删除它，看看会发生什么。

Theorem subseq_shrink : forall h l1 l2,
  subseq (h :: l1) l2 -> subseq l1 l2.
Proof.
  intros h l1 l2 H.
  remember (h :: l1) eqn:Eq.
  induction H.
  - inversion Eq.
  - inversion Eq; clear Eq; subst.
    now constructor.
  - destruct l0; inversion Eq; clear Eq; subst.
    now constructor; apply IHsubseq.
Qed.

Answer 2

这里有多种解决方案。但重要的是理解为什么我们需要归纳法。其实我们想要的是去掉l1前面的h。而由于subseq的定义，我们知道h是l2的第一个元素，否则就是第二个，否则就是第三个，或者...

实际上，我们需要在 l2 中找到 h，为此我们需要对 l2 而不是 l1 进行归纳。按照另一个答案的建议对 subseq 进行归纳也有助于在 l2 中找到 h，这就是它也可以工作的原因。

对l2进行归纳似乎更简单。这是证明的开头：

Theorem subseq_shrink : forall h l1 l2,
  subseq (h :: l1) l2 -> subseq l1 l2.
Proof.
  intros h l1 l2. revert h l1. induction l2; intros.

证明一个被斩首的子序列是同一个序列的子序列

Prove that a beheaded subsequence is a subsequence of the same sequence

coq

subsequence