0

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?

haiyong
  • 21
  • 2

2 Answers2

5

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.
Isabelle Newbie
  • 9,258
  • 1
  • 20
  • 32
0

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.
mpetruska
  • 633
  • 3
  • 6
  • 2
    This doesn't work in the OP's case because `Int.max_unsigned` from the CompCert library is not a constant like `111` is. See my answer. – Isabelle Newbie Feb 07 '18 at 16:33
  • Right, need to do a `compute; reflexivity`. Was not aware of the complication behind `Int.max_unsigned`, thanks. – mpetruska Feb 07 '18 at 16:41