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:
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,
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 CompOpp 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.