如何证明空列表的子序列为空？

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 ，证明实例 (I t) 应成立的所有必要条件通过 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.

如何证明空列表的子序列为空？

How to prove that the subsequence of an empty list is empty?

coq

coq-tactic