coq - 在 Coq 中处理多个整数库？

Question

我经常得到以下形式的证明条款：

Lemma of_nat_gt_0: forall (n: nat),
(Z.of_nat n >=? Int32.unsigned (Int32.repr 0)) = true.

该定理显然是正确的（自然的 Z 将始终为>= 0。同样，unsignedarepr的 a0将屈服0。

但是，它们很烦人，因为我需要处理

1. Int32从CompCert.Integers模块
2. Z.of_nat转换。

通常，我也有术语Pos和N定义。

这些证明涉及多次手动重写以适应某种标准形式，然后是omega调用。

有没有办法将所有这些“规范化”为一个统一的表示？

我知道这隐含地涉及在不同环之间转移（例如Int32is Z/(2^32 - 1)）。如果有某种方法可以解决这个问题，那就太好了，因为这些证明会变得非常长。

标签： coqcoq-tactic