how ot proof 10%Z < Int.max_unsigned in Coq and the Int type from Compcert

Question

I want to proof a Z type value less than Int.max_unsigned.

Lemma test: 10%Z < Int.max_unsigned. Proof. ?? How to prove the above test lemma?

Answer 1

These simple theorems can be proved by the auto tactic. Example:

Require Import ZArith.

Open Scope Z_scope.

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

Answer 2

CompCert's Int.max_unsigned is defined in terms of a lot of other concepts like Int.modulus, Int.wordsize, and the two_power_nat function for calculating some n to the power of 2. It's instructive to understand how things are organized by unfolding each of these definitions one by one and observing what happens:

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 *)

But this gets boring. A simpler proof is to use the compute tactic to evaluate Int.max_unsigned and the comparison against 10:

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