如何在Coq中对列表结尾进行归纳

Question

以一种标准的方式，我可以对这样的列表进行归纳

• 已批准lst
• 证明x::lst

但是我想要：

• 已批准lst
• 证明lst ++ x::nil

对我来说，x在列表中的位置很重要。

我试图写类似this的东西，但是没有成功。

Answer 1

在这种情况下，您需要证明自己的归纳原理。但是在这里，您很幸运，因为您所需要的已经在Coq的标准库中：

Require Import List.

Check rev_ind.
(*
rev_ind
     : forall (A : Type) (P : list A -> Prop),
       P nil ->
       (forall (x : A) (l : list A), P l -> P (l ++ x :: nil)) ->
       forall l : list A, P l
*)