如何在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語句按預期行爲。