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 /backend/SelectDivproof.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 'backend/SelectDivproof.v')
| -rw-r--r-- | backend/SelectDivproof.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 75713289..9e24857a 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -283,14 +283,15 @@ Proof. intros (A & B & C). split. auto. rewrite C. f_equal. f_equal. rewrite Int.add_signed. unfold Int.mulhs. set (n := Int.signed x). transitivity (Int.repr (n * (m - Int.modulus) / Int.modulus + n)). - f_equal. + apply f_equal. replace (n * (m - Int.modulus)) with (n * m + (-n) * Int.modulus) by ring. rewrite Z_div_plus. ring. apply Int.modulus_pos. apply Int.eqm_samerepr. apply Int.eqm_add; auto with ints. apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned. - apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. f_equal. f_equal. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. + apply (f_equal (fun x => n * x / Int.modulus)). rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption. - apply zlt_false. omega. + apply zlt_false. assumption. Qed. Theorem divu_mul_shift: @@ -436,14 +437,15 @@ Proof. intros (A & B & C). split. auto. rewrite C. f_equal. f_equal. rewrite Int64.add_signed. unfold Int64.mulhs. set (n := Int64.signed x). transitivity (Int64.repr (n * (m - Int64.modulus) / Int64.modulus + n)). - f_equal. + apply f_equal. replace (n * (m - Int64.modulus)) with (n * m + (-n) * Int64.modulus) by ring. rewrite Z_div_plus. ring. apply Int64.modulus_pos. apply Int64.eqm_samerepr. apply Int64.eqm_add; auto with ints. apply Int64.eqm_sym. eapply Int64.eqm_trans. apply Int64.eqm_signed_unsigned. - apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2. f_equal. f_equal. + apply Int64.eqm_unsigned_repr_l. apply Int64.eqm_refl2. + apply (f_equal (fun x => n * x / Int64.modulus)). rewrite Int64.signed_repr_eq. rewrite Zmod_small by assumption. - apply zlt_false. omega. + apply zlt_false. assumption. Qed. Remark int64_shru'_div_two_p: |