如何在 Coq 的列表末尾进行归纳

【问题标题】：How to do induction on the end of a list in Coq如何在 Coq 的列表末尾进行归纳
【发布时间】：2019-12-26 18:46:04
【问题描述】：

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

为lst 执行批准
证明x::lst

但我想要：

为lst 执行批准
证明lst ++ x::nil

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

我尝试写this之类的东西，但没有成功。

【问题讨论】：

标签： coq coq-tactic coqide

【解决方案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
*)

【讨论】：