types - Coq 数据类型冲突

Question

在 Coq 中重新定义自然数类型并尝试使用它时，如下所示：

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 发出错误

术语“1”具有“nat”类型，而预期具有“Nat”类型。

我理解这种行为的原因（实际数字 '1' 仍然映射到 Coq 的内置自然数类型），但有没有办法修复它？TIA。

Answer 1

最简单的解决方案当然是

Definition one := S O.

但是，由于您的类型与 完全相同nat，您可以声明强制转换。这看起来像

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.

这告诉 coqto_nat在获得 anat并期望 a时使用Nat。它可以让你做一些事情，比如使用+，以及特殊的数字文字。