diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 44 |
1 files changed, 14 insertions, 30 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 08f05bbf..cd55f9d8 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -97,8 +97,7 @@ Section POS_MOD. assert (HHHHH:= lt_0_wB w_digits). assert (F0: forall x y, x - y + y = x); auto with zarith. intros w1 p; case (spec_to_w_Z p); intros HH1 HH2. - unfold ww_pos_mod; case w1. - simpl; rewrite Zmod_small; split; auto with zarith. + unfold ww_pos_mod; case w1. reflexivity. intros xh xl; rewrite spec_ww_compare. case Z.compare_spec; rewrite spec_w_0W; rewrite spec_zdigits; fold wB; @@ -211,8 +210,7 @@ Section DoubleDiv32. Variable w_div21 : w -> w -> w -> w*w. Variable ww_sub_c : zn2z w -> zn2z w -> carry (zn2z w). - Definition w_div32 a1 a2 a3 b1 b2 := - Eval lazy beta iota delta [ww_add_c_cont ww_add] in + Definition w_div32_body a1 a2 a3 b1 b2 := match w_compare a1 b1 with | Lt => let (q,r) := w_div21 a1 a2 b1 in @@ -233,6 +231,10 @@ Section DoubleDiv32. | Gt => (w_0, W0) (* cas absurde *) end. + Definition w_div32 a1 a2 a3 b1 b2 := + Eval lazy beta iota delta [ww_add_c_cont ww_add w_div32_body] in + w_div32_body a1 a2 a3 b1 b2. + (* Proof *) Variable w_digits : positive. @@ -242,14 +244,14 @@ Section DoubleDiv32. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + (interp_carry 1 wB w_to_Z c) (at level 0, c at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Variable spec_w_0 : [|w_0|] = 0. @@ -312,26 +314,8 @@ Section DoubleDiv32. assert (U:= lt_0_wB w_digits); assert (U1:= lt_0_wwB w_digits). Spec_w_to_Z a1;Spec_w_to_Z a2;Spec_w_to_Z a3;Spec_w_to_Z b1;Spec_w_to_Z b2. rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Z.mul_assoc;rewrite <- Z.mul_add_distr_r. - change (w_div32 a1 a2 a3 b1 b2) with - match w_compare a1 b1 with - | Lt => - let (q,r) := w_div21 a1 a2 b1 in - match ww_sub_c (w_WW r a3) (w_mul_c q b2) with - | C0 r1 => (q,r1) - | C1 r1 => - let q := w_pred q in - ww_add_c_cont w_WW w_add_c w_add_carry_c - (fun r2=>(w_pred q, ww_add w_add_c w_add w_add_carry r2 (WW b1 b2))) - (fun r2 => (q,r2)) - r1 (WW b1 b2) - end - | Eq => - ww_add_c_cont w_WW w_add_c w_add_carry_c - (fun r => (w_Bm2, ww_add w_add_c w_add w_add_carry r (WW b1 b2))) - (fun r => (w_Bm1,r)) - (WW (w_sub a2 b2) a3) (WW b1 b2) - | Gt => (w_0, W0) (* cas absurde *) - end. + change (w_div32 a1 a2 a3 b1 b2) with (w_div32_body a1 a2 a3 b1 b2). + unfold w_div32_body. rewrite spec_compare. case Z.compare_spec; intro Hcmp. simpl in Hlt. rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega. @@ -520,7 +504,7 @@ Section DoubleDiv21. Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). Notation "[-[ c ]]" := (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, x at level 99). + (at level 0, c at level 99). Variable spec_w_0 : [|w_0|] = 0. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. @@ -782,7 +766,7 @@ Section DoubleDivGt. Notation wwB := (base (ww_digits w_digits)). Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). |