实数的形式化 #5 整数

    在自然数的部分中，我们定义的自然数的减法满足：当 a < b 时，a - b = 0。这使得自然数的减法的性质具有局限性，经常需要分类讨论。为了得到性质更完整、更合理的减法，我们需要引入整数。

    现在，我们假设已经声明了整数类型 Z 和输出整数的自然数的减法 "-" : nat -> nat -> Z。我们希望任何整数都可以表示成两个自然数相减的形式。除此之外，还需要让 a "-" b = c "-" d 当且仅当 a + d = b + c。基于这些需求，我们可以像构造基数一样，通过等价类构造整数。

    我们首先定义 nat * nat 上的等价关系 Zeq，从这个等价关系出发即可构造出类型 Z。对于自然数 a 和 b，Z_make (a,b) 是整数。Z_make 相当于之前假设中的 "-"。对于整数 x，Z构造NN x 是两个自然数组成的有序对，满足 Z_make (Z构造NN x) = x。

    对于自然数 n，Z_make (n,0) 可以被视为 n 自然对应的整数，这里记作 n.z。

    对于整数的加法，我们希望 Z_make (a,b) + Z_make (c,d) = Z_make (a+c,b+d)。具体定义与性质如下：

    对于整数 x，我们可以定义它的相反数 - x。我们希望 - Z_make (a,b) = Z_make (b,a)。具体定义与性质如下：

    现在我们可以定义整数的减法。对于整数 x 和 y，我们定义 x - y = x + (- y) 。这与 Z_make 一致。

    在以上定理中我们可以看出，整数的加减法能够能够完美地交融在一起，这是自然数的加减法所不具备的。

    我们还可以定义整数的乘法，这比整数的加法更复杂。

    对于整数 x，x 是正数当且仅当 x 是某个非零自然数自然对应的整数；x 是负数当且仅当 x 是某个非零自然数自然对应的整数的相反数。可以证明：一个整数要么是正数，要么是负数，要么是 0.z。

    利用以上性质可以证明：