コアでナチュラルからナチュラルへの区分関数を定義する方法

Question

もしxの場合f（x）= 0の場合はどうすれば定義できますか？<もしそうでなければ、Coq？

私は、

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が論理的または命題バージョンである比較の決定可能バージョンを使用する必要があると文句を言い、OСamlのように何かをする場合あなたはそれで計算することはできません）。これは、標準ライブラリである：

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. 

あなたが証明してこの作業をするとき、あなたは何をi <? 5リターンについて推論するNat.ltb_ltのような定理を適用する必要があります。

Coqのif b then .. else ...は、bがboolまたはsumboolのいずれかをサポートしています。実際には、のいずれかの誘導型を2つのコンストラクタでサポートし、最初のコンストラクタにはthenブランチを使用し、2番目のコンストラクタにはelseブランチを使用します。 boolとsumboolの定義は、コンストラクターを注文してifステートメントを期待どおりに動作させるよう注意します。