# Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv

Set Implicit Arguments.
Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Require Import DoubleDivn1.
Require Import DoubleAdd.
Require Import DoubleSub.
Local Open Scope Z_scope.
Ltac zarith := auto with zarith.
Section POS_MOD.
Variable w:Type.
Variable w_0 : w.
Variable w_digits : positive.
Variable w_zdigits : w.
Variable w_WW : w -> w -> zn2z w.
Variable w_pos_mod : w -> w -> w.
Variable w_compare : w -> w -> comparison.
Variable ww_compare : zn2z w -> zn2z w -> comparison.
Variable w_0W : w -> zn2z w.
Variable low: zn2z w -> w.
Variable ww_sub: zn2z w -> zn2z w -> zn2z w.
Variable ww_zdigits : zn2z w.
Definition ww_pos_mod p x :=
let zdigits := w_0W w_zdigits in
match x with
| W0 => W0
| WW xh xl =>
match ww_compare p zdigits with
| Eq => w_WW w_0 xl
| Lt => w_WW w_0 (w_pos_mod (low p) xl)
| Gt =>
match ww_compare p ww_zdigits with
| Lt =>
let n := low (ww_sub p zdigits) in
w_WW (w_pos_mod n xh) xl
| _ => x
end
end
end.
Variable w_to_Z : w -> Z.
Notation wB := (base w_digits).
Notation wwB := (base (ww_digits w_digits)).
Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99).
Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
Variable spec_w_0 : [| w_0 |] = 0.
Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_to_w_Z : forall x, 0 <= [[ x ]] < wwB.
Variable spec_w_WW : forall h l, [[ w_WW h l ]] = [| h |] * wB + [| l |].
Variable spec_pos_mod : forall w p,
[| w_pos_mod p w |] = [| w |] mod (2 ^ [| p |] ).
Variable spec_w_0W : forall l, [[ w_0W l ]] = [| l |].
Variable spec_ww_compare : forall x y,
ww_compare x y = Z.compare [[ x ]] [[ y ]].
Variable spec_ww_sub: forall x y,
[[ ww_sub x y ]] = ( [[ x ]] - [[ y ]] ) mod wwB.
Variable spec_zdigits : [| w_zdigits |] = Zpos w_digits.
Variable spec_low: forall x, [| low x |] = [[ x ]] mod wB.
Variable spec_ww_zdigits : [[ ww_zdigits ]] = 2 * [| w_zdigits |].
Variable spec_ww_digits : ww_digits w_digits = xO w_digits.
Hint Rewrite spec_w_0 spec_w_WW : w_rewrite.
Lemma spec_ww_pos_mod : forall w p,
[[ ww_pos_mod p w ]] = [[ w ]] mod (2 ^ [[ p ]] ).
End POS_MOD.
Section DoubleDiv32.
Variable w : Type.
Variable w_0 : w.
Variable w_Bm1 : w.
Variable w_Bm2 : w.
Variable w_WW : w -> w -> zn2z w.
Variable w_compare : w -> w -> comparison.
Variable w_add_c : w -> w -> carry w.
Variable w_add_carry_c : w -> w -> carry w.
Variable w_add : w -> w -> w.
Variable w_add_carry : w -> w -> w.
Variable w_pred : w -> w.
Variable w_sub : w -> w -> w.
Variable w_mul_c : w -> w -> zn2z w.
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
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 )
end.
Variable w_digits : positive.
Variable w_to_Z : w -> Z.
Notation wB := (base w_digits).
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).
Notation "[-| c |]" :=
(interp_carry (-1) wB w_to_Z c) (at level 0, x 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).
Variable spec_w_0 : [| w_0 |] = 0.
Variable spec_w_Bm1 : [| w_Bm1 |] = wB - 1.
Variable spec_w_Bm2 : [| w_Bm2 |] = wB - 2.
Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_w_WW : forall h l, [[ w_WW h l ]] = [| h |] * wB + [| l |].
Variable spec_compare :
forall x y, w_compare x y = Z.compare [| x |] [| y |].
Variable spec_w_add_c : forall x y, [+| w_add_c x y |] = [| x |] + [| y |].
Variable spec_w_add_carry_c :
forall x y, [+| w_add_carry_c x y |] = [| x |] + [| y |] + 1.
Variable spec_w_add : forall x y, [| w_add x y |] = ( [| x |] + [| y |] ) mod wB.
Variable spec_w_add_carry :
forall x y, [| w_add_carry x y |] = ( [| x |] + [| y |] + 1) mod wB.
Variable spec_pred : forall x, [| w_pred x |] = ( [| x |] - 1) mod wB.
Variable spec_sub : forall x y, [| w_sub x y |] = ( [| x |] - [| y |] ) mod wB.
Variable spec_mul_c : forall x y, [[ w_mul_c x y ]] = [| x |] * [| y |].
Variable spec_div21 : forall a1 a2 b,
wB /2 <= [| b |] ->
[| a1 |] < [| b |] ->
let (q,r) := w_div21 a1 a2 b in
[| a1 |] * wB + [| a2 |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Variable spec_ww_sub_c : forall x y, [-[ ww_sub_c x y ]] = [[ x ]] - [[ y ]].
Ltac Spec_w_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Theorem wB_div2: forall x, wB /2 <= x -> wB <= 2 * x.
Lemma Zmult_lt_0_reg_r_2 : forall n m : Z, 0 <= n -> 0 < m * n -> 0 < m.
Theorem spec_w_div32 : forall a1 a2 a3 b1 b2,
wB /2 <= [| b1 |] ->
[[ WW a1 a2 ]] < [[ WW b1 b2 ]] ->
let (q,r) := w_div32 a1 a2 a3 b1 b2 in
[| a1 |] * wwB + [| a2 |] * wB + [| a3 |] =
[| q |] * ( [| b1 |] * wB + [| b2 |] ) + [[ r ]] /\
0 <= [[ r ]] < [| b1 |] * wB + [| b2 |].
End DoubleDiv32.
Section DoubleDiv21.
Variable w : Type.
Variable w_0 : w.
Variable w_0W : w -> zn2z w.
Variable w_div32 : w -> w -> w -> w -> w -> w * zn2z w.
Variable ww_1 : zn2z w.
Variable ww_compare : zn2z w -> zn2z w -> comparison.
Variable ww_sub : zn2z w -> zn2z w -> zn2z w.
Definition ww_div21 a1 a2 b :=
match a1 with
| W0 =>
match ww_compare a2 b with
| Gt => ( ww_1 , ww_sub a2 b )
| Eq => ( ww_1 , W0 )
| Lt => ( W0 , a2 )
end
| WW a1h a1l =>
match a2 with
| W0 =>
match b with
| W0 => ( W0 , W0 )
| WW b1 b2 =>
let (q1, r) := w_div32 a1h a1l w_0 b1 b2 in
match r with
| W0 => ( WW q1 w_0 , W0 )
| WW r1 r2 =>
let (q2, s) := w_div32 r1 r2 w_0 b1 b2 in
( WW q1 q2 , s )
end
end
| WW a2h a2l =>
match b with
| W0 => ( W0 , W0 )
| WW b1 b2 =>
let (q1, r) := w_div32 a1h a1l a2h b1 b2 in
match r with
| W0 => ( WW q1 w_0 , w_0W a2l )
| WW r1 r2 =>
let (q2, s) := w_div32 r1 r2 a2l b1 b2 in
( WW q1 q2 , s )
end
end
end
end.
Variable w_digits : positive.
Variable w_to_Z : w -> Z.
Notation wB := (base w_digits).
Notation wwB := (base (ww_digits w_digits)).
Notation "[| x |]" := (w_to_Z x) (at level 0, x 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).
Variable spec_w_0 : [| w_0 |] = 0.
Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_w_0W : forall l, [[ w_0W l ]] = [| l |].
Variable spec_w_div32 : forall a1 a2 a3 b1 b2,
wB /2 <= [| b1 |] ->
[[ WW a1 a2 ]] < [[ WW b1 b2 ]] ->
let (q,r) := w_div32 a1 a2 a3 b1 b2 in
[| a1 |] * wwB + [| a2 |] * wB + [| a3 |] =
[| q |] * ( [| b1 |] * wB + [| b2 |] ) + [[ r ]] /\
0 <= [[ r ]] < [| b1 |] * wB + [| b2 |].
Variable spec_ww_1 : [[ ww_1 ]] = 1.
Variable spec_ww_compare : forall x y,
ww_compare x y = Z.compare [[ x ]] [[ y ]].
Variable spec_ww_sub : forall x y, [[ ww_sub x y ]] = ( [[ x ]] - [[ y ]] ) mod wwB.
Theorem wwB_div: wwB = 2 * ( wwB / 2).
Ltac Spec_w_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Theorem spec_ww_div21 : forall a1 a2 b,
wwB /2 <= [[ b ]] ->
[[ a1 ]] < [[ b ]] ->
let (q,r) := ww_div21 a1 a2 b in
[[ a1 ]] * wwB + [[ a2 ]] = [[ q ]] * [[ b ]] + [[ r ]] /\ 0 <= [[ r ]] < [[ b ]].
End DoubleDiv21.
Section DoubleDivGt.
Variable w : Type.
Variable w_digits : positive.
Variable w_0 : w.
Variable w_WW : w -> w -> zn2z w.
Variable w_0W : w -> zn2z w.
Variable w_compare : w -> w -> comparison.
Variable w_eq0 : w -> bool.
Variable w_opp_c : w -> carry w.
Variable w_opp w_opp_carry : w -> w.
Variable w_sub_c : w -> w -> carry w.
Variable w_sub w_sub_carry : w -> w -> w.
Variable w_div_gt : w -> w -> w * w.
Variable w_mod_gt : w -> w -> w.
Variable w_gcd_gt : w -> w -> w.
Variable w_add_mul_div : w -> w -> w -> w.
Variable w_head0 : w -> w.
Variable w_div21 : w -> w -> w -> w * w.
Variable w_div32 : w -> w -> w -> w -> w -> w * zn2z w.
Variable _ww_zdigits : zn2z w.
Variable ww_1 : zn2z w.
Variable ww_add_mul_div : zn2z w -> zn2z w -> zn2z w -> zn2z w.
Variable w_zdigits : w.
Definition ww_div_gt_aux ah al bh bl :=
Eval lazy beta iota delta [ww_sub ww_opp] in
let p := w_head0 bh in
match w_compare p w_0 with
| Gt =>
let b1 := w_add_mul_div p bh bl in
let b2 := w_add_mul_div p bl w_0 in
let a1 := w_add_mul_div p w_0 ah in
let a2 := w_add_mul_div p ah al in
let a3 := w_add_mul_div p al w_0 in
let (q,r) := w_div32 a1 a2 a3 b1 b2 in
( WW w_0 q , ww_add_mul_div
(ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r )
| _ => ( ww_1 , ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry (WW ah al) (WW bh bl))
end.
Definition ww_div_gt a b :=
Eval lazy beta iota delta [ww_div_gt_aux double_divn1
double_divn1_p double_divn1_p_aux double_divn1_0 double_divn1_0_aux
double_split double_0 double_WW] in
match a, b with
| W0, _ => ( W0 , W0 )
| _, W0 => ( W0 , W0 )
| WW ah al, WW bh bl =>
if w_eq0 ah then
let (q,r) := w_div_gt al bl in
( WW w_0 q , w_0W r )
else
match w_compare w_0 bh with
| Eq =>
let(q,r):=
double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
w_compare w_sub 1 a bl in
( q , w_0W r )
| Lt => ww_div_gt_aux ah al bh bl
| Gt => ( W0 , W0 )
end
end.
Definition ww_mod_gt_aux ah al bh bl :=
Eval lazy beta iota delta [ww_sub ww_opp] in
let p := w_head0 bh in
match w_compare p w_0 with
| Gt =>
let b1 := w_add_mul_div p bh bl in
let b2 := w_add_mul_div p bl w_0 in
let a1 := w_add_mul_div p w_0 ah in
let a2 := w_add_mul_div p ah al in
let a3 := w_add_mul_div p al w_0 in
let (q,r) := w_div32 a1 a2 a3 b1 b2 in
ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r
| _ =>
ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry (WW ah al) (WW bh bl)
end.
Definition ww_mod_gt a b :=
Eval lazy beta iota delta [ww_mod_gt_aux double_modn1
double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux
double_split double_0 double_WW snd] in
match a, b with
| W0, _ => W0
| _, W0 => W0
| WW ah al, WW bh bl =>
if w_eq0 ah then w_0W (w_mod_gt al bl)
else
match w_compare w_0 bh with
| Eq =>
w_0W (double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
w_compare w_sub 1 a bl)
| Lt => ww_mod_gt_aux ah al bh bl
| Gt => W0
end
end.
Definition ww_gcd_gt_body (cont: w->w->w->w->zn2z w) (ah al bh bl: w) :=
Eval lazy beta iota delta [ww_mod_gt_aux double_modn1
double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux
double_split double_0 double_WW snd] in
match w_compare w_0 bh with
| Eq =>
match w_compare w_0 bl with
| Eq => WW ah al
| Lt =>
let m := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
w_compare w_sub 1 (WW ah al) bl in
WW w_0 (w_gcd_gt bl m)
| Gt => W0
end
| Lt =>
let m := ww_mod_gt_aux ah al bh bl in
match m with
| W0 => WW bh bl
| WW mh ml =>
match w_compare w_0 mh with
| Eq =>
match w_compare w_0 ml with
| Eq => WW bh bl
| _ =>
let r := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
w_compare w_sub 1 (WW bh bl) ml in
WW w_0 (w_gcd_gt ml r)
end
| Lt =>
let r := ww_mod_gt_aux bh bl mh ml in
match r with
| W0 => m
| WW rh rl => cont mh ml rh rl
end
| Gt => W0
end
end
| Gt => W0
end.
Fixpoint ww_gcd_gt_aux
(p:positive) (cont: w -> w -> w -> w -> zn2z w) (ah al bh bl : w)
{struct p} : zn2z w :=
ww_gcd_gt_body
(fun mh ml rh rl => match p with
| xH => cont mh ml rh rl
| xO p => ww_gcd_gt_aux p (ww_gcd_gt_aux p cont) mh ml rh rl
| xI p => ww_gcd_gt_aux p (ww_gcd_gt_aux p cont) mh ml rh rl
end) ah al bh bl.
Variable w_to_Z : w -> Z.
Notation wB := (base w_digits).
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).
Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
Variable spec_w_0 : [| w_0 |] = 0.
Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_to_w_Z : forall x, 0 <= [[ x ]] < wwB.
Variable spec_w_WW : forall h l, [[ w_WW h l ]] = [| h |] * wB + [| l |].
Variable spec_w_0W : forall l, [[ w_0W l ]] = [| l |].
Variable spec_compare :
forall x y, w_compare x y = Z.compare [| x |] [| y |].
Variable spec_eq0 : forall x, w_eq0 x = true -> [| x |] = 0.
Variable spec_opp_c : forall x, [-| w_opp_c x |] = - [| x |].
Variable spec_opp : forall x, [| w_opp x |] = ( - [| x |] ) mod wB.
Variable spec_opp_carry : forall x, [| w_opp_carry x |] = wB - [| x |] - 1.
Variable spec_sub_c : forall x y, [-| w_sub_c x y |] = [| x |] - [| y |].
Variable spec_sub : forall x y, [| w_sub x y |] = ( [| x |] - [| y |] ) mod wB.
Variable spec_sub_carry :
forall x y, [| w_sub_carry x y |] = ( [| x |] - [| y |] - 1) mod wB.
Variable spec_div_gt : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
let (q,r) := w_div_gt a b in
[| a |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Variable spec_mod_gt : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
[| w_mod_gt a b |] = [| a |] mod [| b |].
Variable spec_gcd_gt : forall a b, [| a |] > [| b |] ->
Zis_gcd [| a |] [| b |] [| w_gcd_gt a b |].
Variable spec_add_mul_div : forall x y p,
[| p |] <= Zpos w_digits ->
[| w_add_mul_div p x y |] =
( [| x |] * (2 ^ ( [| p |] ) ) +
[| y |] / (2 ^ ( ( Zpos w_digits ) - [| p |] ) ) ) mod wB.
Variable spec_head0 : forall x, 0 < [| x |] ->
wB / 2 <= 2 ^ [| w_head0 x |] * [| x |] < wB.
Variable spec_div21 : forall a1 a2 b,
wB /2 <= [| b |] ->
[| a1 |] < [| b |] ->
let (q,r) := w_div21 a1 a2 b in
[| a1 |] * wB + [| a2 |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Variable spec_w_div32 : forall a1 a2 a3 b1 b2,
wB /2 <= [| b1 |] ->
[[ WW a1 a2 ]] < [[ WW b1 b2 ]] ->
let (q,r) := w_div32 a1 a2 a3 b1 b2 in
[| a1 |] * wwB + [| a2 |] * wB + [| a3 |] =
[| q |] * ( [| b1 |] * wB + [| b2 |] ) + [[ r ]] /\
0 <= [[ r ]] < [| b1 |] * wB + [| b2 |].
Variable spec_w_zdigits: [| w_zdigits |] = Zpos w_digits.
Variable spec_ww_digits_ : [[ _ww_zdigits ]] = Zpos (xO w_digits).
Variable spec_ww_1 : [[ ww_1 ]] = 1.
Variable spec_ww_add_mul_div : forall x y p,
[[ p ]] <= Zpos (xO w_digits) ->
[[ ww_add_mul_div p x y ]] =
( [[ x ]] * (2^ [[ p ]] ) +
[[ y ]] / (2^( Zpos (xO w_digits) - [[ p ]] ) ) ) mod wwB.
Ltac Spec_w_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Lemma to_Z_div_minus_p : forall x p,
0 < [| p |] < Zpos w_digits ->
0 <= [| x |] / 2 ^ ( Zpos w_digits - [| p |] ) < 2 ^ [| p |].
Hint Resolve to_Z_div_minus_p : zarith.
Lemma spec_ww_div_gt_aux : forall ah al bh bl,
[[ WW ah al ]] > [[ WW bh bl ]] ->
0 < [| bh |] ->
let (q,r) := ww_div_gt_aux ah al bh bl in
[[ WW ah al ]] = [[ q ]] * [[ WW bh bl ]] + [[ r ]] /\
0 <= [[ r ]] < [[ WW bh bl ]].
Lemma spec_ww_div_gt : forall a b, [[ a ]] > [[ b ]] -> 0 < [[ b ]] ->
let (q,r) := ww_div_gt a b in
[[ a ]] = [[ q ]] * [[ b ]] + [[ r ]] /\
0 <= [[ r ]] < [[ b ]].
Lemma spec_ww_mod_gt_aux_eq : forall ah al bh bl,
ww_mod_gt_aux ah al bh bl = snd (ww_div_gt_aux ah al bh bl).
Lemma spec_ww_mod_gt_aux : forall ah al bh bl,
[[ WW ah al ]] > [[ WW bh bl ]] ->
0 < [| bh |] ->
[[ ww_mod_gt_aux ah al bh bl ]] = [[ WW ah al ]] mod [[ WW bh bl ]].
Lemma spec_w_mod_gt_eq : forall a b, [| a |] > [| b |] -> 0 < [| b |] ->
[| w_mod_gt a b |] = [| snd (w_div_gt a b)|].
Lemma spec_ww_mod_gt_eq : forall a b, [[ a ]] > [[ b ]] -> 0 < [[ b ]] ->
[[ ww_mod_gt a b ]] = [[ snd (ww_div_gt a b)]].
Lemma spec_ww_mod_gt : forall a b, [[ a ]] > [[ b ]] -> 0 < [[ b ]] ->
[[ ww_mod_gt a b ]] = [[ a ]] mod [[ b ]].
Lemma Zis_gcd_mod : forall a b d,
0 < b -> Zis_gcd b (a mod b) d -> Zis_gcd a b d.
Lemma spec_ww_gcd_gt_aux_body :
forall ah al bh bl n cont,
[[ WW bh bl ]] <= 2^ n ->
[[ WW ah al ]] > [[ WW bh bl ]] ->
(forall xh xl yh yl,
[[ WW xh xl ]] > [[ WW yh yl ]] -> [[ WW yh yl ]] <= 2^( n -1) ->
Zis_gcd [[ WW xh xl ]] [[ WW yh yl ]] [[ cont xh xl yh yl ]]) ->
Zis_gcd [[ WW ah al ]] [[ WW bh bl ]] [[ ww_gcd_gt_body cont ah al bh bl ]].
Lemma spec_ww_gcd_gt_aux :
forall p cont n,
(forall xh xl yh yl,
[[ WW xh xl ]] > [[ WW yh yl ]] ->
[[ WW yh yl ]] <= 2^ n ->
Zis_gcd [[ WW xh xl ]] [[ WW yh yl ]] [[ cont xh xl yh yl ]]) ->
forall ah al bh bl , [[ WW ah al ]] > [[ WW bh bl ]] ->
[[ WW bh bl ]] <= 2^( Zpos p + n ) ->
Zis_gcd [[ WW ah al ]] [[ WW bh bl ]]
[[ ww_gcd_gt_aux p cont ah al bh bl ]].
End DoubleDivGt.
Section DoubleDiv.
Variable w : Type.
Variable w_digits : positive.
Variable ww_1 : zn2z w.
Variable ww_compare : zn2z w -> zn2z w -> comparison.
Variable ww_div_gt : zn2z w -> zn2z w -> zn2z w * zn2z w.
Variable ww_mod_gt : zn2z w -> zn2z w -> zn2z w.
Definition ww_div a b :=
match ww_compare a b with
| Gt => ww_div_gt a b
| Eq => ( ww_1 , W0 )
| Lt => ( W0 , a )
end.
Definition ww_mod a b :=
match ww_compare a b with
| Gt => ww_mod_gt a b
| Eq => W0
| Lt => a
end.
Variable w_to_Z : w -> Z.
Notation wB := (base w_digits).
Notation wwB := (base (ww_digits w_digits)).
Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99).
Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_ww_1 : [[ ww_1 ]] = 1.
Variable spec_ww_compare : forall x y,
ww_compare x y = Z.compare [[ x ]] [[ y ]].
Variable spec_ww_div_gt : forall a b, [[ a ]] > [[ b ]] -> 0 < [[ b ]] ->
let (q,r) := ww_div_gt a b in
[[ a ]] = [[ q ]] * [[ b ]] + [[ r ]] /\
0 <= [[ r ]] < [[ b ]].
Variable spec_ww_mod_gt : forall a b, [[ a ]] > [[ b ]] -> 0 < [[ b ]] ->
[[ ww_mod_gt a b ]] = [[ a ]] mod [[ b ]].
Ltac Spec_w_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:= fresh "HH" in
assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Lemma spec_ww_div : forall a b, 0 < [[ b ]] ->
let (q,r) := ww_div a b in
[[ a ]] = [[ q ]] * [[ b ]] + [[ r ]] /\
0 <= [[ r ]] < [[ b ]].
Lemma spec_ww_mod : forall a b, 0 < [[ b ]] ->
[[ ww_mod a b ]] = [[ a ]] mod [[ b ]].
Variable w_0 : w.
Variable w_1 : w.
Variable w_compare : w -> w -> comparison.
Variable w_eq0 : w -> bool.
Variable w_gcd_gt : w -> w -> w.
Variable _ww_digits : positive.
Variable spec_ww_digits_ : _ww_digits = xO w_digits.
Variable ww_gcd_gt_fix :
positive -> (w -> w -> w -> w -> zn2z w) ->
w -> w -> w -> w -> zn2z w.
Variable spec_w_0 : [| w_0 |] = 0.
Variable spec_w_1 : [| w_1 |] = 1.
Variable spec_compare :
forall x y, w_compare x y = Z.compare [| x |] [| y |].
Variable spec_eq0 : forall x, w_eq0 x = true -> [| x |] = 0.
Variable spec_gcd_gt : forall a b, [| a |] > [| b |] ->
Zis_gcd [| a |] [| b |] [| w_gcd_gt a b |].
Variable spec_gcd_gt_fix :
forall p cont n,
(forall xh xl yh yl,
[[ WW xh xl ]] > [[ WW yh yl ]] ->
[[ WW yh yl ]] <= 2^ n ->
Zis_gcd [[ WW xh xl ]] [[ WW yh yl ]] [[ cont xh xl yh yl ]]) ->
forall ah al bh bl , [[ WW ah al ]] > [[ WW bh bl ]] ->
[[ WW bh bl ]] <= 2^( Zpos p + n ) ->
Zis_gcd [[ WW ah al ]] [[ WW bh bl ]]
[[ ww_gcd_gt_fix p cont ah al bh bl ]].
Definition gcd_cont (xh xl yh yl:w) :=
match w_compare w_1 yl with
| Eq => ww_1
| _ => WW xh xl
end.
Lemma spec_gcd_cont : forall xh xl yh yl,
[[ WW xh xl ]] > [[ WW yh yl ]] ->
[[ WW yh yl ]] <= 1 ->
Zis_gcd [[ WW xh xl ]] [[ WW yh yl ]] [[ gcd_cont xh xl yh yl ]].
Variable cont : w -> w -> w -> w -> zn2z w.
Variable spec_cont : forall xh xl yh yl,
[[ WW xh xl ]] > [[ WW yh yl ]] ->
[[ WW yh yl ]] <= 1 ->
Zis_gcd [[ WW xh xl ]] [[ WW yh yl ]] [[ cont xh xl yh yl ]].
Definition ww_gcd_gt a b :=
match a, b with
| W0, _ => b
| _, W0 => a
| WW ah al, WW bh bl =>
if w_eq0 ah then (WW w_0 (w_gcd_gt al bl))
else ww_gcd_gt_fix _ww_digits cont ah al bh bl
end.
Definition ww_gcd a b :=
Eval lazy beta delta [ww_gcd_gt] in
match ww_compare a b with
| Gt => ww_gcd_gt a b
| Eq => a
| Lt => ww_gcd_gt b a
end.
Lemma spec_ww_gcd_gt : forall a b, [[ a ]] > [[ b ]] ->
Zis_gcd [[ a ]] [[ b ]] [[ ww_gcd_gt a b ]].
Lemma spec_ww_gcd : forall a b, Zis_gcd [[ a ]] [[ b ]] [[ ww_gcd a b ]].
End DoubleDiv.