Less then函数

Question

我正在通过coq课程"Logical Foundations"。解决问题：

具有较少或相等功能的：

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.

创建"less then“函数：

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的另一个数据类型进行匹配。您可以在here中找到其他示例。

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