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

Question

我试图证明以下定理

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不起作用。这可能吗？我怎样才能结束这个证明？

谢谢。

标签： coqproofcoq-tactic

Answer 1

首先请注意您陈述的定义

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. 此外，我认为您切换了bothandright分支。对于这个答案的其余部分，我将假设定义是

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