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.

3 files changed, 17 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index 308b75fd..c1b8d982 100644
--- a/Makefile
+++ b/Makefile
@@ -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