如何在假设中应用构造函数？
How to apply a constructor in an hypothesis?
我正在尝试证明以下定理
Theorem subseq_subset : forall l1 l2, subseq l1 l2 -> sublist l1 l2.
归纳类型子序列：
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。这是有道理的：如果你应用的定理在 right-hand-side 上有一个 x 而在 left-hand-side 上没有 x，那么 Coq 无法猜测哪个 x使用。您可以通过说 apply (sub_right _ _ x) in H.
明确选择 x
就是说，我看不出如何从您所在的位置完成您的证明。我认为你需要一个归纳假设。例如，如果你试图证明 subseq l1 (x :: l2) -> sublist l1 (x :: l2)，那么知道 subseq l1 l2 -> sublist l1 l2 会很好。您可以通过在子序列 l1 l2 的证明上使用归纳法 而不是在列表之一上使用归纳法来实现此目的：
intros l1 l2 subseql1l2.
unfold sublist.
induction subseql1l2.
...
这为您提供了三个直观的真实案例。为了证明它们，您将需要一些关于 In 和列表的事实，您可以使用 Search In (_ :: _).
来查找它们
我正在尝试证明以下定理
Theorem subseq_subset : forall l1 l2, subseq l1 l2 -> sublist l1 l2.
归纳类型子序列：
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。这是有道理的：如果你应用的定理在 right-hand-side 上有一个 x 而在 left-hand-side 上没有 x，那么 Coq 无法猜测哪个 x使用。您可以通过说 apply (sub_right _ _ x) in H.
x
就是说，我看不出如何从您所在的位置完成您的证明。我认为你需要一个归纳假设。例如，如果你试图证明 subseq l1 (x :: l2) -> sublist l1 (x :: l2)，那么知道 subseq l1 l2 -> sublist l1 l2 会很好。您可以通过在子序列 l1 l2 的证明上使用归纳法 而不是在列表之一上使用归纳法来实现此目的：
intros l1 l2 subseql1l2.
unfold sublist.
induction subseql1l2.
...
这为您提供了三个直观的真实案例。为了证明它们，您将需要一些关于 In 和列表的事实，您可以使用 Search In (_ :: _).