如何在 coq 中定义教会数字的 exp ？

Question

感谢软件基金会的电子书，我目前正在学习 coq 。我成功地添加了如下内容：

Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition plus (n m : cnat) : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).

但由于以下错误，我坚持使用 exp：

Definition exp (n m : cnat) : cnat :=
  m cnat (mult n) n.
(*
In environment
n : cnat
m : cnat
The term "cnat" has type "Type@{cnat.u0+1}"
while it is expected to have type "Type@{cnat.u0}"
(universe inconsistency). 
*)

因为他们写道：

如果遇到“Universe 不一致”错误，请尝试迭代不同的类型。迭代 cnat 本身通常会出现问题。我尝试使用 cnat 的定义：

Definition exp (n m : cnat) : cnat :=
  m (forall X : Type, (X -> X) -> X) (mult n) n.

但后来我有：

In environment
n : cnat
m : cnat
The term "mult n" has type "cnat -> cnat"
while it is expected to have type
 "(forall X : Type, (X -> X) -> X) -> forall X : Type, (X -> X) -> X"
(universe inconsistency).

我不要求解决方案，但我真的很想了解这些错误。谢谢你的灯！

Answer 1

只需为陷入此问题的其他人发布解决方案即可。

Definition exp (n m : cnat) : cnat := 
  fun X => (m (X->X)) (n X).

关键是要理解m (X->X)。下图可能会有所帮助。

2^2的例子