From 873c62128ea8aeb2a26384be2be09b9324b9ed9c Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 12 Feb 2019 19:52:15 +0100 Subject: Make the checker happy (#272) Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0. --- lib/Integers.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index a905a7d1..0e506208 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -150,19 +150,19 @@ Lemma Z_mod_modulus_range: Proof. intros; unfold Z_mod_modulus. destruct x. - - generalize modulus_pos; omega. + - generalize modulus_pos; intuition. - apply P_mod_two_p_range. - set (r := P_mod_two_p p wordsize). assert (0 <= r < modulus) by apply P_mod_two_p_range. destruct (zeq r 0). - + generalize modulus_pos; omega. - + omega. + + generalize modulus_pos; intuition. + + Psatz.lia. Qed. Lemma Z_mod_modulus_range': forall x, -1 < Z_mod_modulus x < modulus. Proof. - intros. generalize (Z_mod_modulus_range x); omega. + intros. generalize (Z_mod_modulus_range x); intuition. Qed. Lemma Z_mod_modulus_eq: @@ -178,10 +178,10 @@ Proof. set (r := P_mod_two_p p wordsize) in *. rewrite <- B in C. change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0). - + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. ring. - generalize modulus_pos; omega. - + symmetry. apply Zmod_unique with (-q - 1). rewrite C. ring. - omega. + + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. Psatz.lia. + intuition. + + symmetry. apply Zmod_unique with (-q - 1). rewrite C. Psatz.lia. + intuition. Qed. (** The [unsigned] and [signed] functions return the Coq integer corresponding -- cgit