如何证明10%Z <Coq中的Int <max.unsigned和Compcert中的Int类型

Question

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

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

Answer 1

CompCert Int.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.