Library Coq.Numbers.Cyclic.Int31.Cyclic31
This library has been deprecated since Coq version 8.10.
Author: Arnaud Spiwack (+ Pierre Letouzey)
Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z
Require Import List.
Require Import Min.
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.
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).
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.
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)).
More advanced results about nshiftr
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.
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.
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.
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.
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.
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.
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.
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.
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.
A variant of p2i with twice and twice_plus_one instead of
2*i and 2*i+1
positive_to_int31
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.
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;
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).
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|]).
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.
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,
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 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.
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.
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_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;
spec_lor := spec_lor;
spec_land := spec_land;
spec_lxor := spec_lxor }.
End Int31_Specs.
Module Int31Cyclic <: CyclicType.
Definition t := int31.
Definition ops := int31_ops.
Definition specs := int31_specs.
End Int31Cyclic.