Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase
Set Implicit Arguments.
Require Import ZArith Ndigits.
Require Import BigNumPrelude.
Require Import DoubleType.
Local Open Scope Z_scope.
Local Infix "<<" :=
Pos.shiftl_nat (
at level 30).
Section DoubleBase.
Variable w :
Type.
Variable w_0 :
w.
Variable w_1 :
w.
Variable w_Bm1 :
w.
Variable w_WW :
w ->
w ->
zn2z w.
Variable w_0W :
w ->
zn2z w.
Variable w_digits :
positive.
Variable w_zdigits:
w.
Variable w_add:
w ->
w ->
zn2z w.
Variable w_to_Z :
w ->
Z.
Variable w_compare :
w ->
w ->
comparison.
Definition ww_digits :=
xO w_digits.
Definition ww_zdigits :=
w_add w_zdigits w_zdigits.
Definition ww_to_Z :=
zn2z_to_Z (
base w_digits)
w_to_Z.
Definition ww_1 :=
WW w_0 w_1.
Definition ww_Bm1 :=
WW w_Bm1 w_Bm1.
Definition ww_WW xh xl :
zn2z (
zn2z w) :=
match xh,
xl with
|
W0,
W0 =>
W0
|
_,
_ =>
WW xh xl
end.
Definition ww_W0 h :
zn2z (
zn2z w) :=
match h with
|
W0 =>
W0
|
_ =>
WW h W0
end.
Definition ww_0W l :
zn2z (
zn2z w) :=
match l with
|
W0 =>
W0
|
_ =>
WW W0 l
end.
Definition double_WW (
n:
nat) :=
match n return word w n ->
word w n ->
word w (
S n)
with
|
O =>
w_WW
|
S n =>
fun (
h l :
zn2z (
word w n)) =>
match h,
l with
|
W0,
W0 =>
W0
|
_,
_ =>
WW h l
end
end.
Definition double_wB n :=
base (
w_digits << n).
Fixpoint double_to_Z (
n:
nat) :
word w n ->
Z :=
match n return word w n ->
Z with
|
O =>
w_to_Z
|
S n =>
zn2z_to_Z (
double_wB n) (
double_to_Z n)
end.
Fixpoint extend_aux (
n:
nat) (
x:
zn2z w) {
struct n}:
word w (
S n) :=
match n return word w (
S n)
with
|
O =>
x
|
S n1 =>
WW W0 (
extend_aux n1 x)
end.
Definition extend (
n:
nat) (
x:
w) :
word w (
S n) :=
let r :=
w_0W x in
match r with
|
W0 =>
W0
|
_ =>
extend_aux n r
end.
Definition double_0 n :
word w n :=
match n return word w n with
|
O =>
w_0
|
S _ =>
W0
end.
Definition double_split (
n:
nat) (
x:
zn2z (
word w n)) :=
match x with
|
W0 =>
match n return word w n * word w n with
|
O =>
(w_0,w_0)
|
S _ =>
(W0, W0)
end
|
WW h l =>
(h,l)
end.
Definition ww_compare x y :=
match x,
y with
|
W0,
W0 =>
Eq
|
W0,
WW yh yl =>
match w_compare w_0 yh with
|
Eq =>
w_compare w_0 yl
|
_ =>
Lt
end
|
WW xh xl,
W0 =>
match w_compare xh w_0 with
|
Eq =>
w_compare xl w_0
|
_ =>
Gt
end
|
WW xh xl,
WW yh yl =>
match w_compare xh yh with
|
Eq =>
w_compare xl yl
|
Lt =>
Lt
|
Gt =>
Gt
end
end.
Fixpoint get_low (
n :
nat) {
struct n}:
word w n ->
w :=
match n return (
word w n ->
w)
with
| 0%
nat =>
fun x =>
x
|
S n1 =>
fun x =>
match x with
|
W0 =>
w_0
|
WW _ x1 =>
get_low n1 x1
end
end.
Section DoubleProof.
Notation wB := (
base w_digits).
Notation wwB := (
base ww_digits).
Notation "[| x |]" := (
w_to_Z x) (
at level 0,
x at level 99).
Notation "[[ x ]]" := (
ww_to_Z x) (
at level 0,
x at level 99).
Notation "[+[ c ]]" :=
(
interp_carry 1
wwB ww_to_Z c) (
at level 0,
x at level 99).
Notation "[-[ c ]]" :=
(
interp_carry (-1)
wwB ww_to_Z c) (
at level 0,
x at level 99).
Notation "[! n | x !]" := (
double_to_Z n x) (
at level 0,
x at level 99).
Variable spec_w_0 :
[|w_0|] = 0.
Variable spec_w_1 :
[|w_1|] = 1.
Variable spec_w_Bm1 :
[|w_Bm1|] = wB - 1.
Variable spec_w_WW :
forall h l,
[[w_WW h l]] = [|h|] * wB + [|l|].
Variable spec_w_0W :
forall l,
[[w_0W l]] = [|l|].
Variable spec_to_Z :
forall x, 0
<= [|x|] < wB.
Variable spec_w_compare :
forall x y,
w_compare x y = Z.compare [|x|] [|y|].
Lemma wwB_wBwB :
wwB = wB^2.
Lemma spec_ww_1 :
[[ww_1]] = 1.
Lemma spec_ww_Bm1 :
[[ww_Bm1]] = wwB - 1.
Lemma lt_0_wB : 0
< wB.
Lemma lt_0_wwB : 0
< wwB.
Lemma wB_pos: 1
< wB.
Lemma wwB_pos: 1
< wwB.
Theorem wB_div_2: 2
* (wB / 2
) = wB.
Theorem wwB_div_2 :
wwB / 2
= wB / 2
* wB.
Lemma mod_wwB :
forall z x,
(z*wB + [|x|]) mod wwB = (z mod wB)*wB + [|x|].
Lemma wB_div :
forall x y,
([|x|] * wB + [|y|]) / wB = [|x|].
Lemma wB_div_plus :
forall x y p,
0
<= p ->
([|x|]*wB + [|y|]) / 2
^(Zpos w_digits + p) = [|x|] / 2
^p.
Lemma lt_wB_wwB :
wB < wwB.
Lemma w_to_Z_wwB :
forall x,
x < wB ->
x < wwB.
Lemma spec_ww_to_Z :
forall x, 0
<= [[x]] < wwB.
Lemma double_wB_wwB :
forall n,
double_wB n * double_wB n = double_wB (
S n).
Lemma double_wB_pos:
forall n, 0
<= double_wB n.
Lemma double_wB_more_digits:
forall n,
wB <= double_wB n.
Lemma spec_double_to_Z :
forall n (
x:
word w n), 0
<= [!n | x!] < double_wB n.
Lemma spec_get_low:
forall n x,
[!n | x!] < wB ->
[|get_low n x|] = [!n | x!].
Lemma spec_double_WW :
forall n (
h l :
word w n),
[!S n|double_WW n h l!] = [!n|h!] * double_wB n + [!n|l!].
Lemma spec_extend_aux :
forall n x,
[!S n|extend_aux n x!] = [[x]].
Lemma spec_extend :
forall n x,
[!S n|extend n x!] = [|x|].
Lemma spec_double_0 :
forall n,
[!n|double_0 n!] = 0.
Lemma spec_double_split :
forall n x,
let (
h,
l) :=
double_split n x in
[!S n|x!] = [!n|h!] * double_wB n + [!n|l!].
Lemma wB_lex_inv:
forall a b c d,
a < c ->
a * wB + [|b|] < c * wB + [|d|].
Ltac comp2ord :=
match goal with
| |-
Lt = (?x ?= ?y) =>
symmetry;
change (
x < y)
| |-
Gt = (?x ?= ?y) =>
symmetry;
change (
x > y);
apply Z.lt_gt
end.
Lemma spec_ww_compare :
forall x y,
ww_compare x y = Z.compare [[x]] [[y]].
End DoubleProof.
End DoubleBase.