Coq data type clashes

Question

When redefining the natural number type in Coq and trying to use it, like so:

Inductive Nat: Type :=
| O: Nat
| S: Nat -> Nat.

Fixpoint plus (n: Nat) (m: Nat): Nat :=
match n with
    | O => m
    | S n' => S (plus n' m)
end.

Fixpoint mult (n: Nat) (m: Nat): Nat :=
match n with
    | O => O
    | S n' => plus m (mult n' m)
end.

Fixpoint factorial (n: Nat) : Nat :=
match n with
    | O => 1
    | (S n') => mult n (factorial n')
end.

Coq emits the error

The term "1" has type "nat" while it is expected to have type "Nat".

I understand the cause of this behaviour (the actual number '1' is still mapped to Coq's built-in natural number type) but is there a way of fixing it? TIA.

Answer 1

well the simplest solution is of course

Definition one := S O.

However, since your type is exactly the same as nat, you can declare a coercion. This would look like

Inductive Nat : Type :=
| O: Nat
| S: Nat -> Nat.
Fixpoint to_nat (n : nat) : Nat :=
  match n with
    | S n' => 1 + (to_nat n')
    | O => 0
  end.
Coercion to_nat : nat >-> Nat.

This tells coq to use to_nat whenever it gets a nat and expects a Nat. It let's you do things like use +, as well as the special numeric literals.