Make the checker happy (AbsInt#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.

Author: vbgl

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)

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:

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