coq - coq 中的模简化

Question

我是 Coq 的初学者，我在 Coq 中遇到了一个问题，我无法进一步简化这个问题。如果有人能提供有关如何将问题分解为更小的步骤的任何提示，那就太好了。引理是这样的:

forall (n : N) (n0 : N),

((1 + 2 * n + (2 * N.pos (2 ^ 32) - 1 - (0 + 2 * n0)))
 mod (2 * N.pos (2 ^ 32)) / (2 * 1)) mod N.pos (2 ^ 32) =
(((n + (N.pos (2 ^ 32) - 1 - n0)) mod N.pos (2 ^ 32) + 1 mod N.pos (2 ^ 32))
 mod N.pos (2 ^ 32) / 1) mod N.pos (2 ^ 32)

Answer 1

因此，您的目标无法证明，您可以尝试:

Goal exists (n : N) (n0 : N),
  ((1 + 2 * n + (2 * N.pos (2 ^ 32) - 1 - (0 + 2 * n0)))
  mod (2 * N.pos (2 ^ 32)) / (2 * 1)) mod N.pos (2 ^ 32) <>
  (((n + (N.pos (2 ^ 32) - 1 - n0)) mod N.pos (2 ^ 32) + 1 mod N.pos (2 ^ 32))
  mod N.pos (2 ^ 32) / 1) mod N.pos (2 ^ 32).
Proof.
  now exists 0, (N.pos 2^33).
Qed.

问题来自于正数之间的减法，当第二个参数较大时，它会返回 0，因此它不是单射的。