Как доказать 10%Z <Int.max_unsigned в Coq и тип Int из Compcert

Question

Я хочу доказать значение Z-типа меньше, чем Int.max_unsigned.

Тест леммы: 10%Z

Answer 1

CompCert-х Int.max_unsigned определяется с точки зрения многих других понятий, таких как Int.modulus, Int.wordsizeи two_power_nat функция для расчета некоторых n до степени 2. Поучительно понять, как все организовано, развернув каждое из этих определений одно за другим и наблюдая за тем, что происходит:

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.