如何证明一个空列表的子序列是空的

Question

我是coq的新手。我试图证明一个空列表的子序列是空的

这是我正在研究的引理：

Lemma sub_nil : forall l , subseq l nil <-> l=nil. 

我试着分开，这样我就可以有了

subseq l nil -> l = nil

和

l = nil -> subseq l nil

为了证明第一个，我尝试了在l上进行归纳，但当它证明时，我阻止了

subseq (a :: l) nil -> a :: l = nil

谢谢。

Answer 1

此处使用的策略是inversion。为inversion！解释coq文档：

给定一个归纳假设(H:I t(，那么应用于H的反演为(I t(的每个可能的构造函数c I导出，所有必要的条件都应该适用于由c I证明的实例。

假设subseq谓词如下所示：

Inductive subseq {A:Type} : list A -> list A -> Prop :=
| SubNil   : forall (l:list A), subseq  nil l
| SubCons1 : forall (s l:list A) (x:A), subseq  s l -> subseq s (x::l)
| SubCons2 : forall (s l: list A) (x:A), subseq s l -> subseq (x::s) (x::l). 

证据会被粘在这里(正好在你指定的地方(：

Lemma sub_nil2 : forall (A:Type) (l: list A) , subseq l nil <-> l=nil.
Proof.
split.
-  destruct l eqn:E; intros.
*  reflexivity.
(*Now unable to prove a::l0 = [] because the hypothesis: subseq (a :: l0) [] is absurd.*)
* inversion H.(*Coq reasons that this hypothesis is not possible and discharges the proof trivially*)
- intros. subst. apply SubNil.
Qed.

注意，我使用了destruct策略，但即使使用归纳策略，问题仍然存在。

整个证明可以干净地写如下：

Lemma sub_nil : forall (A:Type) (l: list A) , subseq l nil <-> l=nil.
Proof.
split; intros.
- inversion H. reflexivity.
- subst. apply SubNil.
Qed.