我对 Coq 很陌生，但是对于我的项目，我必须在 Coq 中使用 union-find 数据结构。 Coq 中是否有 union-find（不相交集）数据结构的实现？
如果没有，有人可以提供一个实现或一些想法吗？它不必非常有效。 （不需要进行路径压缩或所有花哨的优化）我只需要一个可以保存任意数据类型（如果太难的话是 nat）并执行的数据结构：union em> 和 找到。
提前致谢
【问题讨论】：
标签： data-structures coq disjoint-sets union-find
Maëlan 有一个很好的答案，但是对于更简单和更低效的不相交集数据结构，您可以只使用 nat 的函数来表示它们。这避免了任何终止粘性。本质上，任何全函数的原像在域上形成不相交的集合。另一种看待这个问题的方法是将任何不相交集G 表示为柯里化应用程序find_root G : nat -> nat，因为find_root 是不相交集提供的基本接口。
这也类似于在 Coq 中使用函数来表示地图，就像在 Software Foundations 中一样。 https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
Require Import Arith.
Search eq_nat_decide.
(* disjoint set *)
Definition ds := nat -> nat.
Definition init_ds : ds := fun x => x.
Definition find_root (g : ds) x := g x.
Definition in_same_set (g : ds) x y :=
eq_nat_decide (g x) (g y).
Definition union (g : ds) x y : ds :=
fun z =>
if in_same_set g x z
then find_root g y
else find_root g z.
您也可以像这样在不相交集中保存的类型上使其通用
Definition ds (a : Type) := a -> nat.
Definition find_root {a} (g : ds a) x := g x.
Definition in_same_set {a} (g : ds a) x y :=
eq_nat_decide (g x) (g y).
Definition union {a} (g : ds a) x y : ds a :=
fun z =>
if in_same_set g x z
then find_root g y
else find_root g z.
要初始化特定a 的不相交集，您基本上需要一个用于您的类型a 的Enum 实例。
Definition init_bool_ds : ds bool := fun x => if x then 0 else 1.
根据您的证明风格和需要，您可能希望将eq_nat_decide 换成eqb 或其他大致相当的东西。
【讨论】：
如果您只需要一个数学模型，而不关心实际性能，我会选择最直接的模型：一个函数映射（有限偏函数），其中每个元素可选地链接到另一个与之关联的元素合并。
注意：在这个答案的其余部分，作为联合查找的标准，我将假设元素只是自然数。如果您想要其他类型的元素，只需使用另一个将所有元素绑定到唯一编号的映射。
然后，您将定义一个函数find : UnionFind → nat → nat，该函数返回给定元素的规范代表，只要您可以跟踪链接。请注意，该函数将使用递归，其终止参数并非微不足道。为了实现它，我认为最简单的方法是保持一个数字只链接到一个较小的数字的不变量（即如果i 链接到j，那么i > j）。然后递归终止，因为当跟随链接时，当前元素是一个递减的自然数。
定义函数union : UnionFind → nat → nat → UnionFind 更容易：union m i j 只返回一个更新的地图，其中max i' j' 链接到min i' j'，其中i' = find m i 和j' = find m j。
[关于性能的旁注：保持不变性意味着您无法根据它们的等级充分选择一对分区中的哪一个要合并到另一个中；但是，如果您愿意，您仍然可以实现路径压缩！]
至于地图究竟使用哪种数据结构：有几种可用的。 standard library（查看标题FSets）有几个满足FMapInterface 接口的实现（FMapList、FMapPositive 等）。 stdpp 库有gmap。
同样，如果性能不是问题，只需选择最简单的编码，或者更重要的是，选择最简单的证明。我正在考虑的只是一个自然数列表。 列表的位置是元素以相反的顺序。 列表的值是偏移量，即向前跳过以到达链接目标的位置数。
j (i > j) 的元素i，偏移量为i − j。以我最好的伪 ASCII 艺术技能，这里有一个链接是 { 6↦2, 4↦2, 3↦0, 2↦1 } 和规范代表是 { 5, 1, 0 } 的地图：
6 5 4 3 2 1 0 element
↓ ↓ ↓ ↓ ↓ ↓ ↓
/‾‾‾‾‾‾‾‾‾↘
[ 4 ; 0 ; 2 ; 3 ; 1 ; 0 ; 0 ] map
\ \____↗↗ \_↗
\___________/
动机是上面讨论的不变量随后在结构上被强制执行。因此，有希望find实际上可以通过结构归纳来定义（在列表的结构上），并且可以免费终止。
它描述了在 ML 中有效的联合查找数据结构的实现，从用户的角度来看是持久的，但在内部使用了变异。你可能更感兴趣的是，他们在 Coq 中证明了它是正确的，这意味着他们有一个用于联合查找的 Coq 模型。然而，这个模型反映了他们试图证明是正确的命令式程序的内存存储。我不确定它对您的问题的适用程度。
【讨论】：