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

Question

如何在fq（x）= 0的情况下定义函数，如f（x）= 0？

如果我做这样的事情在OСaml，

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

它抱怨

Error: The term i < 5 has type Prop which is not a (co-)inductive type.

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。事实上，它支持任何感应类型与两个构造函数，并使用then分支为第一个构造函数和else分支为第二个; bool和sumbool的定义都要小心地命令其构造函数使if语句按预期行为。