diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2019-02-12 19:52:15 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-02-12 19:52:15 +0100 |
| commit | 873c62128ea8aeb2a26384be2be09b9324b9ed9c (patch) | |
| tree | 2694dc9aa9028568557aa84f10cdcc893b53fafe /lib/Integers.v | |
| parent | 0b3193b0019373305aec293362956bdb24cbb9a0 (diff) | |
| download | compcert-kvx-873c62128ea8aeb2a26384be2be09b9324b9ed9c.tar.gz compcert-kvx-873c62128ea8aeb2a26384be2be09b9324b9ed9c.zip | |
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.
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 16 |
1 files changed, 8 insertions, 8 deletions
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 |