3

我试图在列表中搜索一个对象，然后如果找到它可能返回 true；否则为假。

但是，我试图想出的是不正确的。我真的很感激一些指导。我需要该函数通过将列表的头部与相关元素进行比较来搜索元素列表，如果不匹配，则递归地将列表的其余部分通过函数并重复，通过匹配列表的头部。

Fixpoint find (li:list Interface){struct li}: list Interface :=
match li with
| nil => nil
| y::rest => find rest 
end.

非常感谢您的指导和帮助。

先感谢您

4

2 回答 2

3

List标准库中的理论中有一个非常相似的函数。该函数将谓词作为参数，即f从元素类型到的函数，如果找到匹配元素，或者没有找到匹配元素bool，则返回。Some xxNone

Variable A : Type.
Fixpoint find (f:A->bool) (l:list A) : option A :=
  match l with
    | nil => None
    | x :: tl => if f x then Some x else find tl
  end.

您正在寻找与特定对象相等的元素a。这意味着你的谓词是eq_Interface a，eq_Interface你想要的平等在哪里Interface。

你可以在你的类型上定义一个相等函数，因为可以有很多相等的定义。Coq 定义了=Leibniz相等：两个值相等，如果没有办法区分它们。=是一个命题，而不是布尔值，因为这个属性通常是不可判定的。它也不总是一个类型的理想相等，有时你想要一个更粗略的等价关系，以便两个对象可以被认为是相等的，如果它们以不同的方式构造但仍然具有相同的含义。

IfInterface是一个简单的数据类型——直观地说，一个没有嵌入命题的数据结构——有一个内置的策略可以从类型定义中构建一个结构相等函数。decide equality在参考手册中查找。

Definition Interface_dec : forall x y : Interface, {x=y} + {x <> y}.
Proof. decide equality. Defined.
Definition Interface_eq x y := if Interface_dec x y then true else false.

Interface_dec不仅告诉您它的论点是否相等，而且还提供了论点相等或不同的证明。

一旦你有了那个相等函数，你就可以find根据标准库函数来定义你的函数：

Definition Interface_is_in x := if List.find (Interface_eq x) then true else false.
于 2011-07-10T14:03:34.607 回答
-1

嗯，我不会通过提供工作代码来破坏乐趣:)。你显然错过了一些东西。你的问题是如何在 Coq 中编码还是更普遍？你会如何用伪代码编写它？或者使用您熟悉的其他语言？

于 2011-07-09T19:50:57.067 回答