如何在Coq中证明10%Z < Int.max_unsigned和Compcert中的整型

Question

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

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

Answer 1

CompCert的Int.max_unsigned是根据许多其他概念定义的，如Int.modulus、Int.wordsize和用于计算某些n的2次方的two_power_nat函数。通过逐个展开这些定义并观察发生了什么，了解事物是如何组织的是很有指导意义的：

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.