问题描述
我试图证明以下定理
Theorem subseq_subset : forall l1 l2,subseq l1 l2 -> sublist l1 l2.
归纳类型为subseq：
Inductive subseq {A:Type} : list A -> list A -> Prop :=
| SubNil : forall (l:list A),subseq nil l
| Sub_both : forall (s l:list A) (x:A),subseq s l -> subseq s (x::l)
| Sub_right : forall (s l: list A) (x:A),subseq s l -> subseq (x::s) (x::l).
和子列表的定义：
DeFinition sublist (l1 l2 : list A) : Prop := forall x : A,In x l1 -> In x l2.
这是我开始做的证明
Theorem subseq_subset : forall l1 l2,subseq l1 l2 -> sublist l1 l2.
Proof.
intros.
unfold sublist. intros.
induction l2.
+ inversion H in H0. simpl. simpl in H0. assumption.
+ apply in_cons. apply IHl2.
Qed.
我现在有这个上下文
1 subgoals
l1 : list A
a : A
l2 : list A
H : subseq l1 (a :: l2)
x : A
H0 : In x l1
IHl2 : subseq l1 l2 -> In x l2
______________________________________(1/1)
subseq l1 l2
我认为对H申请sub_right，所以我可以用假设结束证明，但是apply sub_right in H不起作用。这可能吗？我该如何结束这个证明？
谢谢。
解决方法
首先请注意，您已经定义了
Inductive subseq {A:Type} : list A -> list A -> Prop :=
| SubNil : forall (l:list A),subseq nil l
| Sub_both : forall (s l:list A) (x:A),subseq s l -> subseq s (x::l)
| Sub_right : forall (s l: list A) (x:A),subseq s l -> subseq (x::s) (x::l).
对分支使用大写字母，因此将为apply Sub_right in H。此外，我认为您切换了both和right分支。对于此答案的其余部分，我将假定定义为
Inductive subseq {A:Type} : list A -> list A -> Prop :=
| subNil : forall (l:list A),subseq nil l
| sub_right : forall (s l:list A) (x:A),subseq s l -> subseq s (x::l)
| sub_both : forall (s l: list A) (x:A),subseq s l -> subseq (x::s) (x::l).
现在是您的实际问题。当您说apply sub_right in H不起作用时，您会收到什么错误消息？ Coq告诉我找不到x。这是有道理的：如果您要应用一个在右侧具有x而在左侧没有x的定理，则Coq无法猜测哪个x使用。您可以通过说出x来明确选择apply (sub_right _ _ x) in H。
也就是说，我不知道如何从您所在的位置来完成您的证明。我认为您需要归纳假设。例如，如果您要证明subseq l1 (x :: l2) -> sublist l1 (x :: l2)，那么很高兴知道subseq l1 l2 -> sublist l1 l2。您可以通过在subseq l1 l2的证明上使用归纳 而不是在列表之一上进行归纳来实现：
intros l1 l2 subseql1l2.
unfold sublist.
induction subseql1l2.
...
这为您提供了三个不错的案例，可以直观地看出它们是真实的。为了证明它们，您将需要一些有关In和列表的事实，您可以使用Search In (_ :: _).