Coq中列表的布尔相等性：如何将相等判断转为布尔值

嘿，这个问题我太熟悉了！你现在用的=是Coq里的命题相等（属于Prop类型），它用来表达“两个对象相等”这个逻辑断言，但本身并不是可计算的布尔值（true/false）。要得到你想要的直接布尔结果，得用专门的可判定相等函数——这类函数能在计算层面判断两个对象是否相等，并返回明确的布尔值。

下面给你两种最常用的解决方案：

方案1：直接用List.eqb（推荐，返回纯布尔值） #

Coq标准库提供了List.eqb函数，专门用来比较列表并返回bool类型结果。使用时需要传入对应元素类型的布尔相等判断函数（比如你的列表元素是自然数，就用Nat.eqb）：

// 先导入需要的标准库模块
Require Import List Nat.

// 定义你要比较的两个列表
Definition list1 := nil :: (2 :: 3 :: nil) :: (2 :: nil) :: (3 :: nil) :: nil.
Definition list2 := nil :: (2 :: 3 :: nil) :: (2 :: nil) :: (3 :: nil) :: nil.

// 执行计算，直接得到布尔值
Eval vm_compute in List.eqb Nat.eqb list1 list2.

执行后你会得到：

= true : bool

简单解释： #

• List.eqb的类型是forall A : Type, (A -> A -> bool) -> list A -> list A -> bool：它会递归遍历列表，用你传入的元素相等函数逐一比较对应位置的元素。
• Nat.eqb是自然数的布尔相等函数，类型为nat -> nat -> bool，负责判断单个自然数是否相等。

方案2：用list_eq_dec（支持同时获取证明） #

如果你不仅需要布尔值，还需要“相等/不相等”的逻辑证明，可以用list_eq_dec。它返回的是sumbool类型（{P} + {Q}，表示要么P成立，要么Q成立），计算后可以转换成布尔值：

Eval vm_compute in list_eq_dec Nat.eq_dec list1 list2.

执行后会得到：

= left eq_refl : {list1 = list2} + {list1 <> list2}

如果要转换成布尔值，只需要加个条件判断：

Eval vm_compute in if list_eq_dec Nat.eq_dec list1 list2 then true else false.

为什么直接用=不行？ #

Coq里的=是逻辑命题（Prop），它用来描述“相等”这个事实，但不是可执行的计算函数。虽然Coq能识别出两个明显相等的列表，但它不会自动把这个逻辑断言转换成布尔值——必须用专门的可计算函数来完成这个转换。

内容的提问来源于stack exchange，提问作者Alyssa Byrnes