coq - 小于函数

Question

我正在通过 coq 课程“逻辑基础”。解决问题：

具有较少或相等的功能：

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

创建“小于”功能：

Definition blt_nat (n m : nat) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

据我了解，它应该像这样工作：

if (n == m)
   return false
else
    return (leb n m)

我创建了这个：

Definition blt_nat (n m : nat) : bool
  match n with
  | m => false
  | _ => leb n m
  end.

但它不起作用 - 输出：“错误：此子句是多余的。” 对于该行：

| _ => leb n m

请帮忙。

Answer 1

通过使用match ... with...end，我们可以检查特定数据类型的构造函数，并根据其构造函数找出它是如何构建的。因此，您不能将 nat 数据类型与另一个 nat 数据类型匹配。您可以在此处找到其他示例。

Definition blt_nat (n m : nat) : bool :=
  match m with
  | 0 => false
  | S m' => leb n m'
  end.