Merge remote-tracking branch 'origin/master' into stm+doc_hook

2 files changed, 57 insertions, 32 deletions

diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v
index 3b431d5b47..c03e6615cb 100644
--- a/theories/Numbers/Cyclic/Int63/Cyclic63.v
+++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v
@@ -177,21 +177,6 @@ Proof.
  inversion W;rewrite Zmult_comm;trivial.
 Qed.
 
-Lemma diveucl_21_spec_aux : forall a1 a2 b,
-      wB/2 <= [|b|] ->
-      [|a1|] < [|b|] ->
-      let (q,r) := diveucl_21 a1 a2 b in
-      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
-      0 <= [|r|] < [|b|].
-Proof.
- intros a1 a2 b H1 H2;assert (W:= diveucl_21_spec a1 a2 b).
- assert (W1:= to_Z_bounded a1).
- assert ([|b|]>0) by (auto with zarith).
- generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H).
- destruct (diveucl_21 a1 a2 b);destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]).
- inversion W;rewrite (Zmult_comm [|b|]);trivial.
-Qed.
-
 Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n ->
    ((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) =
    a mod 2 ^ p.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index eac26add03..3c96130bf3 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -387,7 +387,8 @@ Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y.
 
 Axiom diveucl_21_spec :  forall a1 a2 b,
    let (q,r) := diveucl_21 a1 a2 b in
-   ([|q|],[|r|]) = Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|].
+   let (q',r') := Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in
+   [|q|] = Z.modulo q' wB /\ [|r|] = r'.
 
 Axiom addmuldiv_def_spec : forall p x y,
   addmuldiv p x y = addmuldiv_def p x y.
@@ -1413,12 +1414,51 @@ Proof.
  apply Z.le_trans with ([|ih|] * wB)%Z;try rewrite Z.pow_2_r; auto with zarith.
 Qed.
 
-Lemma div2_phi ih il j:
-  [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|].
-Proof.
- generalize (diveucl_21_spec ih il j).
- case diveucl_21; intros q r Heq.
- simpl zn2z_to_Z;unfold Z.div;rewrite <- Heq;trivial.
+Lemma diveucl_21_spec_aux : forall a1 a2 b,
+      wB/2 <= [|b|] ->
+      [|a1|] < [|b|] ->
+      let (q,r) := diveucl_21 a1 a2 b in
+      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
+      0 <= [|r|] < [|b|].
+Proof.
+ intros a1 a2 b H1 H2;assert (W:= diveucl_21_spec a1 a2 b).
+ assert (W1:= to_Z_bounded a1).
+ assert (W2:= to_Z_bounded a2).
+ assert (Wb:= to_Z_bounded b).
+ assert ([|b|]>0) by (auto with zarith).
+ generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H).
+ revert W.
+ destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]).
+ intros (H', H''); rewrite H', H''; clear H' H''.
+ intros (H', H''); split; [ |exact H''].
+ rewrite H', Zmult_comm, Z.mod_small; [reflexivity| ].
+ split.
+ { revert H'; case z; [now simpl..|intros p H'].
+   exfalso; apply (Z.lt_irrefl 0), (Z.le_lt_trans _ ([|a1|] * wB + [|a2|])).
+   { now apply Z.add_nonneg_nonneg; [apply Z.mul_nonneg_nonneg| ]. }
+   rewrite H'; apply (Zplus_lt_reg_r _ _ (- z0)); ring_simplify.
+   apply (Z.le_lt_trans _ (- [|b|])); [ |now auto with zarith].
+   rewrite Z.opp_eq_mul_m1; apply Zmult_le_compat_l; [ |now apply Wb].
+   rewrite <-!Pos2Z.opp_pos, <-Z.opp_le_mono.
+   now change 1 with (Z.succ 0); apply Zlt_le_succ. }
+ rewrite <-Z.nle_gt; intro Hz; revert H2; apply Zle_not_lt.
+ rewrite (Z.div_unique_pos (wB * [|a1|] + [|a2|]) wB [|a1|] [|a2|]);
+   [ |now simpl..].
+ rewrite Z.mul_comm, H'.
+ rewrite (Z.div_unique_pos (wB * [|b|] + z0) wB [|b|] z0) at 1;
+   [ |split; [ |apply (Z.lt_trans _ [|b|])]; now simpl|reflexivity].
+ apply Z_div_le; [now simpl| ]; rewrite Z.mul_comm; apply Zplus_le_compat_r.
+ now apply Zmult_le_compat_l.
+Qed.
+
+Lemma div2_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] ->
+  [|fst (diveucl_21 ih il j)|] = [|| WW ih il||] /[|j|])%Z.
+Proof.
+ intros Hj Hj1.
+ generalize (diveucl_21_spec_aux ih il j Hj Hj1).
+ case diveucl_21; intros q r (Hq, Hr).
+ apply Zdiv_unique with [|r|]; auto with zarith.
+ simpl @fst; apply eq_trans with (1 := Hq); ring.
 Qed.
 
 Lemma sqrt2_step_correct rec ih il j:
@@ -1436,9 +1476,9 @@ Proof.
  case (to_Z_bounded il); intros Hil1 _.
  case (to_Z_bounded j); intros _ Hj1.
  assert (Hp3: (0 < [||WW ih il||])).
-  simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith.
+ {simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith.
   apply Zmult_lt_0_compat; auto with zarith.
-  refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith.
+  refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. }
  cbv zeta.
  case_eq (ih < j)%int63;intros Heq.
  rewrite -> ltb_spec in Heq.
@@ -1450,28 +1490,28 @@ Proof.
  2: rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith.
  case (Zle_or_lt (2^(Z_of_nat size -1)) [|j|]); intros Hjj.
  case_eq (fst (diveucl_21 ih il j) < j)%int63;intros Heq0.
- 2: rewrite <-not_true_iff_false, ltb_spec, div2_phi in Heq0.
+ 2: rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0.
  2: split; auto; apply sqrt_test_true; auto with zarith.
- rewrite -> ltb_spec, div2_phi in Heq0.
+ rewrite -> ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0.
  match goal with |- context[rec _ _ ?X] =>
   set (u := X)
  end.
  assert (H: [|u|] = ([|j|] + ([||WW ih il||])/([|j|]))/2).
-  unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j)));
-  case addc;unfold interp_carry;rewrite div2_phi;simpl zn2z_to_Z.
-  intros i H;rewrite lsr_spec, H;trivial.
+ { unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j)));
+  case addc;unfold interp_carry;rewrite (div2_phi _ _ _ Hjj Heq);simpl zn2z_to_Z.
+  { intros i H;rewrite lsr_spec, H;trivial. }
   intros i H;rewrite <- H.
   case (to_Z_bounded i); intros H1i H2i.
   rewrite -> add_spec, Zmod_small, lsr_spec.
-  change (1 * wB) with ([|(1 << (digits -1))|] * 2)%Z.
-  rewrite Z_div_plus_full_l; auto with zarith.
+  { change (1 * wB) with ([|(1 << (digits -1))|] * 2)%Z.
+    rewrite Z_div_plus_full_l; auto with zarith. }
   change wB with (2 * (wB/2))%Z; auto.
   replace [|(1 << (digits - 1))|] with (wB/2); auto.
   rewrite lsr_spec; auto.
   replace (2^[|1|]) with 2%Z; auto.
   split; auto with zarith.
   assert ([|i|]/2 < wB/2); auto with zarith.
-  apply Zdiv_lt_upper_bound; auto with zarith.
+  apply Zdiv_lt_upper_bound; auto with zarith. }
  apply Hrec; rewrite H; clear u H.
  assert (Hf1: 0 <= [||WW ih il||]/ [|j|]) by (apply Z_div_pos; auto with zarith).
  case (Zle_lt_or_eq 1 ([|j|])); auto with zarith; intros Hf2.