# 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.