Library Coq.Numbers.Natural.BigN.Nbasic
Require Import ZArith.
Require Import BigNumPrelude.
Require Import Max.
Require Import DoubleType.
Require Import DoubleBase.
Require Import CyclicAxioms.
Require Import DoubleCyclic.
Fixpoint plength (
p:
positive) :
positive :=
match p with
xH =>
xH
|
xO p1 =>
Psucc (
plength p1)
|
xI p1 =>
Psucc (
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 (
Ppred p)))%Z.
Definition Pdiv p q :=
match Zdiv (
Zpos p) (
Zpos q)
with
Zpos q1 =>
match (
Zpos p) - (
Zpos q) * (
Zpos q1)
with
Z0 =>
q1
|
_ => (
Psucc 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 Psucc (
plength (
Ppred 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 =>
refl_equal (
S m)
|
S n1 =>
let v :=
S (
S n1 +
m)
in
eq_ind_r (
fun n =>
S n =
v) (
refl_equal v) (
plusnS n1 m)
end.
Fixpoint plusn0 n :
n + 0 =
n :=
match n return (
n + 0 =
n)
with
| 0 =>
refl_equal 0
|
S n1 =>
let v :=
S n1 in
eq_ind_r (
fun n :
nat =>
S n =
v) (
refl_equal 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 =>
refl_equal _
|
S n0 =>
refl_equal _
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) (
refl_equal 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 =>
refl_equal _
|
S _ =>
plusn0 _
end
|
S m =>
match n return (
snd (
diff (
S m)
n) +
S m =
max (
S m)
n)
with
| 0 =>
refl_equal (
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)
(
refl_equal 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
|
refl_equal =>
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.
Implicit Arguments extend_tr[
w m].
Implicit Arguments castm[
w m n].
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:zn2
z 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.
Definition opp_compare cmp :=
match cmp with
|
Lt =>
Gt
|
Eq =>
Eq
|
Gt =>
Lt
end.
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,
match compare0_m x with
Eq =>
w_to_Z w_0 =
wm_to_Z x
|
Lt =>
w_to_Z w_0 <
wm_to_Z x
|
Gt =>
w_to_Z w_0 >
wm_to_Z x
end.
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,
match compare0_mn n x with
Eq => 0 =
double_to_Z n x
|
Lt => 0 <
double_to_Z n x
|
Gt => 0 >
double_to_Z n x
end.
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,
match compare x y with
Eq =>
w_to_Z x =
w_to_Z y
|
Lt =>
w_to_Z x <
w_to_Z y
|
Gt =>
w_to_Z x >
w_to_Z y
end.
Variable spec_compare_m:
forall x y,
match compare_m x y with
Eq =>
wm_to_Z x =
w_to_Z y
|
Lt =>
wm_to_Z x <
w_to_Z y
|
Gt =>
wm_to_Z x >
w_to_Z y
end.
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,
match compare_mn_1 n x y with
Eq =>
double_to_Z n x =
w_to_Z y
|
Lt =>
double_to_Z n x <
w_to_Z y
|
Gt =>
double_to_Z n x >
w_to_Z y
end.
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.
Lemma spec_opp:
forall u x y,
match u with
|
Eq =>
y =
x
|
Lt =>
y <
x
|
Gt =>
y >
x
end ->
match opp_compare u with
|
Eq =>
x =
y
|
Lt =>
x <
y
|
Gt =>
x >
y
end.
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 w (
x:
znz_op w),
znz_digits (
mk_zn2z_op x) =
xO (
znz_digits x).
Theorem digits_kzop:
forall w (
x:
znz_op w),
znz_digits (
mk_zn2z_op_karatsuba x) =
xO (
znz_digits x).
Theorem make_zop:
forall w (
x:
znz_op w),
znz_to_Z (
mk_zn2z_op x) =
fun z =>
match z with
W0 => 0
|
WW xh xl =>
znz_to_Z x xh *
base (
znz_digits x)
+
znz_to_Z x xl
end.
Theorem make_kzop:
forall w (
x:
znz_op w),
znz_to_Z (
mk_zn2z_op_karatsuba x) =
fun z =>
match z with
W0 => 0
|
WW xh xl =>
znz_to_Z x xh *
base (
znz_digits x)
+
znz_to_Z x xl
end.
End SimplOp.