# Library Coq.Numbers.Cyclic.Int31.Cyclic31

This library has been deprecated since Coq version 8.10.

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

Author: Arnaud Spiwack (+ Pierre Letouzey)

Require Import List.
Require Export Int31.
Require Import Znumtheory.
Require Import Zgcd_alt.
Require Import Zpow_facts.
Require Import CyclicAxioms.
Require Import Lia.

Local Open Scope nat_scope.
Local Open Scope int31_scope.

Local Hint Resolve Z.lt_gt Z.div_pos : zarith.

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 x := nat_rect _ x (fun _ => shiftr).

Lemma nshiftr_S :
forall n x, nshiftr x (S n) = shiftr (nshiftr x n).

Lemma nshiftr_S_tail :
forall n x, nshiftr x (S n) = nshiftr (shiftr x) n.

Lemma nshiftr_n_0 : forall n, nshiftr 0 n = 0.

Lemma nshiftr_size : forall x, nshiftr x size = 0.

Lemma nshiftr_above_size : forall k x, size<=k ->
nshiftr x k = 0.

# Iterated shift to the left

Definition nshiftl x := nat_rect _ x (fun _ => shiftl).

Lemma nshiftl_S :
forall n x, nshiftl x (S n) = shiftl (nshiftl x n).

Lemma nshiftl_S_tail :
forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.

Lemma nshiftl_n_0 : forall n, nshiftl 0 n = 0.

Lemma nshiftl_size : forall x, nshiftl x size = 0.

Lemma nshiftl_above_size : forall k x, size<=k ->
nshiftl x k = 0.

Lemma firstr_firstl :
forall x, firstr x = firstl (nshiftl x (pred size)).

Lemma firstl_firstr :
forall x, firstl x = firstr (nshiftr x (pred size)).

Lemma nshiftr_predsize_0_firstl : forall x,
nshiftr x (pred size) = 0 -> firstl x = D0.

Lemma nshiftr_0_propagates : forall n p x, n <= p ->
nshiftr x n = 0 -> nshiftr x p = 0.

Lemma nshiftr_0_firstl : forall n x, n < size ->
nshiftr x n = 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 x (size - n)) =
recr_aux p A case0 caserec (nshiftr x (size - n)).

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 x (size-n)) < 2 ^ (Z.of_nat n))%Z.

Lemma phi_nonneg : forall x, (0 <= phi x)%Z.

#[local]
Hint Resolve phi_nonneg : zarith.

Lemma phi_bounded : forall x, (0 <= phi x < 2 ^ (Z.of_nat size))%Z.

Lemma phibis_aux_lowerbound :
forall n x, firstr (nshiftr x n) = 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 x n = nshiftl y n.

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 x n) = 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 proving 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.

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 x (size-n))) =
nshiftr x (size-n).

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 (snd (p2ibis n p)) n = 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.

#[global]

Instance int31_ops : ZnZ.Ops int31 :=
{
digits := 31%positive;
zdigits := 31;
to_Z := phi;
of_pos := positive_to_int31;
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;
succ := fun i => i + 1;
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;
pos_mod :=
fun p i =>
match p ?= 31 with
| _ => i
end;
is_even :=
fun i => let (_,r) := i/2 in
match r ?= 0 with Eq => true | _ => false end;
sqrt2 := sqrt312;
sqrt := sqrt31;
lor := lor31;
land := land31;
lxor := lxor31
}.

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, c at level 99).

Notation "[-| c |]" :=
(interp_carry (-1) wB phi c) (at level 0, c 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|]).

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.

forall x y, [|x+y+1|] = ([|x|] + [|y|] + 1) mod wB.

Lemma spec_succ : forall x, [|x+1|] = ([|x|] + 1) mod wB.

Subtraction

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,

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

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.

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 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|].
Qed.

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.

Strategy 1 [iter312_sqrt].

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.

Lemma log2_phi_bounded x : Z.log2 [|x|] < Z.of_nat size.

Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x|] [|y|].

Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x|] [|y|].

Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x|] [|y|].

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_succ := spec_succ;
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_tail00 := spec_tail00;
spec_tail0 := spec_tail0;
spec_pos_mod := spec_pos_mod;
spec_is_even := spec_is_even;
spec_sqrt2 := spec_sqrt2;
spec_sqrt := spec_sqrt;
spec_lor := spec_lor;
spec_land := spec_land;
spec_lxor := spec_lxor }.

End Int31_Specs.

Module Int31Cyclic <: CyclicType.