gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-02 20:27:56 25 4
gpt4 key购买 nike

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

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

但我想要:

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

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

我尝试写类似 this 的内容,但没有成功。

最佳答案

在这种情况下,你需要证明你自己的归纳原理。但在这里你很幸运,因为你需要的东西已经在 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
*)

关于coq - 如何在 Coq 中的列表末尾进行归纳,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59492270/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com