如何在coq中定义从自然到自然的分段函数

Question

如果 x

如果我在 OСaml 中做类似的事情，

Definition test (i:nat):nat :=
  if i < 5 then 0 else 1.

它抱怨

错误：术语i < 5 的类型为Prop，它不是（共）归纳类型。

Answer 1

您需要使用比较的可判定 版本（i < 5 是逻辑或命题版本，您无法计算）。这是在标准库中：

Require Import Arith.
Check lt_dec.

Definition test (i:nat) : nat := if lt_dec i 5 then 0 else 1.

标准库对小于的测试返回的不是布尔值，而是一个 sumbool，其中包括两种情况下的证明，以告诉您函数的作用（这些证明在您的示例中未使用，但如果您想证明会很方便关于test)。您在lt_dec 的类型中看到的{n < m} + {~n < m} 类型是sumbool (n < m) (~n < m) 的符号。

如果您不关心证明，那么您可以使用不同的函数Nat.ltb，它返回一个布尔值。标准库也包含了这个函数的方便符号：

Require Import Arith.

Definition test (i:nat) : nat := if i <? 5 then 0 else 1.

当您在证明中使用它时，您需要应用像 Nat.ltb_lt 这样的定理来推断 i <? 5 返回的内容。

注意 Coq 中的 if b then .. else ... 支持 b 是 bool 或 sumbool。事实上，它支持 any 具有两个构造函数的归纳类型，第一个构造函数使用 then 分支，第二个构造函数使用 else 分支； bool 和 sumbool 的定义小心地命令它们的构造函数使 if 语句按预期运行。