时间戳

首页 > 解决方案 > 检查自然数列表对的相等性

coq - 检查自然数列表对的相等性

问题描述

我有两个自然数列表对，想检查它们是否相等。

Fixpoint beq_natlist (l1 l2 : list*list) : bool :=
 match l1, l2 with
| (nil , nil) => true
| (h :: nil, nil)  => false
| ( nil , h :: nil) => false
| h1 :: t1, h2 :: t2 => if beq_nat h1 h2 then beq_natlist t1 t2 else false

end.

标签： coq

解决方案

首先，s 的相等性list nat如下所示。请注意，多重匹配模式a, b和对表示法(a, b)是两个完全不同的东西。前者匹配两个术语，而后者匹配一个术语，它是一对。

Fixpoint beq_natlist (l1 l2 : list nat) : bool :=
  match l1, l2 with
  | nil, nil => true
  | h :: nil, nil => false
  | nil, h :: nil => false
  | h1 :: t1, h2 :: t2 => if beq_nat h1 h2 then beq_natlist t1 t2 else false
  end.

然后你可以使用beq_natlist来建立平等list nat * list nat：

Fixpoint beq_natlist_pair (p1 p2 : list nat * list nat) : bool :=
  match p1, p2 with
  | (l1, l2), (l3, l4) => beq_natlist l1 l3 && beq_natlist l2 l4
  end.

推荐阅读