Coq 数据类型冲突

【问题标题】：Coq data type clashesCoq 数据类型冲突
【发布时间】：2013-06-25 22:41:48
【问题描述】：

在 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。

【问题讨论】：

标签： types coq

【解决方案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.

这告诉 coq 使用 to_nat，只要它得到一个 nat 并期望一个 Nat。它可以让你做一些事情，比如使用+，以及特殊的数字文字。

【讨论】：