Coq中列表的布尔相等？

Question

我希望能够在 Coq 中比较两个“列表”类型的项目，并得到一个布尔值“真”或“假”来表示它们的等价性。

现在，我正在这样比较两个列表：

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

Answer 2

您可以使用 Coq 的命令自动生成一个布尔列表相等函数，该函数将元素的布尔相等作为输入：

Require Import Coq.Lists.List Coq.Bool.Bool.

Import Coq.Lists.List.ListNotations.

Scheme Equality for list.

打印出来：

list_beq is defined
list_eq_dec is defined

其中list_beq 是列表上的布尔相等函数，其第一个参数是列表元素的比较函数，然后是两个列表：

Print list_beq.

给予

list_beq = 
fun (A : Type) (eq_A : A -> A -> bool) =>
fix list_eqrec (X Y : list A) {struct X} : bool :=
  match X with
  | [] => match Y with
          | [] => true
          | _ :: _ => false
          end
  | x :: x0 => match Y with
               | [] => false
               | x1 :: x2 => eq_A x x1 && list_eqrec x0 x2
               end
  end
     : forall A : Type, (A -> A -> bool) -> list A -> list A -> bool

和

Check list_eq_dec

给予

list_eq_dec
     : forall (A : Type) (eq_A : A -> A -> bool),
       (forall x y : A, eq_A x y = true -> x = y) ->
       (forall x y : A, x = y -> eq_A x y = true) -> forall x y : list A, {x =  y} + {x <> y}

如果底层类型相等与莱布尼茨相等一致，则表明列表相等是可判定的。