我正在尝试在列表中搜索一个对象，如果找到，则可能返回 true；否则为假。
但是，我试图想出的是不正确的。我真的很感激一些指导。我需要该函数通过将列表的头部与相关元素进行比较来搜索元素列表，如果不匹配，则递归地将列表的其余部分通过函数并重复，通过匹配列表的头部。
Fixpoint find (li:list Interface){struct li}: list Interface :=
match li with
| nil => nil
| y::rest => find rest
end.
非常感谢您的指导和帮助。
提前谢谢你
【问题讨论】：
标签： list coq theorem-proving
在标准库的List 理论中有一个非常相似的函数。该函数将谓词作为参数，即从元素类型到bool的函数f，如果找到匹配元素x，则返回Some x，如果找不到匹配元素，则返回None。
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 equality：如果无法区分两个值，则它们相等。 = 是一个命题，而不是布尔值，因为这个属性通常是不可判定的。类型上的相等并不总是理想的，有时您需要更粗略的等价关系，以便两个对象可以被认为是相等的，如果它们以不同的方式构造但仍然具有相同的含义。
如果Interface 是一个简单的数据类型——直观地说，是一个没有嵌入命题的数据结构——则有一种内置策略可以从类型定义中构建一个结构相等函数。在参考手册中查找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.
【讨论】：
嗯，我不会通过提供工作代码来破坏乐趣:)。你显然错过了一些东西。您的问题是如何在 Coq 中编码还是更通用？你会如何用伪代码编写它？还是用您熟悉的其他语言？
【讨论】：
find 的定义？