coq - Coq 中列表的 bool 相等性？

Question

我希望能够在 Coq 中比较两个类型为“list”的项目，并得到一个 bool 值“true”或“false”来表示它们是否等价。

现在，我正在以这种方式比较两个列表:

Eval vm_compute in (list 1 = list 2). 

我得到一个形式的 Prop:

= nil
   :: (2 :: 3 :: nil)
      :: (2 :: nil)
         :: (3 :: nil) :: nil =
   nil
   :: (2 :: 3 :: nil)
      :: (2 :: nil)
         :: (3 :: nil) :: nil
 : Prop

很明显 list1 = list2，那么我如何让它只返回 true 或 false？

Answer 1

我使用 Mathematical Components Library boolean equality operators :

From mathcomp Require Import all_ssreflect.

...

Eval vm_compute in list 1 == list 2