如何在假设中应用构造函数？

如何解决如何在假设中应用构造函数？

我试图证明以下定理

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 (_ :: _).

查找这些事实。