# Library Coq.Numbers.Natural.BigN.NMake

# NMake

From a cyclic Z/nZ representation to arbitrary precision natural numbers.
NB: This file contain the part which is independent from the underlying representation. The representation-dependent (and macro-generated) part is now in NMake_gen.
Require Import Bool BigNumPrelude ZArith Nnat Ndigits CyclicAxioms DoubleType
Nbasic Wf_nat StreamMemo NSig NMake_gen.
Module Make (W0:CyclicType) <: NType.
Let's include the macro-generated part. Even if we can't functorize things (due to Eval red_t below), the rest of the module only uses elements mentionned in interface NAbstract.
Include NMake_gen.Make W0.
Open Scope Z_scope.
Local Notation "[ x ]" := (to_Z x).
Definition eq (x y : t) := [ x ] = [ y ].
Ltac red_t :=
match goal with |- ?u => let v := (eval red_t in u) in change v end.

# Generic results

Tactic Notation "destr_t" constr(x) "as" simple_intropattern(pat) :=
destruct (destr_t x) as pat; cbv zeta;
rewrite ?iter_mk_t, ?spec_mk_t, ?spec_reduce.
Lemma spec_same_level : forall A (P:Z->Z->A->Prop)
(f : forall n, dom_t n -> dom_t n -> A),
(forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)) ->
forall x y, P [ x ] [ y ] (same_level f x y).
Theorem spec_pos: forall x, 0 <= [ x ].
Lemma digits_dom_op_incr : forall n m, (n <= m)%nat ->
(ZnZ.digits (dom_op n) <= ZnZ.digits (dom_op m))%positive.
Definition to_N (x : t) := Z.to_N (to_Z x).

# Zero, One

Definition zero := mk_t O ZnZ.zero.
Definition one := mk_t O ZnZ.one.
Theorem spec_0: [ zero ] = 0.
Theorem spec_1: [ one ] = 1.

# Successor

NB: it is crucial here and for the rest of this file to preserve the let-in's. They allow to pre-compute once and for all the field access to Z/nZ initial structures (when n=0..6).
Local Notation succn := (fun n =>
let op := dom_op n in
let succ_c := ZnZ.succ_c in
let one := ZnZ.one in
fun x => match succ_c x with
| C0 r => mk_t n r
| C1 r => mk_t_S n (WW one r)
end).
Definition succ : t -> t := Eval red_t in iter_t succn.
Lemma succ_fold : succ = iter_t succn.
Theorem spec_succ: forall n, [ succ n ] = [ n ] + 1.
Two
Not really pretty, but since W0 might be Z/2Z, we're not sure there's a proper 2 there.
Definition two := succ one.
Lemma spec_2 : [ two ] = 2.

# Addition

Local Notation addn := (fun n =>
let op := dom_op n in
let add_c := ZnZ.add_c in
let one := ZnZ.one in
fun x y =>match add_c x y with
| C0 r => mk_t n r
| C1 r => mk_t_S n (WW one r)
end).
Definition add : t -> t -> t := Eval red_t in same_level addn.
Lemma add_fold : add = same_level addn.
Theorem spec_add: forall x y, [ add x y ] = [ x ] + [ y ].

# Predecessor

Local Notation predn := (fun n =>
let pred_c := ZnZ.pred_c in
fun x => match pred_c x with
| C0 r => reduce n r
| C1 _ => zero
end).
Definition pred : t -> t := Eval red_t in iter_t predn.
Lemma pred_fold : pred = iter_t predn.
Theorem spec_pred_pos : forall x, 0 < [ x ] -> [ pred x ] = [ x ] - 1.
Theorem spec_pred0 : forall x, [ x ] = 0 -> [ pred x ] = 0.
Lemma spec_pred x : [ pred x ] = Z.max 0 ([ x ] -1).

# Subtraction

Local Notation subn := (fun n =>
let sub_c := ZnZ.sub_c in
fun x y => match sub_c x y with
| C0 r => reduce n r
| C1 r => zero
end).
Definition sub : t -> t -> t := Eval red_t in same_level subn.
Lemma sub_fold : sub = same_level subn.
Theorem spec_sub_pos : forall x y, [ y ] <= [ x ] -> [ sub x y ] = [ x ] - [ y ].
Theorem spec_sub0 : forall x y, [ x ] < [ y ] -> [ sub x y ] = 0.
Lemma spec_sub : forall x y, [ sub x y ] = Z.max 0 ([ x ] - [ y ]).

# Comparison

Definition comparen_m n :
forall m, word (dom_t n) (S m) -> dom_t n -> comparison :=
let op := dom_op n in
let zero := @ZnZ.zero _ op in
let compare := @ZnZ.compare _ op in
let compare0 := compare zero in
fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
Let spec_comparen_m:
forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y).
Definition comparenm n m wx wy :=
let mn := Max.max n m in
let d := diff n m in
let op := make_op mn in
ZnZ.compare
(castm (diff_r n m) (extend_tr wx (snd d)))
(castm (diff_l n m) (extend_tr wy (fst d))).
Local Notation compare_folded :=
(iter_sym _
(fun n => @ZnZ.compare _ (dom_op n))
comparen_m
comparenm
CompOpp).
Definition compare : t -> t -> comparison :=
Eval lazy beta iota delta [iter_sym dom_op dom_t comparen_m] in
compare_folded.
Lemma compare_fold : compare = compare_folded.
Theorem spec_compare : forall x y,
compare x y = Z.compare [ x ] [ y ].
Definition eqb (x y : t) : bool :=
match compare x y with
| Eq => true
| _ => false
end.
Theorem spec_eqb x y : eqb x y = Z.eqb [ x ] [ y ].
Definition lt (n m : t) := [ n ] < [ m ].
Definition le (n m : t) := [ n ] <= [ m ].
Definition ltb (x y : t) : bool :=
match compare x y with
| Lt => true
| _ => false
end.
Theorem spec_ltb x y : ltb x y = Z.ltb [ x ] [ y ].
Definition leb (x y : t) : bool :=
match compare x y with
| Gt => false
| _ => true
end.
Theorem spec_leb x y : leb x y = Z.leb [ x ] [ y ].
Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end.
Theorem spec_max : forall n m, [ max n m ] = Z.max [ n ] [ m ].
Theorem spec_min : forall n m, [ min n m ] = Z.min [ n ] [ m ].

# Multiplication

Definition wn_mul n : forall m, word (dom_t n) (S m) -> dom_t n -> t :=
let op := dom_op n in
let zero := @ZnZ.zero _ op in
let succ := @ZnZ.succ _ op in
let add_c := @ZnZ.add_c _ op in
let mul_c := @ZnZ.mul_c _ op in
let ww := @ZnZ.WW _ op in
let ow := @ZnZ.OW _ op in
let eq0 := @ZnZ.eq0 _ op in
let mul_add := @DoubleMul.w_mul_add _ zero succ add_c mul_c in
let mul_add_n1 := @DoubleMul.double_mul_add_n1 _ zero ww ow mul_add in
fun m x y =>
let (w,r) := mul_add_n1 (S m) x y zero in
if eq0 w then mk_t_w' n m r
else mk_t_w' n (S m) (WW (extend n m w) r).
Definition mulnm n m x y :=
let mn := Max.max n m in
let d := diff n m in
let op := make_op mn in
reduce_n (S mn) (ZnZ.mul_c
(castm (diff_r n m) (extend_tr x (snd d)))
(castm (diff_l n m) (extend_tr y (fst d)))).
Local Notation mul_folded :=
(iter_sym _
(fun n => let mul_c := ZnZ.mul_c in
fun x y => reduce (S n) (succ_t _ (mul_c x y)))
wn_mul
mulnm
(fun x => x)).
Definition mul : t -> t -> t :=
Eval lazy beta iota delta
[iter_sym dom_op dom_t reduce succ_t extend zeron
wn_mul DoubleMul.w_mul_add mk_t_w'] in
mul_folded.
Lemma mul_fold : mul = mul_folded.
Lemma spec_muln:
forall n (x: word _ (S n)) y,
[ Nn (S n) (ZnZ.mul_c (Ops:=make_op n) x y)] = [ Nn n x ] * [ Nn n y ].
Lemma spec_mul_add_n1: forall n m x y z,
let (q,r) := DoubleMul.double_mul_add_n1 ZnZ.zero ZnZ.WW ZnZ.OW
(DoubleMul.w_mul_add ZnZ.zero ZnZ.succ ZnZ.add_c ZnZ.mul_c)
(S m) x y z in
ZnZ.to_Z q * ( base (ZnZ.digits (nmake_op _ (dom_op n) (S m))))
+ eval n (S m) r =
eval n (S m) x * ZnZ.to_Z y + ZnZ.to_Z z.
Lemma spec_wn_mul : forall n m x y,
[ wn_mul n m x y ] = ( eval n (S m) x ) * ZnZ.to_Z y.
Theorem spec_mul : forall x y, [ mul x y ] = [ x ] * [ y ].

# Division by a smaller number

Definition wn_divn1 n :=
let op := dom_op n in
let zd := ZnZ.zdigits op in
let zero := @ZnZ.zero _ op in
let ww := @ZnZ.WW _ op in
let head0 := @ZnZ.head0 _ op in
let add_mul_div := @ZnZ.add_mul_div _ op in
let div21 := @ZnZ.div21 _ op in
let compare := @ZnZ.compare _ op in
let sub := @ZnZ.sub _ op in
let ddivn1 :=
DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
fun m x y => let (u,v) := ddivn1 (S m) x y in ( mk_t_w' n m u , mk_t n v ).
Let div_gtnm n m wx wy :=
let mn := Max.max n m in
let d := diff n m in
let op := make_op mn in
let (q, r):= ZnZ.div_gt
(castm (diff_r n m) (extend_tr wx (snd d)))
(castm (diff_l n m) (extend_tr wy (fst d))) in
( reduce_n mn q , reduce_n mn r ).
Local Notation div_gt_folded :=
(iter _
(fun n => let div_gt := ZnZ.div_gt in
fun x y => let (u,v) := div_gt x y in ( reduce n u , reduce n v ))
(fun n =>
let div_gt := ZnZ.div_gt in
fun m x y =>
let y' := DoubleBase.get_low (zeron n) (S m) y in
let (u,v) := div_gt x y' in ( reduce n u , reduce n v ))
wn_divn1
div_gtnm).
Definition div_gt :=
Eval lazy beta iota delta
[iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t] in
div_gt_folded.
Lemma div_gt_fold : div_gt = div_gt_folded.
Lemma spec_get_endn: forall n m x y,
eval n m x <= [ mk_t n y ] ->
[ mk_t n (DoubleBase.get_low (zeron n) m x)] = eval n m x.
Let spec_divn1 n :=
DoubleDivn1.spec_double_divn1
(ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
ZnZ.WW ZnZ.head0
ZnZ.add_mul_div ZnZ.div21
ZnZ.compare ZnZ.sub ZnZ.to_Z
ZnZ.spec_to_Z
ZnZ.spec_zdigits
ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
ZnZ.spec_add_mul_div ZnZ.spec_div21
ZnZ.spec_compare ZnZ.spec_sub.
Lemma spec_div_gt_aux : forall x y, [ x ] > [ y ] -> 0 < [ y ] ->
let (q,r) := div_gt x y in
[ x ] = [ q ] * [ y ] + [ r ] /\ 0 <= [ r ] < [ y ].
Theorem spec_div_gt: forall x y, [ x ] > [ y ] -> 0 < [ y ] ->
let (q,r) := div_gt x y in
[ q ] = [ x ] / [ y ] /\ [ r ] = [ x ] mod [ y ].

# General Division

Definition div_eucl (x y : t) : t * t :=
if eqb y zero then ( zero , zero ) else
match compare x y with
| Eq => ( one , zero )
| Lt => ( zero , x )
| Gt => div_gt x y
end.
Theorem spec_div_eucl: forall x y,
let (q,r) := div_eucl x y in
( [ q ] , [ r ] ) = Z.div_eucl [ x ] [ y ].
Definition div (x y : t) : t := fst (div_eucl x y).
Theorem spec_div:
forall x y, [ div x y ] = [ x ] / [ y ].

# Modulo by a smaller number

Definition wn_modn1 n :=
let op := dom_op n in
let zd := ZnZ.zdigits op in
let zero := @ZnZ.zero _ op in
let head0 := @ZnZ.head0 _ op in
let add_mul_div := @ZnZ.add_mul_div _ op in
let div21 := @ZnZ.div21 _ op in
let compare := @ZnZ.compare _ op in
let sub := @ZnZ.sub _ op in
let dmodn1 :=
DoubleDivn1.double_modn1 zd zero head0 add_mul_div div21 compare sub in
fun m x y => reduce n (dmodn1 (S m) x y).
Let mod_gtnm n m wx wy :=
let mn := Max.max n m in
let d := diff n m in
let op := make_op mn in
reduce_n mn (ZnZ.modulo_gt
(castm (diff_r n m) (extend_tr wx (snd d)))
(castm (diff_l n m) (extend_tr wy (fst d)))).
Local Notation mod_gt_folded :=
(iter _
(fun n => let modulo_gt := ZnZ.modulo_gt in
fun x y => reduce n (modulo_gt x y))
(fun n => let modulo_gt := ZnZ.modulo_gt in
fun m x y =>
reduce n (modulo_gt x (DoubleBase.get_low (zeron n) (S m) y)))
wn_modn1
mod_gtnm).
Definition mod_gt :=
Eval lazy beta iota delta [iter dom_op dom_t reduce wn_modn1 zeron] in
mod_gt_folded.
Lemma mod_gt_fold : mod_gt = mod_gt_folded.
Let spec_modn1 n :=
DoubleDivn1.spec_double_modn1
(ZnZ.zdigits (dom_op n)) (ZnZ.zero:dom_t n)
ZnZ.WW ZnZ.head0
ZnZ.add_mul_div ZnZ.div21
ZnZ.compare ZnZ.sub ZnZ.to_Z
ZnZ.spec_to_Z
ZnZ.spec_zdigits
ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
ZnZ.spec_add_mul_div ZnZ.spec_div21
ZnZ.spec_compare ZnZ.spec_sub.
Theorem spec_mod_gt:
forall x y, [ x ] > [ y ] -> 0 < [ y ] -> [ mod_gt x y ] = [ x ] mod [ y ].

# General Modulo

Definition modulo (x y : t) : t :=
if eqb y zero then zero else
match compare x y with
| Eq => zero
| Lt => x
| Gt => mod_gt x y
end.
Theorem spec_modulo:
forall x y, [ modulo x y ] = [ x ] mod [ y ].

# Square

Local Notation squaren := (fun n =>
let square_c := ZnZ.square_c in
fun x => reduce (S n) (succ_t _ (square_c x))).
Definition square : t -> t := Eval red_t in iter_t squaren.
Lemma square_fold : square = iter_t squaren.
Theorem spec_square: forall x, [ square x ] = [ x ] * [ x ].

# Square Root

Local Notation sqrtn := (fun n =>
let sqrt := ZnZ.sqrt in
fun x => reduce n (sqrt x)).
Definition sqrt : t -> t := Eval red_t in iter_t sqrtn.
Lemma sqrt_fold : sqrt = iter_t sqrtn.
Theorem spec_sqrt_aux: forall x, [ sqrt x ] ^ 2 <= [ x ] < ( [ sqrt x ] + 1) ^ 2.
Theorem spec_sqrt: forall x, [ sqrt x ] = Z.sqrt [ x ].

# Power

Fixpoint pow_pos (x:t)(p:positive) : t :=
match p with
| xH => x
| xO p => square (pow_pos x p)
| xI p => mul (square (pow_pos x p)) x
end.
Theorem spec_pow_pos: forall x n, [ pow_pos x n ] = [ x ] ^ Zpos n.
Definition pow_N (x:t)(n:N) : t := match n with
| BinNat.N0 => one
| BinNat.Npos p => pow_pos x p
end.
Theorem spec_pow_N: forall x n, [ pow_N x n ] = [ x ] ^ Z.of_N n.
Definition pow (x y:t) : t := pow_N x (to_N y).
Theorem spec_pow : forall x y, [ pow x y ] = [ x ] ^ [ y ].

# digits

Number of digits in the representation of a numbers (including head zero's). NB: This function isn't a morphism for setoid eq.
Local Notation digitsn := (fun n =>
let digits := ZnZ.digits (dom_op n) in
fun _ => digits).
Definition digits : t -> positive := Eval red_t in iter_t digitsn.
Lemma digits_fold : digits = iter_t digitsn.
Theorem spec_digits: forall x, 0 <= [ x ] < 2 ^ Zpos (digits x).
Lemma digits_level : forall x, digits x = ZnZ.digits (dom_op (level x)).

# Gcd

Definition gcd_gt_body a b cont :=
match compare b zero with
| Gt =>
let r := mod_gt a b in
match compare r zero with
| Gt => cont r (mod_gt b r)
| _ => b
end
| _ => a
end.
Theorem Zspec_gcd_gt_body: forall a b cont p,
[ a ] > [ b ] -> [ a ] < 2 ^ p ->
(forall a1 b1, [ a1 ] < 2 ^ ( p - 1) -> [ a1 ] > [ b1 ] ->
Zis_gcd [ a1 ] [ b1 ] [ cont a1 b1 ]) ->
Zis_gcd [ a ] [ b ] [ gcd_gt_body a b cont ].
Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) : t :=
gcd_gt_body a b
(fun a b =>
match p with
| xH => cont a b
| xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b
| xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b
end).
Theorem Zspec_gcd_gt_aux: forall p n a b cont,
[ a ] > [ b ] -> [ a ] < 2 ^ ( Zpos p + n ) ->
(forall a1 b1, [ a1 ] < 2 ^ n -> [ a1 ] > [ b1 ] ->
Zis_gcd [ a1 ] [ b1 ] [ cont a1 b1 ]) ->
Zis_gcd [ a ] [ b ] [ gcd_gt_aux p cont a b ].
Definition gcd_cont a b :=
match compare one b with
| Eq => one
| _ => a
end.
Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b.
Theorem spec_gcd_gt: forall a b,
[ a ] > [ b ] -> [ gcd_gt a b ] = Z.gcd [ a ] [ b ].
Definition gcd (a b : t) : t :=
match compare a b with
| Eq => a
| Lt => gcd_gt b a
| Gt => gcd_gt a b
end.
Theorem spec_gcd: forall a b, [ gcd a b ] = Z.gcd [ a ] [ b ].

# Parity test

Definition even : t -> bool := Eval red_t in
iter_t (fun n x => ZnZ.is_even x).
Definition odd x := negb (even x).
Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x).
Theorem spec_even_aux: forall x,
if even x then [ x ] mod 2 = 0 else [ x ] mod 2 = 1.
Theorem spec_even: forall x, even x = Z.even [ x ].
Theorem spec_odd: forall x, odd x = Z.odd [ x ].

# Conversion

Definition pheight p :=
Peano.pred (Pos.to_nat (get_height (ZnZ.digits (dom_op 0)) (plength p))).
Theorem pheight_correct: forall p,
Zpos p < 2 ^ ( Zpos (ZnZ.digits (dom_op 0)) * 2 ^ ( Z.of_nat (pheight p))).
Definition of_pos (x:positive) : t :=
let n := pheight x in
reduce n (snd (ZnZ.of_pos x)).
Theorem spec_of_pos: forall x,
[ of_pos x ] = Zpos x.
Definition of_N (x:N) : t :=
match x with
| BinNat.N0 => zero
| Npos p => of_pos p
end.
Theorem spec_of_N: forall x,
[ of_N x ] = Z.of_N x.

# head0 and tail0

Number of zero at the beginning and at the end of the representation of the number. NB: these functions are not morphism for setoid eq.
Local Notation head0n := (fun n =>
let head0 := ZnZ.head0 in
fun x => reduce n (head0 x)).
Definition head0 : t -> t := Eval red_t in iter_t head0n.
Lemma head0_fold : head0 = iter_t head0n.
Theorem spec_head00: forall x, [ x ] = 0 -> [ head0 x ] = Zpos (digits x).
Lemma pow2_pos_minus_1 : forall z, 0< z -> 2^( z -1) = 2^ z / 2.
Theorem spec_head0: forall x, 0 < [ x ] ->
2 ^ ( Zpos (digits x) - 1) <= 2 ^ [ head0 x ] * [ x ] < 2 ^ Zpos (digits x).
Local Notation tail0n := (fun n =>
let tail0 := ZnZ.tail0 in
fun x => reduce n (tail0 x)).
Definition tail0 : t -> t := Eval red_t in iter_t tail0n.
Lemma tail0_fold : tail0 = iter_t tail0n.
Theorem spec_tail00: forall x, [ x ] = 0 -> [ tail0 x ] = Zpos (digits x).
Theorem spec_tail0: forall x,
0 < [ x ] -> exists y , 0 <= y /\ [ x ] = (2 * y + 1) * 2 ^ [ tail0 x ].

# Ndigits

Same as digits but encoded using large integers NB: this function is not a morphism for setoid eq.
Local Notation Ndigitsn := (fun n =>
let d := reduce n (ZnZ.zdigits (dom_op n)) in
fun _ => d).
Definition Ndigits : t -> t := Eval red_t in iter_t Ndigitsn.
Lemma Ndigits_fold : Ndigits = iter_t Ndigitsn.
Theorem spec_Ndigits: forall x, [ Ndigits x ] = Zpos (digits x).

# Binary logarithm

Local Notation log2n := (fun n =>
let op := dom_op n in
let zdigits := ZnZ.zdigits op in
let head0 := ZnZ.head0 in
let sub_carry := ZnZ.sub_carry in
fun x => reduce n (sub_carry zdigits (head0 x))).
Definition log2 : t -> t := Eval red_t in
let log2 := iter_t log2n in
fun x => if eqb x zero then zero else log2 x.
Lemma log2_fold :
log2 = fun x => if eqb x zero then zero else iter_t log2n x.
Lemma spec_log2_0 : forall x, [ x ] = 0 -> [ log2 x ] = 0.
Lemma head0_zdigits : forall n (x : dom_t n),
0 < ZnZ.to_Z x ->
ZnZ.to_Z (ZnZ.head0 x) < ZnZ.to_Z (ZnZ.zdigits (dom_op n)).
Lemma spec_log2_pos : forall x, [ x ] <>0 ->
2^ [ log2 x ] <= [ x ] < 2^( [ log2 x ] +1).
Lemma spec_log2 : forall x, [ log2 x ] = Z.log2 [ x ].
Lemma log2_digits_head0 : forall x, 0 < [ x ] ->
[ log2 x ] = Zpos (digits x) - [ head0 x ] - 1.

# Right shift

Local Notation shiftrn := (fun n =>
let op := dom_op n in
let zdigits := ZnZ.zdigits op in
let sub_c := ZnZ.sub_c in
let add_mul_div := ZnZ.add_mul_div in
let zzero := ZnZ.zero in
fun x p => match sub_c zdigits p with
| C0 d => reduce n (add_mul_div d zzero x)
| C1 _ => zero
end).
Definition shiftr : t -> t -> t := Eval red_t in
same_level shiftrn.
Lemma shiftr_fold : shiftr = same_level shiftrn.
Lemma div_pow2_bound :forall x y z,
0 <= x -> 0 <= y -> x < z -> 0 <= x / 2 ^ y < z.
Theorem spec_shiftr_pow2 : forall x n,
[ shiftr x n ] = [ x ] / 2 ^ [ n ].
Subtraction without underflow : p <= digits
Subtraction with underflow : digits < p
Lemma spec_shiftr: forall x p, [ shiftr x p ] = Z.shiftr [ x ] [ p ].

# Left shift

First an unsafe version, working correctly only if the representation is large enough
Local Notation unsafe_shiftln := (fun n =>
let op := dom_op n in
let add_mul_div := ZnZ.add_mul_div in
let zero := ZnZ.zero in
fun x p => reduce n (add_mul_div p x zero)).
Definition unsafe_shiftl : t -> t -> t := Eval red_t in
same_level unsafe_shiftln.
Lemma unsafe_shiftl_fold : unsafe_shiftl = same_level unsafe_shiftln.
Theorem spec_unsafe_shiftl_aux : forall x p K,
0 <= K ->
[ x ] < 2^ K ->
[ p ] + K <= Zpos (digits x) ->
[ unsafe_shiftl x p ] = [ x ] * 2 ^ [ p ].
Theorem spec_unsafe_shiftl: forall x p,
[ p ] <= [ head0 x ] -> [ unsafe_shiftl x p ] = [ x ] * 2 ^ [ p ].
Then we define a function doubling the size of the representation but without changing the value of the number.
Local Notation double_size_n := (fun n =>
let zero := ZnZ.zero in
fun x => mk_t_S n (WW zero x)).
Definition double_size : t -> t := Eval red_t in
iter_t double_size_n.
Lemma double_size_fold : double_size = iter_t double_size_n.
Lemma double_size_level : forall x, level (double_size x) = S (level x).
Theorem spec_double_size_digits:
forall x, Zpos (digits (double_size x)) = 2 * ( Zpos (digits x)).
Theorem spec_double_size: forall x, [ double_size x ] = [ x ].
Theorem spec_double_size_head0:
forall x, 2 * [ head0 x ] <= [ head0 (double_size x)].
Theorem spec_double_size_head0_pos:
forall x, 0 < [ head0 (double_size x)].
Finally we iterate double_size enough before unsafe_shiftl in order to get a fully correct shiftl.
Definition shiftl_aux_body cont x n :=
match compare n (head0 x) with
Gt => cont (double_size x) n
| _ => unsafe_shiftl x n
end.
Theorem spec_shiftl_aux_body: forall n x p cont,
2^ Zpos p <= [ head0 x ] ->
(forall x, 2 ^ ( Zpos p + 1) <= [ head0 x ]->
[ cont x n ] = [ x ] * 2 ^ [ n ]) ->
[ shiftl_aux_body cont x n ] = [ x ] * 2 ^ [ n ].
Fixpoint shiftl_aux p cont x n :=
shiftl_aux_body
(fun x n => match p with
| xH => cont x n
| xO p => shiftl_aux p (shiftl_aux p cont) x n
| xI p => shiftl_aux p (shiftl_aux p cont) x n
end) x n.
Theorem spec_shiftl_aux: forall p q x n cont,
2 ^ ( Zpos q ) <= [ head0 x ] ->
(forall x, 2 ^ ( Zpos p + Zpos q ) <= [ head0 x ] ->
[ cont x n ] = [ x ] * 2 ^ [ n ]) ->
[ shiftl_aux p cont x n ] = [ x ] * 2 ^ [ n ].
Definition shiftl x n :=
shiftl_aux_body
(shiftl_aux_body
(shiftl_aux (digits n) unsafe_shiftl)) x n.
Theorem spec_shiftl_pow2 : forall x n,
[ shiftl x n ] = [ x ] * 2 ^ [ n ].
Lemma spec_shiftl: forall x p, [ shiftl x p ] = Z.shiftl [ x ] [ p ].
Other bitwise operations
Definition testbit x n := odd (shiftr x n).
Lemma spec_testbit: forall x p, testbit x p = Z.testbit [ x ] [ p ].
Definition div2 x := shiftr x one.
Lemma spec_div2: forall x, [ div2 x ] = Z.div2 [ x ].
TODO : provide efficient versions instead of just converting from/to N (see with Laurent)
Definition lor x y := of_N (N.lor (to_N x) (to_N y)).
Definition land x y := of_N (N.land (to_N x) (to_N y)).
Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)).
Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)).
Lemma spec_land: forall x y, [ land x y ] = Z.land [ x ] [ y ].
Lemma spec_lor: forall x y, [ lor x y ] = Z.lor [ x ] [ y ].
Lemma spec_ldiff: forall x y, [ ldiff x y ] = Z.ldiff [ x ] [ y ].
Lemma spec_lxor: forall x y, [ lxor x y ] = Z.lxor [ x ] [ y ].
End Make.