小于函数答案

【问题标题】：Less then function小于函数
【发布时间】：2018-12-31 14:11:43
【问题描述】：

我正在通过 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.

创建“小于”函数：

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

请帮忙。

【问题讨论】：

我对@987654328@ 没有经验，但我怀疑第一种情况| m => ... 与m 不匹配，但匹配任何值并调用该值m（覆盖原m)。这可能会有所帮助：stackoverflow.com/a/46384468

标签： coq logical-foundations

【解决方案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.

【讨论】：