Merge pull request #33 from coq/use-make

Prepare the release of coq-bignums.8.11.0

.gitignore

@@ -14,3 +14,5 @@ Makefile.coq
 Makefile.coq.conf
 .merlin
 *.install
+*.vos
+*.vok

.travis.yml

@@ -50,3 +50,8 @@ matrix:
     - NJOBS=2
     <<: *OPAM
 
+  - env:
+    - COQ_IMAGE=coqorg/coq:8.11
+    - CONTRIB_NAME=coq-bignums
+    - NJOBS=2
+    <<: *OPAM

BigN/NMake.v

@@ -789,12 +789,12 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  intros x n; generalize x; elim n; clear n x; simpl pow_pos.
  intros; rewrite spec_mul; rewrite spec_square; rewrite H.
- rewrite Pos2Z.inj_xI; rewrite Zpower_exp; auto with zarith.
- rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith.
+ rewrite Pos2Z.inj_xI; rewrite Zpower_exp by auto with zarith.
+ rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r by auto with zarith.
  rewrite Z.pow_2_r; rewrite Z.pow_1_r; auto.
  intros; rewrite spec_square; rewrite H.
  rewrite Pos2Z.inj_xO; auto with zarith.
- rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r; auto with zarith.
+ rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r by auto with zarith.
  rewrite Z.pow_2_r; auto.
  intros; rewrite Z.pow_1_r; auto.
  Qed.
@@ -1281,9 +1281,9 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
    intros x y z HH HH1 HH2.
    split; auto with zarith.
-   apply Z.le_lt_trans with (2 := HH2); auto with zarith.
-   apply Zdiv_le_upper_bound; auto with zarith.
-   pattern x at 1; replace x with (x * 2 ^ 0); auto with zarith.
+   apply Z.le_lt_trans with (2 := HH2).
+   apply Zdiv_le_upper_bound. auto with zarith.
+   pattern x at 1; replace x with (x * 2 ^ 0).
    apply Z.mul_le_mono_nonneg_l; auto.
    apply Z.pow_le_mono_r; auto with zarith.
    rewrite Z.pow_0_r; ring.
@@ -1356,7 +1356,7 @@ Module Make (W0:CyclicType) <: NType.
  intros n x p K HK Hx Hp. simpl. rewrite spec_reduce.
  destruct (ZnZ.spec_to_Z x).
  destruct (ZnZ.spec_to_Z p).
- rewrite ZnZ.spec_add_mul_div by (omega with *).
+ rewrite ZnZ.spec_add_mul_div by (zify; omega).
  rewrite ZnZ.spec_0, Zdiv_0_l, Z.add_0_r.
  apply Zmod_small. unfold base.
  split; auto with zarith.
@@ -1373,7 +1373,7 @@ Module Make (W0:CyclicType) <: NType.
  intros.
  destruct (Z.eq_dec [x] 0) as [EQ|NEQ].
  (* [x] = 0 *)
- apply spec_unsafe_shiftl_aux with 0; auto with zarith.
+ apply spec_unsafe_shiftl_aux with 0. auto with zarith.
  now rewrite EQ.
  rewrite spec_head00 in *; auto with zarith.
  (* [x] <> 0 *)
@@ -1408,7 +1408,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  intros x. rewrite ! digits_level, double_size_level.
  rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower,
-         Nat2Z.inj_succ, Z.pow_succ_r; auto with zarith.
+         Nat2Z.inj_succ, Z.pow_succ_r by auto with zarith.
  ring.
  Qed.
 
@@ -1443,7 +1443,7 @@ Module Make (W0:CyclicType) <: NType.
      rewrite <- (fun x y z => Z.pow_add_r x (y - z)); auto with zarith.
      rewrite Z.sub_add.
      apply Z.le_trans with (2 := Z.lt_le_incl _ _ HH2).
-     apply Z.mul_le_mono_nonneg_l; auto with zarith.
+     apply Z.mul_le_mono_nonneg_l. auto with zarith.
      rewrite Z.pow_1_r; auto with zarith.
    - apply Z.pow_le_mono_r; auto with zarith.
      case (Z.le_gt_cases (Zpos (digits x)) [head0 x]); auto with zarith; intros HH6.
@@ -1484,7 +1484,7 @@ Module Make (W0:CyclicType) <: NType.
  generalize F3; rewrite <- (spec_double_size x); intros F4.
  absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))).
  { apply Z.le_ngt.
-   apply Z.pow_le_mono_r; auto with zarith.
+   apply Z.pow_le_mono_r. auto with zarith.
    rewrite Pos2Z.inj_xO; auto with zarith. }
  case (spec_head0 x F3).
  rewrite <- F1; rewrite Z.pow_0_r; rewrite Z.mul_1_l; intros _ HH.

BigN/Nbasic.v

@@ -338,7 +338,7 @@ Section CompareRec.
   symmetry. apply Z.gt_lt, Z.lt_gt. (* ;-) *)
   assert (0 < wB).
    unfold wB, DoubleBase.double_wB, base; auto with zarith.
-  change 0 with (0 + 0); apply Z.add_lt_le_mono; auto with zarith.
+  change 0 with (0 + 0); apply Z.add_lt_le_mono. 2: auto with zarith.
   apply Z.mul_pos_pos; auto with zarith.
   case (double_to_Z_pos n xl); auto with zarith.
   case (double_to_Z_pos n xh); intros; exfalso; omega.

BigN/gen/NMake_gen.ml

@@ -722,7 +722,7 @@ pr
  set (f' := fun n x y => (n, f n x y)).
  set (P' := fun z z' r => P (fst r) z z' (snd r)).
  assert (FST : forall x y, level x <= fst (same_level f' x y))
-  by (destruct x, y; simpl; omega with * ).
+  by (destruct x, y; simpl; zify; omega).
  assert (SND : forall x y, same_level f x y = snd (same_level f' x y))
   by (destruct x, y; reflexivity).
  intros. eapply Pantimon; [eapply FST|].

BigNumPrelude.v

@@ -19,6 +19,7 @@ Require Export ZArith.
 Require Export Znumtheory.
 Require Export Zpow_facts.
 Require Int63.
+Require Import Lia.
 
 Declare Scope bigN_scope.
 Declare Scope bigZ_scope.
@@ -73,40 +74,21 @@ Hint Resolve Z.lt_gt Z.le_ge Z_div_pos: zarith.
        a * beta + b <= c * beta + d ->
        0 <= b < beta -> 0 <= d < beta ->
        a <= c.
- Proof.
-  intros a b c d beta H1 (H3, H4) (H5, H6).
-  assert (a - c < 1); auto with zarith.
-  apply Z.mul_lt_mono_pos_r with beta; auto with zarith.
-  apply Z.le_lt_trans with (d  - b); auto with zarith.
-  rewrite Z.mul_sub_distr_r; auto with zarith.
- Qed.
+ Proof. nia. Qed.
 
  Theorem beta_lex_inv: forall a b c d beta,
       a < c -> 0 <= b < beta ->
       0 <= d < beta ->
       a * beta + b < c * beta  + d.
- Proof.
-  intros a b c d beta H1 (H3, H4) (H5, H6).
-  case (Z.le_gt_cases (c * beta + d) (a * beta + b)); auto with zarith.
-  intros H7. contradict H1. apply Z.le_ngt. apply beta_lex with (1 := H7); auto.
- Qed.
+ Proof. nia. Qed.
 
  Lemma beta_mult : forall h l beta,
    0 <= h < beta -> 0 <= l < beta -> 0 <= h*beta+l < beta^2.
- Proof.
-  intros h l beta H1 H2;split. auto with zarith.
-  rewrite <- (Z.add_0_r (beta^2)); rewrite Z.pow_2_r;
-   apply beta_lex_inv;auto with zarith.
- Qed.
+ Proof. nia. Qed.
 
  Lemma Zmult_lt_b :
    forall b x y, 0 <= x < b -> 0 <= y < b -> 0 <= x * y <= b^2 - 2*b + 1.
- Proof.
-  intros b x y (Hx1,Hx2) (Hy1,Hy2);split;auto with zarith.
-  apply Z.le_trans with ((b-1)*(b-1)).
-  apply Z.mul_le_mono_nonneg;auto with zarith.
-  apply Z.eq_le_incl; ring.
- Qed.
+ Proof. nia. Qed.
 
  Lemma sum_mul_carry : forall xh xl yh yl wc cc beta,
    1 < beta ->
@@ -118,54 +100,29 @@ Hint Resolve Z.lt_gt Z.le_ge Z_div_pos: zarith.
    0 <= cc < beta^2 ->
    wc*beta^2 + cc = xh*yl + xl*yh ->
    0 <= wc <= 1.
- Proof.
-  intros xh xl yh yl wc cc beta U H1 H2 H3 H4 H5 H6 H7.
-  assert (H8 := Zmult_lt_b beta xh yl H2 H5).
-  assert (H9 := Zmult_lt_b beta xl yh H3 H4).
-  split;auto with zarith.
-  apply beta_lex with (cc) (beta^2 - 2) (beta^2); auto with zarith.
- Qed.
+ Proof. nia. Qed.
 
  Theorem mult_add_ineq: forall x y cross beta,
    0 <= x < beta ->
    0 <= y < beta ->
    0 <= cross < beta ->
    0 <= x * y + cross < beta^2.
- Proof.
-  intros x y cross beta HH HH1 HH2.
-  split; auto with zarith.
-  apply Z.le_lt_trans with  ((beta-1)*(beta-1)+(beta-1)); auto with zarith.
-  apply Z.add_le_mono; auto with zarith.
-  apply Z.mul_le_mono_nonneg; auto with zarith.
-  rewrite ?Z.mul_sub_distr_l, ?Z.mul_sub_distr_r, Z.pow_2_r; auto with zarith.
- Qed.
+ Proof. nia. Qed.
 
  Theorem mult_add_ineq2: forall x y c cross beta,
    0 <= x < beta ->
    0 <= y < beta ->
    0 <= c*beta + cross <= 2*beta - 2 ->
    0 <= x * y + (c*beta + cross) < beta^2.
- Proof.
-  intros x y c cross beta HH HH1 HH2.
-  split; auto with zarith.
-  apply Z.le_lt_trans with ((beta-1)*(beta-1)+(2*beta-2));auto with zarith.
-  apply Z.add_le_mono; auto with zarith.
-  apply Z.mul_le_mono_nonneg; auto with zarith.
-  rewrite ?Z.mul_sub_distr_l, ?Z.mul_sub_distr_r, Z.pow_2_r; auto with zarith.
- Qed.
+ Proof. nia. Qed.
 
 Theorem mult_add_ineq3: forall x y c cross beta,
    0 <= x < beta ->
    0 <= y < beta ->
    0 <= cross <= beta - 2 ->
    0 <= c <= 1 ->
    0 <= x * y + (c*beta + cross) < beta^2.
- Proof.
-  intros x y c cross beta HH HH1 HH2 HH3.
-  apply mult_add_ineq2;auto with zarith.
-  split;auto with zarith.
-  apply Z.le_trans with (1*beta+cross);auto with zarith.
- Qed.
+ Proof. nia. Qed.
 
 Hint Rewrite Z.mul_1_r Z.mul_0_r Z.mul_1_l Z.mul_0_l Z.add_0_l Z.add_0_r Z.sub_0_r: rm10.
 

BigQ/QMake.v

@@ -310,11 +310,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
 
  Theorem spec_add : forall x y, [add x y] == [x] + [y].
  Proof.
- intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl;
-  auto with zarith.
+ intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl.
+ 1-2, 4, 6: lia.
  rewrite Pos.mul_1_r, Z2Pos.id; auto.
  rewrite Pos.mul_1_r, Z2Pos.id; auto.
- rewrite Z.mul_eq_0 in *; intuition.
  rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto.
  Qed.
 

BigZ/ZMake.v

@@ -232,7 +232,7 @@ Module Make (NN:NType) <: ZType.
  unfold add, to_Z; intros [x | x] [y | y];
    try (rewrite NN.spec_add; auto with zarith);
  rewrite NN.spec_compare; case Z.compare_spec;
-  unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *.
+  unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; zify; omega.
  Qed.
 
  Definition pred x :=
@@ -251,7 +251,7 @@ Module Make (NN:NType) <: ZType.
    try (rewrite NN.spec_succ; ring).
  rewrite NN.spec_compare; case Z.compare_spec;
   rewrite ?NN.spec_0, ?NN.spec_1, ?NN.spec_pred;
-  generalize (NN.spec_pos x); omega with *.
+  generalize (NN.spec_pos x); zify; omega.
  Qed.
 
  Definition sub x y :=
@@ -277,7 +277,7 @@ Module Make (NN:NType) <: ZType.
  unfold sub, to_Z; intros [x | x] [y | y];
   try (rewrite NN.spec_add; auto with zarith);
  rewrite NN.spec_compare; case Z.compare_spec;
-  unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *.
+  unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; zify; omega.
  Qed.
 
  Definition mul x y :=
@@ -438,7 +438,7 @@ Module Make (NN:NType) <: ZType.
  break_nonneg r pr EQr.
  subst; simpl. rewrite NN.spec_0; auto.
  subst. lazy iota beta delta [Z.eqb].
- rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *.
+ rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. zify; omega.
  (* Neg Pos *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
@@ -453,7 +453,7 @@ Module Make (NN:NType) <: ZType.
  break_nonneg r pr EQr.
  subst; simpl. rewrite NN.spec_0; auto.
  subst. lazy iota beta delta [Z.eqb].
- rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *.
+ rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. zify; omega.
  (* Neg Neg *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;

CyclicDouble/DoubleBase.v

@@ -208,11 +208,10 @@ Section DoubleBase.
    clear spec_w_0 w_0 spec_w_1 w_1 spec_w_Bm1 w_Bm1 spec_w_WW spec_w_0W
     spec_to_Z;unfold base.
    assert (2 ^ Zpos w_digits = 2 * (2 ^ (Zpos w_digits - 1))).
-   pattern 2 at 2; rewrite <- Z.pow_1_r.
-   rewrite <- Zpower_exp; auto with zarith.
-   f_equal; auto with zarith.
-   case w_digits; compute; intros; discriminate.
-   rewrite H; f_equal; auto with zarith.
+   { pattern 2 at 2; rewrite <- Z.pow_1_r.
+     rewrite <- Zpower_exp by Lia.lia.
+     f_equal; auto with zarith. }
+   rewrite H; f_equal.
    rewrite Z.mul_comm; apply Z_div_mult; auto with zarith.
   Qed.
 

CyclicDouble/DoubleCyclic.v

@@ -277,11 +277,11 @@ Section Z_2nZ.
 
  Let gcd_gt :=
   Eval lazy beta delta [ww_gcd_gt] in
-  ww_gcd_gt w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont.
+  ww_gcd_gt w_0 w_eq0 w_gcd_gt gcd_gt_fix gcd_cont _ww_digits.
 
  Let gcd :=
   Eval lazy beta delta [ww_gcd] in
-  ww_gcd compare w_0 w_eq0 w_gcd_gt _ww_digits gcd_gt_fix gcd_cont.
+  ww_gcd compare w_0 w_eq0 w_gcd_gt gcd_gt_fix gcd_cont _ww_digits.
 
  Definition lor (x y : zn2z t) :=
   match x, y with
@@ -635,7 +635,7 @@ Section Z_2nZ.
  Proof.
  refine (spec_ww_head00 w_0 w_0W
                 w_compare w_head0 w_add2 w_zdigits _ww_zdigits
-                w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); wwauto.
+                w_to_Z _ _ _ _ _ _ _ _ ); wwauto.
  exact ZnZ.spec_head00.
  exact ZnZ.spec_zdigits.
  Qed.
@@ -653,7 +653,7 @@ Section Z_2nZ.
  Proof.
  refine (spec_ww_tail00 w_0 w_0W
                 w_compare w_tail0 w_add2 w_zdigits _ww_zdigits
-                w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); wwauto.
+                w_to_Z _ _ _ _ _ _ _ _); wwauto.
  exact ZnZ.spec_tail00.
  exact ZnZ.spec_zdigits.
  Qed.
@@ -738,38 +738,38 @@ refine
 
  Let spec_ww_mod :  forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|].
  Proof.
-  refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);wwauto.
+  refine (spec_ww_mod w_digits compare mod_gt w_to_Z _ _ _);wwauto.
  Qed.
 
  Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] ->
       Zis_gcd [|a|] [|b|] [|gcd_gt a b|].
  Proof.
-  refine (@spec_ww_gcd_gt t w_digits W0 w_to_Z _
-    w_0 w_0 w_eq0 w_gcd_gt _ww_digits
-  _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
+  refine (@spec_ww_gcd_gt t w_digits w_to_Z _
+    w_0 w_eq0 w_gcd_gt
+  gcd_gt_fix _ _ _ _ gcd_cont _ _ww_digits _);wwauto.
   refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
    _ _ _ _ _   _ _ _ _ _   _ _ _ _ _   _ _ _ _ _);wwauto.
   exact ZnZ.spec_div21.
   exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
-  refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
+  refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_1 w_compare
    _ _);wwauto.
  Qed.
 
  Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].
  Proof.
-  refine (@spec_ww_gcd t w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt
-  _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
+  refine (@spec_ww_gcd t w_digits compare w_to_Z _ _ w_0 w_eq0 w_gcd_gt
+  gcd_gt_fix _ _ _ _ gcd_cont _ _ww_digits _);wwauto.
   refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
    _ _ _ _ _   _ _ _ _ _   _ _ _ _ _   _ _ _ _ _);wwauto.
   exact ZnZ.spec_div21.
   exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
-  refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
+  refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_1 w_compare
    _ _);wwauto.
  Qed.