Library Coq.Numbers.Natural.BigN.Nbasic
Require Import ZArith Ndigits.
Require Import BigNumPrelude.
Require Import Max.
Require Import DoubleType.
Require Import DoubleBase.
Require Import CyclicAxioms.
Require Import DoubleCyclic.
Lemma Pshiftl_nat_Zpower :
forall n p,
Zpos (
Pos.shiftl_nat p n)
= Zpos p * 2
^ Z.of_nat n.
Fixpoint plength (
p:
positive) :
positive :=
match p with
xH =>
xH
|
xO p1 =>
Pos.succ (
plength p1)
|
xI p1 =>
Pos.succ (
plength p1)
end.
Theorem plength_correct:
forall p, (
Zpos p < 2
^ Zpos (
plength p))%
Z.
Theorem plength_pred_correct:
forall p, (
Zpos p <= 2
^ Zpos (
plength (
Pos.pred p)))%
Z.
Definition Pdiv p q :=
match Z.div (
Zpos p) (
Zpos q)
with
Zpos q1 =>
match (Zpos p) - (Zpos q) * (Zpos q1) with
Z0 =>
q1
|
_ => (
Pos.succ q1)
end
|
_ =>
xH
end.
Theorem Pdiv_le:
forall p q,
Zpos p <= Zpos q * Zpos (
Pdiv p q).
Definition is_one p :=
match p with xH =>
true |
_ =>
false end.
Theorem is_one_one:
forall p,
is_one p = true ->
p = xH.
Definition get_height digits p :=
let r :=
Pdiv p digits in
if is_one r then xH else Pos.succ (
plength (
Pos.pred r)).
Theorem get_height_correct:
forall digits N,
Zpos N <= Zpos digits * (2
^ (Zpos (
get_height digits N)
-1
)).
Definition zn2z_word_comm :
forall w n,
zn2z (
word w n)
= word (
zn2z w)
n.
Defined.
Fixpoint extend (
n:
nat) {
struct n} :
forall w:
Type,
zn2z w ->
word w (
S n) :=
match n return forall w:
Type,
zn2z w ->
word w (
S n)
with
|
O =>
fun w x =>
x
|
S m =>
let aux :=
extend m in
fun w x =>
WW W0 (
aux w x)
end.
Section ExtendMax.
Open Scope nat_scope.
Fixpoint plusnS (
n m:
nat) {
struct n} : (
n + S m = S (
n + m))%
nat :=
match n return (
n + S m = S (
n + m))%
nat with
| 0 =>
eq_refl (
S m)
|
S n1 =>
let v :=
S (
S n1 + m)
in
eq_ind_r (
fun n =>
S n = v) (
eq_refl v) (
plusnS n1 m)
end.
Fixpoint plusn0 n :
n + 0
= n :=
match n return (
n + 0
= n)
with
| 0 =>
eq_refl 0
|
S n1 =>
let v :=
S n1 in
eq_ind_r (
fun n :
nat =>
S n = v) (
eq_refl v) (
plusn0 n1)
end.
Fixpoint diff (
m n:
nat) {
struct m}:
nat * nat :=
match m,
n with
O,
n =>
(O, n)
|
m,
O =>
(m, O)
|
S m1,
S n1 =>
diff m1 n1
end.
Fixpoint diff_l (
m n :
nat) {
struct m} :
fst (
diff m n)
+ n = max m n :=
match m return fst (
diff m n)
+ n = max m n with
| 0 =>
match n return (
n = max 0
n)
with
| 0 =>
eq_refl _
|
S n0 =>
eq_refl _
end
|
S m1 =>
match n return (
fst (
diff (
S m1)
n)
+ n = max (
S m1)
n)
with
| 0 =>
plusn0 _
|
S n1 =>
let v :=
fst (
diff m1 n1)
+ n1 in
let v1 :=
fst (
diff m1 n1)
+ S n1 in
eq_ind v (
fun n =>
v1 = S n)
(
eq_ind v1 (
fun n =>
v1 = n) (
eq_refl v1) (
S v) (
plusnS _ _))
_ (
diff_l _ _)
end
end.
Fixpoint diff_r (
m n:
nat) {
struct m}:
snd (
diff m n)
+ m = max m n :=
match m return (
snd (
diff m n)
+ m = max m n)
with
| 0 =>
match n return (
snd (
diff 0
n)
+ 0
= max 0
n)
with
| 0 =>
eq_refl _
|
S _ =>
plusn0 _
end
|
S m =>
match n return (
snd (
diff (
S m)
n)
+ S m = max (
S m)
n)
with
| 0 =>
eq_refl (
snd (
diff (
S m) 0)
+ S m)
|
S n1 =>
let v :=
S (
max m n1)
in
eq_ind_r (
fun n =>
n = v)
(
eq_ind_r (
fun n =>
S n = v)
(
eq_refl v) (
diff_r _ _)) (
plusnS _ _)
end
end.
Variable w:
Type.
Definition castm (
m n:
nat) (
H:
m = n) (
x:
word w (
S m)):
(
word w (
S n)) :=
match H in (
_ = y)
return (
word w (
S y))
with
|
eq_refl =>
x
end.
Variable m:
nat.
Variable v: (
word w (
S m)).
Fixpoint extend_tr (
n :
nat) {
struct n}: (
word w (
S (
n + m))) :=
match n return (
word w (
S (
n + m)))
with
|
O =>
v
|
S n1 =>
WW W0 (
extend_tr n1)
end.
End ExtendMax.
Section Reduce.
Variable w :
Type.
Variable nT :
Type.
Variable N0 :
nT.
Variable eq0 :
w ->
bool.
Variable reduce_n :
w ->
nT.
Variable zn2z_to_Nt :
zn2z w ->
nT.
Definition reduce_n1 (
x:
zn2z w) :=
match x with
|
W0 =>
N0
|
WW xh xl =>
if eq0 xh then reduce_n xl
else zn2z_to_Nt x
end.
End Reduce.
Section ReduceRec.
Variable w :
Type.
Variable nT :
Type.
Variable N0 :
nT.
Variable reduce_1n :
zn2z w ->
nT.
Variable c :
forall n,
word w (
S n) ->
nT.
Fixpoint reduce_n (
n:
nat) :
word w (
S n) ->
nT :=
match n return word w (
S n) ->
nT with
|
O =>
reduce_1n
|
S m =>
fun x =>
match x with
|
W0 =>
N0
|
WW xh xl =>
match xh with
|
W0 => @
reduce_n m xl
|
_ => @
c (
S m)
x
end
end
end.
End ReduceRec.
Section CompareRec.
Variable wm w :
Type.
Variable w_0 :
w.
Variable compare :
w ->
w ->
comparison.
Variable compare0_m :
wm ->
comparison.
Variable compare_m :
wm ->
w ->
comparison.
Fixpoint compare0_mn (
n:
nat) :
word wm n ->
comparison :=
match n return word wm n ->
comparison with
|
O =>
compare0_m
|
S m =>
fun x =>
match x with
|
W0 =>
Eq
|
WW xh xl =>
match compare0_mn m xh with
|
Eq =>
compare0_mn m xl
|
r =>
Lt
end
end
end.
Variable wm_base:
positive.
Variable wm_to_Z:
wm ->
Z.
Variable w_to_Z:
w ->
Z.
Variable w_to_Z_0:
w_to_Z w_0 = 0.
Variable spec_compare0_m:
forall x,
compare0_m x = (w_to_Z w_0 ?= wm_to_Z x).
Variable wm_to_Z_pos:
forall x, 0
<= wm_to_Z x < base wm_base.
Let double_to_Z :=
double_to_Z wm_base wm_to_Z.
Let double_wB :=
double_wB wm_base.
Lemma base_xO:
forall n,
base (
xO n)
= (base n)^2.
Let double_to_Z_pos:
forall n x, 0
<= double_to_Z n x < double_wB n :=
(
spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos).
Lemma spec_compare0_mn:
forall n x,
compare0_mn n x = (0
?= double_to_Z n x).
Fixpoint compare_mn_1 (
n:
nat) :
word wm n ->
w ->
comparison :=
match n return word wm n ->
w ->
comparison with
|
O =>
compare_m
|
S m =>
fun x y =>
match x with
|
W0 =>
compare w_0 y
|
WW xh xl =>
match compare0_mn m xh with
|
Eq =>
compare_mn_1 m xl y
|
r =>
Gt
end
end
end.
Variable spec_compare:
forall x y,
compare x y = Z.compare (
w_to_Z x) (
w_to_Z y).
Variable spec_compare_m:
forall x y,
compare_m x y = Z.compare (
wm_to_Z x) (
w_to_Z y).
Variable wm_base_lt:
forall x,
0
<= w_to_Z x < base (
wm_base).
Let double_wB_lt:
forall n x,
0
<= w_to_Z x < (double_wB n).
Lemma spec_compare_mn_1:
forall n x y,
compare_mn_1 n x y = Z.compare (
double_to_Z n x) (
w_to_Z y).
End CompareRec.
Section AddS.
Variable w wm :
Type.
Variable incr :
wm ->
carry wm.
Variable addr :
w ->
wm ->
carry wm.
Variable injr :
w ->
zn2z wm.
Variable w_0 u:
w.
Fixpoint injs (
n:
nat):
word w (
S n) :=
match n return (
word w (
S n))
with
O =>
WW w_0 u
|
S n1 => (
WW W0 (
injs n1))
end.
Definition adds x y :=
match y with
W0 =>
C0 (
injr x)
|
WW hy ly =>
match addr x ly with
C0 z =>
C0 (
WW hy z)
|
C1 z =>
match incr hy with
C0 z1 =>
C0 (
WW z1 z)
|
C1 z1 =>
C1 (
WW z1 z)
end
end
end.
End AddS.
Fixpoint length_pos x :=
match x with xH =>
O |
xO x1 =>
S (
length_pos x1) |
xI x1 =>
S (
length_pos x1)
end.
Theorem length_pos_lt:
forall x y,
(
length_pos x < length_pos y)%
nat ->
Zpos x < Zpos y.
Theorem cancel_app:
forall A B (
f g:
A ->
B)
x,
f = g ->
f x = g x.
Section SimplOp.
Variable w:
Type.
Theorem digits_zop:
forall t (
ops :
ZnZ.Ops t),
ZnZ.digits (
mk_zn2z_ops ops)
= xO (
ZnZ.digits ops).
Theorem digits_kzop:
forall t (
ops :
ZnZ.Ops t),
ZnZ.digits (
mk_zn2z_ops_karatsuba ops)
= xO (
ZnZ.digits ops).
Theorem make_zop:
forall t (
ops :
ZnZ.Ops t),
@
ZnZ.to_Z _ (
mk_zn2z_ops ops)
=
fun z =>
match z with
|
W0 => 0
|
WW xh xl =>
ZnZ.to_Z xh * base (
ZnZ.digits ops)
+ ZnZ.to_Z xl
end.
Theorem make_kzop:
forall t (
ops:
ZnZ.Ops t),
@
ZnZ.to_Z _ (
mk_zn2z_ops_karatsuba ops)
=
fun z =>
match z with
|
W0 => 0
|
WW xh xl =>
ZnZ.to_Z xh * base (
ZnZ.digits ops)
+ ZnZ.to_Z xl
end.
End SimplOp.
Abstract vision of a datatype of arbitrary-large numbers.
Concrete operations can be derived from these generic
fonctions, in particular from iter_t and same_level.
The domains: a sequence of Z/nZ structures
The type t of arbitrary-large numbers, with abstract constructor mk_t
and destructor destr_t and iterator iter_t
Conversion to ZArith
reduce is like mk_t, but try to minimise the level of the number
Number of level in the tree representation of a number.
NB: This function isn't a morphism for setoid eq.
Definition level :=
iter_t (
fun n _ =>
n).
same_level and its rich specification, indexed by level
mk_t_S : building a number of the next level