小编Sar*_*ara的帖子

我正在尝试编写一个函数,它接受一个自然数列表并返回其中不同元素的数量作为输出.例如,如果我有列表[1,2,2,4,1],我的函数DifElem应该输出"3".我尝试了很多东西,我得到的最接近的是:

Fixpoint DifElem (l : list nat) : nat :=
   match l with
   | [] => 0
   | m::tm => 
   let n := listWidth tm in
   if (~ In m tm) then S n else n
end.

我的逻辑是:如果m不在列表的尾部,那么将一个添加到计数器.如果是,不要添加到计数器,所以我只计算一次:它是最后一次出现.我收到错误:

Error: The term "~ In m tm" has type "Prop"
which is not a (co-)inductive type.

In是Coq列表标准库的一部分Coq.Lists.List.它定义为:

Fixpoint In (a:A) (l:list A) : Prop :=
   match l with
   | [] => False
   | b :: m => b = a …

我需要使用名为Coq.Arith.PeanoNat(https://coq.inria.fr/library/Coq.Arith.PeanoNat.html)的标准库部分.

我已经尝试导入整个Arith库或只是导入这个模块,但我不能以任何方式使用它.

我试过的其他每个图书馆工作得很好.我什么时候Require Import Bool.编译,我可以正确使用它.当Print Bool.我可以看看所有在接下来的格式里面的功能:

Module
Bool
:= Struct
Definition...
.
.
.
End

当我做任何一个Require Import Arith.PeanoNat.或Require Import Arith.我得到这个立即输出:

[Loading ML file z_syntax_plugin.cmxs ... done]
[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]
<W> Grammar extension: in [tactic:simple_tactic], some rule has been     masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic], some rule has been masked
<W> Grammar …

我正在 Coq 中工作，并试图弄清楚如何做下一步：如果我有一个自然数列表和一个给定的 number n，我想在每个 之前和之后打破我的列表n。为了更清楚地说明，如果我有列表[1; 2; 0; 3; 4; 0; 9]和数字n = 0，那么我希望输出三个列表：[1;2]、[3;4]和[9]。我遇到的主要问题是我不知道如何在Fixpoint. 我想我需要嵌套Fixpoints 但我只是不知道如何做。作为一个非常原始的想法，我有太多问题：

Fixpoint SubLists (A : list nat)(m : nat) :=
 match A with
 |[] => []
 |n::A0 => if n =? m then (SubLists L) else n :: (SubLists L)
end.

我非常感谢您对如何执行此操作以及如何导航具有多个元素的输出的意见。

我在理解如何使用证明中在Coq中定义的某些内容时遇到了一些麻烦。我有这个定义和功能的片段：

Inductive string : Set :=
| E  : string
| s  : nat -> string -> string.

Inductive deduce : Set :=
|de : string -> string -> deduce.

Infix "|=" := de. 

Inductive Rules : deduce -> Prop :=
| compress : forall (n   : nat) (A    : string), rule (( s n ( s n A))  |= ( s n A))
 | transitive : forall A B C : string, rule (A |= B) -> rule (B …