coq - 如何证明 Coq 中的 10%Z < Int.max_unsigned 和 Compcert 中的 Int 类型

Question

我想证明一个小于 Int.max_unsigned 的 Z 类型值。

引理检验：10%Z < Int.max_unsigned。证明。?? 如何证明上述测试引理？

Answer 1

CompCertInt.max_unsigned是根据许多其他概念定义的，例如Int.modulus,Int.wordsize和two_power_nat计算一些n2 次方的函数。通过一一展开这些定义并观察发生的情况，了解事物的组织方式具有指导意义：

unfold Int.max_unsigned.
(* 10 < Int.modulus - 1 *)
unfold Int.modulus.
(* 10 < two_power_nat Int.wordsize - 1 *)
unfold Int.wordsize.
(* 10 < two_power_nat Wordsize_32.wordsize - 1 *)

但这会变得无聊。一个更简单的证明是使用compute策略来评估Int.max_unsigned和与 10 进行比较：

Lemma test: 10%Z < Int.max_unsigned.
Proof.
  compute.
  (* The goal is now simply [Lt = Lt]. *)
  auto.
Qed.

Answer 2

这些简单的定理可以通过auto策略来证明。例子：

Require Import ZArith.

Open Scope Z_scope.

Lemma test: 10 < 111.
Proof.
  auto with zarith.
Qed.