How can I define a function like f(x)=0 if x<5 otherwise f(x)=1 in Coq?
If I do something like in OСaml,
Definition test (i:nat):nat :=
if i < 5 then 0 else 1.
It complains that
Error: The term
i < 5has typePropwhich is not a (co-)inductive type.
You need to use a decidable version of the comparison (i < 5 is a logical or propositional version, which you can't compute with). This is in the standard library:
Require Import Arith.
Check lt_dec.
Definition test (i:nat) : nat := if lt_dec i 5 then 0 else 1.
The standard library's test for less than returns not a boolean but actually a sumbool, which includes proofs in both cases to tell you what the function does (these proofs go unused in your example, but would be handy if you wanted to prove something about test). The {n < m} + {~n < m} type you see in lt_dec's type is notation for sumbool (n < m) (~n < m).
If you didn't care about proofs, then you can use a different function, Nat.ltb, that returns a boolean. The standard library includes convenient notation for this function as well:
Require Import Arith.
Definition test (i:nat) : nat := if i <? 5 then 0 else 1.
When you work with this in proofs, you'll need to apply a theorem like Nat.ltb_lt to reason about what i <? 5 returns.
Note that the if b then .. else ... in Coq supports b being either a bool or a sumbool. In fact, it supports any inductive type with two constructors and uses the then branch for the first constructor and the else branch for the second; the definitions for bool and sumbool are careful to order their constructors to make if statements behave as expected.