在 Coq 中将 nat 转换为 Q
Conversion of nat to Q in Coq
如何在 Coq 中将 nat 转换为 Q（有理数）？
我希望能够写出这样的东西：
Require Import Coq.QArith.QArith.
Open Scope Q_scope.
Definition a := 2/3.
当我尝试这样做时，Coq 告诉我：
Error: The term "2" has type "nat" while it is expected to have type "Q".
你可以这样写：
Definition a := Z.of_nat 2 # Pos.of_nat 3.
# 运算符只是 Q 类型的 Qmake 构造函数的符号。该构造函数将 Z 和 positive 的元素作为参数，因此您需要强制转换才能将 nat 放入其中。
如果您使用文字数字语法，您也可以直接使用 Z 和 positive：
Definition a := 2 # 3.
区别是这个定义不会提到nat的转换；数字已经是正确的类型，因为 Coq 直接将数字符号解释为 Z 和 positive。
我个人不是很喜欢标准的Coq有理数库，因为它使用的是等价性而不是莱布尼茨等式；也就是说，Q 1 # 1 和 2 # 2 的元素等价于有理数，但根据 Coq 等式不相等：
Goal (1 # 1 <> 2 # 2).
congruence.
Qed.
有一个名为 setoid rewrite 的功能可以让您假装它们是相等的。它的工作原理是只允许您重写已证明与 Q 上的等价概念兼容的函数。但是，还是有比莱布尼兹等式更难用的情况。
您也可以尝试 Ssreflect and MathComp packages (see the documentation here) 的 rat 库。它有一个与莱布尼兹等式一起工作的有理数定义，比 Coq 的更全面。
如何在 Coq 中将 nat 转换为 Q（有理数）？
我希望能够写出这样的东西：
Require Import Coq.QArith.QArith.
Open Scope Q_scope.
Definition a := 2/3.
当我尝试这样做时，Coq 告诉我：
Error: The term "2" has type "nat" while it is expected to have type "Q".
你可以这样写：
Definition a := Z.of_nat 2 # Pos.of_nat 3.
# 运算符只是 Q 类型的 Qmake 构造函数的符号。该构造函数将 Z 和 positive 的元素作为参数，因此您需要强制转换才能将 nat 放入其中。
如果您使用文字数字语法，您也可以直接使用 Z 和 positive：
Definition a := 2 # 3.
区别是这个定义不会提到nat的转换；数字已经是正确的类型，因为 Coq 直接将数字符号解释为 Z 和 positive。
我个人不是很喜欢标准的Coq有理数库，因为它使用的是等价性而不是莱布尼茨等式；也就是说，Q 1 # 1 和 2 # 2 的元素等价于有理数，但根据 Coq 等式不相等：
Goal (1 # 1 <> 2 # 2).
congruence.
Qed.
有一个名为 setoid rewrite 的功能可以让您假装它们是相等的。它的工作原理是只允许您重写已证明与 Q 上的等价概念兼容的函数。但是，还是有比莱布尼兹等式更难用的情况。
您也可以尝试 Ssreflect and MathComp packages (see the documentation here) 的 rat 库。它有一个与莱布尼兹等式一起工作的有理数定义，比 Coq 的更全面。