# Library Coq.Numbers.Cyclic.Int31.Cyclic31

# Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z

Author: Arnaud Spiwack (+ Pierre Letouzey)
Require Import List.
Require Import Min.
Require Export Int31.
Require Import Znumtheory.
Require Import Zgcd_alt.
Require Import Zpow_facts.
Require Import BigNumPrelude.
Require Import CyclicAxioms.
Require Import ROmega.
Local Open Scope nat_scope.
Local Open Scope int31_scope.
Section Basics.

# Basic results about iszero, shiftl, shiftr

Lemma iszero_eq0 : forall x, iszero x = true -> x =0.
Lemma iszero_not_eq0 : forall x, iszero x = false -> x <>0.
Lemma sneakl_shiftr : forall x,
x = sneakl (firstr x) (shiftr x).
Lemma sneakr_shiftl : forall x,
x = sneakr (firstl x) (shiftl x).
Lemma twice_zero : forall x,
twice x = 0 <-> twice_plus_one x = 1.
Lemma twice_or_twice_plus_one : forall x,
x = twice (shiftr x) \/ x = twice_plus_one (shiftr x).

# Iterated shift to the right

Definition nshiftr n x := iter_nat n _ shiftr x.
Lemma nshiftr_S :
forall n x, nshiftr (S n) x = shiftr (nshiftr n x).
Lemma nshiftr_S_tail :
forall n x, nshiftr (S n) x = nshiftr n (shiftr x).
Lemma nshiftr_n_0 : forall n, nshiftr n 0 = 0.
Lemma nshiftr_size : forall x, nshiftr size x = 0.
Lemma nshiftr_above_size : forall k x, size <= k ->
nshiftr k x = 0.

# Iterated shift to the left

Definition nshiftl n x := iter_nat n _ shiftl x.
Lemma nshiftl_S :
forall n x, nshiftl (S n) x = shiftl (nshiftl n x).
Lemma nshiftl_S_tail :
forall n x, nshiftl (S n) x = nshiftl n (shiftl x).
Lemma nshiftl_n_0 : forall n, nshiftl n 0 = 0.
Lemma nshiftl_size : forall x, nshiftl size x = 0.
Lemma nshiftl_above_size : forall k x, size <= k ->
nshiftl k x = 0.
Lemma firstr_firstl :
forall x, firstr x = firstl (nshiftl (pred size) x).
Lemma firstl_firstr :
forall x, firstl x = firstr (nshiftr (pred size) x).
More advanced results about nshiftr
Lemma nshiftr_predsize_0_firstl : forall x,
nshiftr (pred size) x = 0 -> firstl x = D0.
Lemma nshiftr_0_propagates : forall n p x, n <= p ->
nshiftr n x = 0 -> nshiftr p x = 0.
Lemma nshiftr_0_firstl : forall n x, n < size ->
nshiftr n x = 0 -> firstl x = D0.

# Some induction principles over int31

Not used for the moment. Are they really useful ?
Lemma int31_ind_sneakl : forall P : int31->Prop,
P 0 ->
(forall x d, P x -> P (sneakl d x)) ->
forall x, P x.
Lemma int31_ind_twice : forall P : int31->Prop,
P 0 ->
(forall x, P x -> P (twice x)) ->
(forall x, P x -> P (twice_plus_one x)) ->
forall x, P x.

# Some generic results about recr

Section Recr.
recr satisfies the fixpoint equation used for its definition.
Variable (A:Type)(case0:A)(caserec:digits->int31->A->A).
Lemma recr_aux_eqn : forall n x, iszero x = false ->
recr_aux (S n) A case0 caserec x =
caserec (firstr x) (shiftr x) (recr_aux n A case0 caserec (shiftr x)).
Lemma recr_aux_converges :
forall n p x, n <= size -> n <= p ->
recr_aux n A case0 caserec (nshiftr (size - n) x) =
recr_aux p A case0 caserec (nshiftr (size - n) x).
Lemma recr_eqn : forall x, iszero x = false ->
recr A case0 caserec x =
caserec (firstr x) (shiftr x) (recr A case0 caserec (shiftr x)).
recr is usually equivalent to a variant recrbis written without iszero check.
Fixpoint recrbis_aux (n:nat)(A:Type)(case0:A)(caserec:digits->int31->A->A)
(i:int31) : A :=
match n with
| O => case0
| S next =>
let si := shiftr i in
caserec (firstr i) si (recrbis_aux next A case0 caserec si)
end.
Definition recrbis := recrbis_aux size.
Hypothesis case0_caserec : caserec D0 0 case0 = case0.
Lemma recrbis_aux_equiv : forall n x,
recrbis_aux n A case0 caserec x = recr_aux n A case0 caserec x.
Lemma recrbis_equiv : forall x,
recrbis A case0 caserec x = recr A case0 caserec x.
End Recr.

# Incrementation

Section Incr.
Variant of incr via recrbis
Let Incr (b : digits) (si rec : int31) :=
match b with
| D0 => sneakl D1 si
| D1 => sneakl D0 rec
end.
Definition incrbis_aux n x := recrbis_aux n _ In Incr x.
Lemma incrbis_aux_equiv : forall x, incrbis_aux size x = incr x.
Recursive equations satisfied by incr
Lemma incr_eqn1 :
forall x, firstr x = D0 -> incr x = twice_plus_one (shiftr x).
Lemma incr_eqn2 :
forall x, firstr x = D1 -> incr x = twice (incr (shiftr x)).
Lemma incr_twice : forall x, incr (twice x) = twice_plus_one x.
Lemma incr_twice_plus_one_firstl :
forall x, firstl x = D0 -> incr (twice_plus_one x) = twice (incr x).
The previous result is actually true even without the constraint on firstl, but this is harder to prove (see later).
End Incr.

# Conversion to Z : the phi function

Section Phi.
Variant of phi via recrbis
Let Phi := fun b (_:int31) =>
match b with D0 => Z.double | D1 => Z.succ_double end.
Definition phibis_aux n x := recrbis_aux n _ Z0 Phi x.
Lemma phibis_aux_equiv : forall x, phibis_aux size x = phi x.
Recursive equations satisfied by phi
Lemma phi_eqn1 : forall x, firstr x = D0 ->
phi x = Z.double (phi (shiftr x)).
Lemma phi_eqn2 : forall x, firstr x = D1 ->
phi x = Z.succ_double (phi (shiftr x)).
Lemma phi_twice_firstl : forall x, firstl x = D0 ->
phi (twice x) = Z.double (phi x).
Lemma phi_twice_plus_one_firstl : forall x, firstl x = D0 ->
phi (twice_plus_one x) = Z.succ_double (phi x).
End Phi.
phi x is positive and lower than 2^31
Lemma phibis_aux_pos : forall n x, (0 <= phibis_aux n x)%Z.
Lemma phibis_aux_bounded :
forall n x, n <= size ->
(phibis_aux n (nshiftr (size - n) x) < 2 ^ ( Z.of_nat n ))%Z.
Lemma phi_bounded : forall x, (0 <= phi x < 2 ^ ( Z.of_nat size ))%Z.
Lemma phibis_aux_lowerbound :
forall n x, firstr (nshiftr n x) = D1 ->
(2 ^ Z.of_nat n <= phibis_aux (S n) x)%Z.
Lemma phi_lowerbound :
forall x, firstl x = D1 -> (2^( Z.of_nat (pred size)) <= phi x)%Z.

# Equivalence modulo 2^n

Section EqShiftL.
After killing n bits at the left, are the numbers equal ?
Definition EqShiftL n x y :=
nshiftl n x = nshiftl n y.
Lemma EqShiftL_zero : forall x y, EqShiftL O x y <-> x = y.
Lemma EqShiftL_size : forall k x y, size <= k -> EqShiftL k x y.
Lemma EqShiftL_le : forall k k' x y, k <= k' ->
EqShiftL k x y -> EqShiftL k' x y.
Lemma EqShiftL_firstr : forall k x y, k < size ->
EqShiftL k x y -> firstr x = firstr y.
Lemma EqShiftL_twice : forall k x y,
EqShiftL k (twice x) (twice y) <-> EqShiftL (S k) x y.

# From int31 to list of digits.

Lower (=rightmost) bits comes first.
Definition i2l := recrbis _ nil (fun d _ rec => d :: rec).
Lemma i2l_length : forall x, length (i2l x) = size.
Fixpoint lshiftl l x :=
match l with
| nil => x
| d :: l => sneakl d (lshiftl l x)
end.
Definition l2i l := lshiftl l On.
Lemma l2i_i2l : forall x, l2i (i2l x) = x.
Lemma i2l_sneakr : forall x d,
i2l (sneakr d x) = tail (i2l x) ++ d :: nil.
Lemma i2l_sneakl : forall x d,
i2l (sneakl d x) = d :: removelast (i2l x).
Lemma i2l_l2i : forall l, length l = size ->
i2l (l2i l) = l.
Fixpoint cstlist (A:Type)(a:A) n :=
match n with
| O => nil
| S n => a :: cstlist _ a n
end.
Lemma i2l_nshiftl : forall n x, n <= size ->
i2l (nshiftl n x) = cstlist _ D0 n ++ firstn (size - n) (i2l x).
i2l can be used to define a relation equivalent to EqShiftL
Lemma EqShiftL_i2l : forall k x y,
EqShiftL k x y <-> firstn (size - k) (i2l x) = firstn (size - k) (i2l y).
This equivalence allows to prove easily the following delicate result
Lemma EqShiftL_twice_plus_one : forall k x y,
EqShiftL k (twice_plus_one x) (twice_plus_one y) <-> EqShiftL (S k) x y.
Lemma EqShiftL_shiftr : forall k x y, EqShiftL k x y ->
EqShiftL (S k) (shiftr x) (shiftr y).
Lemma EqShiftL_incrbis : forall n k x y, n <= size ->
(n + k = S size)%nat ->
EqShiftL k x y ->
EqShiftL k (incrbis_aux n x) (incrbis_aux n y).
Lemma EqShiftL_incr : forall x y,
EqShiftL 1 x y -> EqShiftL 1 (incr x) (incr y).
End EqShiftL.

# More equations about incr

Lemma incr_twice_plus_one :
forall x, incr (twice_plus_one x) = twice (incr x).
Lemma incr_firstr : forall x, firstr (incr x) <> firstr x.
Lemma incr_inv : forall x y,
incr x = twice_plus_one y -> x = twice y.

# Conversion from Z : the phi_inv function

First, recursive equations
Lemma phi_inv_double_plus_one : forall z,
phi_inv (Z.succ_double z) = twice_plus_one (phi_inv z).
Lemma phi_inv_double : forall z,
phi_inv (Z.double z) = twice (phi_inv z).
Lemma phi_inv_incr : forall z,
phi_inv (Z.succ z) = incr (phi_inv z).
phi_inv o inv, the always-exact and easy-to-prove trip : from int31 to Z and then back to int31.
Lemma phi_inv_phi_aux :
forall n x, n <= size ->
phi_inv (phibis_aux n (nshiftr (size - n) x)) =
nshiftr (size - n) x.
Lemma phi_inv_phi : forall x, phi_inv (phi x) = x.
The other composition phi o phi_inv is harder to prove correct. In particular, an overflow can happen, so a modulo is needed. For the moment, we proceed via several steps, the first one being a detour to positive_to_in31.

# positive_to_int31

A variant of p2i with twice and twice_plus_one instead of 2*i and 2*i+1
Fixpoint p2ibis n p : (N * int31)%type :=
match n with
| O => ( Npos p , On )
| S n => match p with
| xO p => let (r,i) := p2ibis n p in ( r , twice i )
| xI p => let (r,i) := p2ibis n p in ( r , twice_plus_one i )
| xH => ( N0 , In )
end
end.
Lemma p2ibis_bounded : forall n p,
nshiftr n (snd (p2ibis n p)) = 0.
Local Open Scope Z_scope.
Lemma p2ibis_spec : forall n p, (n <= size)%nat ->
Zpos p = ( Z.of_N (fst (p2ibis n p)))*2^( Z.of_nat n ) +
phi (snd (p2ibis n p)).
We now prove that this p2ibis is related to phi_inv_positive
Lemma phi_inv_positive_p2ibis : forall n p, (n <= size)%nat ->
EqShiftL (size - n) (phi_inv_positive p) (snd (p2ibis n p)).
This gives the expected result about phi o phi_inv, at least for the positive case.
Lemma phi_phi_inv_positive : forall p,
phi (phi_inv_positive p) = ( Zpos p ) mod (2^( Z.of_nat size ) ).
Moreover, p2ibis is also related with p2i and hence with positive_to_int31.
Lemma double_twice_firstl : forall x, firstl x = D0 ->
(Twon * x = twice x)%int31.
Lemma double_twice_plus_one_firstl : forall x, firstl x = D0 ->
(Twon * x + In = twice_plus_one x)%int31.
Lemma p2i_p2ibis : forall n p, (n <= size)%nat ->
p2i n p = p2ibis n p.
Lemma positive_to_int31_phi_inv_positive : forall p,
snd (positive_to_int31 p) = phi_inv_positive p.
Lemma positive_to_int31_spec : forall p,
Zpos p = ( Z.of_N (fst (positive_to_int31 p)))*2^( Z.of_nat size ) +
phi (snd (positive_to_int31 p)).
Thanks to the result about phi o phi_inv_positive, we can now establish easily the most general results about phi o twice and so one.
Lemma phi_twice : forall x,
phi (twice x) = ( Z.double (phi x)) mod 2^( Z.of_nat size ).
Lemma phi_twice_plus_one : forall x,
phi (twice_plus_one x) = ( Z.succ_double (phi x)) mod 2^( Z.of_nat size ).
Lemma phi_incr : forall x,
phi (incr x) = ( Z.succ (phi x)) mod 2^( Z.of_nat size ).
With the previous results, we can deal with phi o phi_inv even in the negative case
Lemma phi_phi_inv_negative :
forall p, phi (incr (complement_negative p)) = ( Zneg p ) mod 2^( Z.of_nat size ).
Lemma phi_phi_inv :
forall z, phi (phi_inv z) = z mod 2 ^ ( Z.of_nat size ).
End Basics.
Instance int31_ops : ZnZ.Ops int31 :=
{
digits := 31%positive;
zdigits := 31;
to_Z := phi;
of_pos := positive_to_int31;
head0 := head031;
tail0 := tail031;
zero := 0;
one := 1;
minus_one := Tn;
compare := compare31;
eq0 := fun i => match i ?= 0 with Eq => true | _ => false end;
opp_c := fun i => 0 - c i;
opp := opp31;
opp_carry := fun i => 0- i -1;
succ_c := fun i => i + c 1;
add_c := add31c;
add_carry_c := add31carryc;
succ := fun i => i + 1;
add := add31;
add_carry := fun i j => i + j + 1;
pred_c := fun i => i - c 1;
sub_c := sub31c;
sub_carry_c := sub31carryc;
pred := fun i => i - 1;
sub := sub31;
sub_carry := fun i j => i - j - 1;
mul_c := mul31c;
mul := mul31;
square_c := fun x => x * c x;
div21 := div3121;
div_gt := div31;
div := div31;
modulo_gt := fun i j => let (_,r) := i / j in r;
modulo := fun i j => let (_,r) := i / j in r;
gcd_gt := gcd31;
gcd := gcd31;
add_mul_div := addmuldiv31;
pos_mod :=
fun p i =>
match p ?= 31 with
| Lt => addmuldiv31 p 0 (addmuldiv31 (31- p) i 0)
| _ => i
end;
is_even :=
fun i => let (_,r) := i /2 in
match r ?= 0 with Eq => true | _ => false end;
sqrt2 := sqrt312;
sqrt := sqrt31
}.
Section Int31_Specs.
Local Open Scope Z_scope.
Notation "[| x |]" := (phi x) (at level 0, x at level 99).
Local Notation wB := (2 ^ ( Z.of_nat size )).
Lemma wB_pos : wB > 0.
Notation "[+| c |]" :=
(interp_carry 1 wB phi c) (at level 0, x at level 99).
Notation "[-| c |]" :=
(interp_carry (-1) wB phi c) (at level 0, x at level 99).
Notation "[|| x ||]" :=
(zn2z_to_Z wB phi x) (at level 0, x at level 99).
Lemma spec_zdigits : [| 31 |] = 31.
Lemma spec_more_than_1_digit: 1 < 31.
Lemma spec_0 : [| 0 |] = 0.
Lemma spec_1 : [| 1 |] = 1.
Lemma spec_m1 : [| Tn |] = wB - 1.
Lemma spec_compare : forall x y,
(x ?= y)%int31 = ( [| x |] ?= [| y |] ).
Addition
Lemma spec_add_c : forall x y, [+| add31c x y |] = [| x |] + [| y |].
Lemma spec_succ_c : forall x, [+| add31c x 1|] = [| x |] + 1.
Lemma spec_add_carry_c : forall x y, [+| add31carryc x y |] = [| x |] + [| y |] + 1.
Lemma spec_add : forall x y, [| x + y |] = ( [| x |] + [| y |] ) mod wB.
Lemma spec_add_carry :
forall x y, [| x + y +1|] = ( [| x |] + [| y |] + 1) mod wB.
Lemma spec_succ : forall x, [| x +1|] = ( [| x |] + 1) mod wB.
Substraction
Lemma spec_sub_c : forall x y, [-| sub31c x y |] = [| x |] - [| y |].
Lemma spec_sub_carry_c : forall x y, [-| sub31carryc x y |] = [| x |] - [| y |] - 1.
Lemma spec_sub : forall x y, [| x - y |] = ( [| x |] - [| y |] ) mod wB.
Lemma spec_sub_carry :
forall x y, [| x - y -1|] = ( [| x |] - [| y |] - 1) mod wB.
Lemma spec_opp_c : forall x, [-| sub31c 0 x |] = - [| x |].
Lemma spec_opp : forall x, [|0 - x |] = ( - [| x |] ) mod wB.
Lemma spec_opp_carry : forall x, [|0 - x - 1|] = wB - [| x |] - 1.
Lemma spec_pred_c : forall x, [-| sub31c x 1|] = [| x |] - 1.
Lemma spec_pred : forall x, [| x -1|] = ( [| x |] - 1) mod wB.
Multiplication
Lemma phi2_phi_inv2 : forall x, [|| phi_inv2 x ||] = x mod ( wB ^2).
Lemma spec_mul_c : forall x y, [|| mul31c x y ||] = [| x |] * [| y |].
Lemma spec_mul : forall x y, [| x * y |] = ( [| x |] * [| y |] ) mod wB.
Lemma spec_square_c : forall x, [|| mul31c x x ||] = [| x |] * [| x |].
Division
Lemma spec_div21 : forall a1 a2 b,
wB /2 <= [| b |] ->
[| a1 |] < [| b |] ->
let (q,r) := div3121 a1 a2 b in
[| a1 |] * wB + [| a2 |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Lemma spec_div : forall a b, 0 < [| b |] ->
let (q,r) := div31 a b in
[| a |] = [| q |] * [| b |] + [| r |] /\
0 <= [| r |] < [| b |].
Lemma spec_mod : forall a b, 0 < [| b |] ->
[| let (_,r) := (a / b)%int31 in r |] = [| a |] mod [| b |].
Lemma phi_gcd : forall i j,
[| gcd31 i j |] = Zgcdn (2* size) [| j |] [| i |].
Lemma spec_gcd : forall a b, Zis_gcd [| a |] [| b |] [| gcd31 a b |].
Lemma iter_int31_iter_nat : forall A f i a,
iter_int31 i A f a = iter_nat (Z.abs_nat [| i |]) A f a.
Fixpoint addmuldiv31_alt n i j :=
match n with
| O => i
| S n => addmuldiv31_alt n (sneakl (firstl j) i) (shiftl j)
end.
Lemma addmuldiv31_equiv : forall p x y,
addmuldiv31 p x y = addmuldiv31_alt (Z.abs_nat [| p |]) x y.
Lemma spec_add_mul_div : forall x y p, [| p |] <= Zpos 31 ->
[| addmuldiv31 p x y |] =
( [| x |] * (2 ^ [| p |] ) + [| y |] / (2 ^ ( ( Zpos 31) - [| p |] ) ) ) mod wB.
Lemma spec_pos_mod : forall w p,
[| ZnZ.pos_mod p w |] = [| w |] mod (2 ^ [| p |] ).
Shift operations
Lemma spec_head00: forall x, [| x |] = 0 -> [| head031 x |] = Zpos 31.
Fixpoint head031_alt n x :=
match n with
| O => 0%nat
| S n => match firstl x with
| D0 => S (head031_alt n (shiftl x))
| D1 => 0%nat
end
end.
Lemma head031_equiv :
forall x, [| head031 x |] = Z.of_nat (head031_alt size x).
Lemma phi_nz : forall x, 0 < [| x |] <-> x <> 0%int31.
Lemma spec_head0 : forall x, 0 < [| x |] ->
wB / 2 <= 2 ^ ( [| head031 x |] ) * [| x |] < wB.
Lemma spec_tail00: forall x, [| x |] = 0 -> [| tail031 x |] = Zpos 31.
Fixpoint tail031_alt n x :=
match n with
| O => 0%nat
| S n => match firstr x with
| D0 => S (tail031_alt n (shiftr x))
| D1 => 0%nat
end
end.
Lemma tail031_equiv :
forall x, [| tail031 x |] = Z.of_nat (tail031_alt size x).
Lemma spec_tail0 : forall x, 0 < [| x |] ->
exists y , 0 <= y /\ [| x |] = (2 * y + 1) * (2 ^ [| tail031 x |] ).
Lemma quotient_by_2 a: a - 1 <= ( a /2) + ( a /2).
Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k ->
( j * k ) + j <= ( ( j + k )/2 + 1) ^ 2.
Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ( ( j + ( i / j ) )/2 + 1) ^ 2.
Lemma sqrt_init i: 1 < i -> i < ( i /2 + 1) ^ 2.
Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i / j >= j -> j ^ 2 <= i.
Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i / j < j -> ( j + ( i / j ) )/2 < j.
Lemma sqrt31_step_def rec i j:
sqrt31_step rec i j =
match (fst (i / j) ?= j)%int31 with
Lt => rec i (fst (( j + fst(i / j))/2))%int31
| _ => j
end.
Lemma div31_phi i j: 0 < [| j |] -> [| fst (i / j)%int31 |] = [| i |] / [| j |].
Lemma sqrt31_step_correct rec i j:
0 < [| i |] -> 0 < [| j |] -> [| i |] < ( [| j |] + 1) ^ 2 ->
2 * [| j |] < wB ->
(forall j1 : int31,
0 < [| j1 |] < [| j |] -> [| i |] < ( [| j1 |] + 1) ^ 2 ->
[| rec i j1 |] ^ 2 <= [| i |] < ( [| rec i j1 |] + 1) ^ 2) ->
[| sqrt31_step rec i j |] ^ 2 <= [| i |] < ( [| sqrt31_step rec i j |] + 1) ^ 2.
Lemma iter31_sqrt_correct n rec i j: 0 < [| i |] -> 0 < [| j |] ->
[| i |] < ( [| j |] + 1) ^ 2 -> 2 * [| j |] < 2 ^ ( Z.of_nat size ) ->
(forall j1, 0 < [| j1 |] -> 2^( Z.of_nat n ) + [| j1 |] <= [| j |] ->
[| i |] < ( [| j1 |] + 1) ^ 2 -> 2 * [| j1 |] < 2 ^ ( Z.of_nat size ) ->
[| rec i j1 |] ^ 2 <= [| i |] < ( [| rec i j1 |] + 1) ^ 2) ->
[| iter31_sqrt n rec i j |] ^ 2 <= [| i |] < ( [| iter31_sqrt n rec i j |] + 1) ^ 2.
Lemma spec_sqrt : forall x,
[| sqrt31 x |] ^ 2 <= [| x |] < ( [| sqrt31 x |] + 1) ^ 2.
Lemma sqrt312_step_def rec ih il j:
sqrt312_step rec ih il j =
match (ih ?= j)%int31 with
Eq => j
| Gt => j
| _ =>
match (fst (div3121 ih il j) ?= j)%int31 with
Lt => let m := match j + c fst (div3121 ih il j) with
C0 m1 => fst (m1 /2)%int31
| C1 m1 => (fst (m1 /2) + v30)%int31
end in rec ih il m
| _ => j
end
end.
Lemma sqrt312_lower_bound ih il j:
phi2 ih il < ( [| j |] + 1) ^ 2 -> [| ih |] <= [| j |].
Lemma div312_phi ih il j: (2^30 <= [| j |] -> [| ih |] < [| j |] ->
[| fst (div3121 ih il j)|] = phi2 ih il / [| j |])%Z.
Lemma sqrt312_step_correct rec ih il j:
2 ^ 29 <= [| ih |] -> 0 < [| j |] -> phi2 ih il < ( [| j |] + 1) ^ 2 ->
(forall j1, 0 < [| j1 |] < [| j |] -> phi2 ih il < ( [| j1 |] + 1) ^ 2 ->
[| rec ih il j1 |] ^ 2 <= phi2 ih il < ( [| rec ih il j1 |] + 1) ^ 2) ->
[| sqrt312_step rec ih il j |] ^ 2 <= phi2 ih il
< ( [| sqrt312_step rec ih il j |] + 1) ^ 2.
Lemma iter312_sqrt_correct n rec ih il j:
2^29 <= [| ih |] -> 0 < [| j |] -> phi2 ih il < ( [| j |] + 1) ^ 2 ->
(forall j1, 0 < [| j1 |] -> 2^( Z.of_nat n ) + [| j1 |] <= [| j |] ->
phi2 ih il < ( [| j1 |] + 1) ^ 2 ->
[| rec ih il j1 |] ^ 2 <= phi2 ih il < ( [| rec ih il j1 |] + 1) ^ 2) ->
[| iter312_sqrt n rec ih il j |] ^ 2 <= phi2 ih il
< ( [| iter312_sqrt n rec ih il j |] + 1) ^ 2.
Lemma spec_sqrt2 : forall x y,
wB / 4 <= [| x |] ->
let (s,r) := sqrt312 x y in
[|| WW x y ||] = [| s |] ^ 2 + [+| r |] /\
[+| r |] <= 2 * [| s |].
iszero
Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [| x |] = 0.
Lemma spec_is_even : forall x,
if ZnZ.is_even x then [| x |] mod 2 = 0 else [| x |] mod 2 = 1.
Global Instance int31_specs : ZnZ.Specs int31_ops := {
spec_to_Z := phi_bounded;
spec_of_pos := positive_to_int31_spec;
spec_zdigits := spec_zdigits;
spec_more_than_1_digit := spec_more_than_1_digit;
spec_0 := spec_0;
spec_1 := spec_1;
spec_m1 := spec_m1;
spec_compare := spec_compare;
spec_eq0 := spec_eq0;
spec_opp_c := spec_opp_c;
spec_opp := spec_opp;
spec_opp_carry := spec_opp_carry;
spec_succ_c := spec_succ_c;
spec_add_c := spec_add_c;
spec_add_carry_c := spec_add_carry_c;
spec_succ := spec_succ;
spec_add := spec_add;
spec_add_carry := spec_add_carry;
spec_pred_c := spec_pred_c;
spec_sub_c := spec_sub_c;
spec_sub_carry_c := spec_sub_carry_c;
spec_pred := spec_pred;
spec_sub := spec_sub;
spec_sub_carry := spec_sub_carry;
spec_mul_c := spec_mul_c;
spec_mul := spec_mul;
spec_square_c := spec_square_c;
spec_div21 := spec_div21;
spec_div_gt := fun a b _ => spec_div a b;
spec_div := spec_div;
spec_modulo_gt := fun a b _ => spec_mod a b;
spec_modulo := spec_mod;
spec_gcd_gt := fun a b _ => spec_gcd a b;
spec_gcd := spec_gcd;
spec_head00 := spec_head00;
spec_head0 := spec_head0;
spec_tail00 := spec_tail00;
spec_tail0 := spec_tail0;
spec_add_mul_div := spec_add_mul_div;
spec_pos_mod := spec_pos_mod;
spec_is_even := spec_is_even;
spec_sqrt2 := spec_sqrt2;
spec_sqrt := spec_sqrt }.
End Int31_Specs.
Module Int31Cyclic <: CyclicType.
Definition t := int31.
Definition ops := int31_ops.
Definition specs := int31_specs.
End Int31Cyclic.