diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | backend/SelectDivproof.v | 14 | ||||
| -rw-r--r-- | lib/Integers.v | 16 |
3 files changed, 17 insertions, 19 deletions
@@ -279,12 +279,8 @@ distclean: check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." -# Problems with coqchk (coq 8.6): -# Integers.Int.Z_mod_modulus_range takes forever to check -# compcert.backend.SelectDivproof.divs_mul_shift_2 takes forever to check - check-proof: $(FILES) - $(COQCHK) -admit compcert.lib.Integers -admit compcert.backend.SelectDivproof compcert.driver.Complements + $(COQCHK) compcert.driver.Complements print-includes: @echo $(COQINCLUDES) 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: 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 |