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

Question

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

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.

Answer 1

首先，list nats 的相等如下所示。请注意，多重匹配模式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.