Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleAdd
Set Implicit Arguments.
Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Local Open Scope Z_scope.
Section DoubleAdd.
Variable w :
Type.
Variable w_0 :
w.
Variable w_1 :
w.
Variable w_WW :
w ->
w ->
zn2z w.
Variable w_W0 :
w ->
zn2z w.
Variable ww_1 :
zn2z w.
Variable w_succ_c :
w ->
carry w.
Variable w_add_c :
w ->
w ->
carry w.
Variable w_add_carry_c :
w ->
w ->
carry w.
Variable w_succ :
w ->
w.
Variable w_add :
w ->
w ->
w.
Variable w_add_carry :
w ->
w ->
w.
Definition ww_succ_c x :=
match x with
|
W0 =>
C0 ww_1
|
WW xh xl =>
match w_succ_c xl with
|
C0 l =>
C0 (
WW xh l)
|
C1 l =>
match w_succ_c xh with
|
C0 h =>
C0 (
WW h w_0)
|
C1 h =>
C1 W0
end
end
end.
Definition ww_succ x :=
match x with
|
W0 =>
ww_1
|
WW xh xl =>
match w_succ_c xl with
|
C0 l =>
WW xh l
|
C1 l =>
w_W0 (
w_succ xh)
end
end.
Definition ww_add_c x y :=
match x,
y with
|
W0,
_ =>
C0 y
|
_,
W0 =>
C0 x
|
WW xh xl,
WW yh yl =>
match w_add_c xl yl with
|
C0 l =>
match w_add_c xh yh with
|
C0 h =>
C0 (
WW h l)
|
C1 h =>
C1 (
w_WW h l)
end
|
C1 l =>
match w_add_carry_c xh yh with
|
C0 h =>
C0 (
WW h l)
|
C1 h =>
C1 (
w_WW h l)
end
end
end.
Variable R :
Type.
Variable f0 f1 :
zn2z w ->
R.
Definition ww_add_c_cont x y :=
match x,
y with
|
W0,
_ =>
f0 y
|
_,
W0 =>
f0 x
|
WW xh xl,
WW yh yl =>
match w_add_c xl yl with
|
C0 l =>
match w_add_c xh yh with
|
C0 h =>
f0 (
WW h l)
|
C1 h =>
f1 (
w_WW h l)
end
|
C1 l =>
match w_add_carry_c xh yh with
|
C0 h =>
f0 (
WW h l)
|
C1 h =>
f1 (
w_WW h l)
end
end
end.
Definition ww_add x y :=
match x,
y with
|
W0,
_ =>
y
|
_,
W0 =>
x
|
WW xh xl,
WW yh yl =>
match w_add_c xl yl with
|
C0 l =>
WW (
w_add xh yh)
l
|
C1 l =>
WW (
w_add_carry xh yh)
l
end
end.
Definition ww_add_carry_c x y :=
match x,
y with
|
W0,
W0 =>
C0 ww_1
|
W0,
WW yh yl =>
ww_succ_c (
WW yh yl)
|
WW xh xl,
W0 =>
ww_succ_c (
WW xh xl)
|
WW xh xl,
WW yh yl =>
match w_add_carry_c xl yl with
|
C0 l =>
match w_add_c xh yh with
|
C0 h =>
C0 (
WW h l)
|
C1 h =>
C1 (
WW h l)
end
|
C1 l =>
match w_add_carry_c xh yh with
|
C0 h =>
C0 (
WW h l)
|
C1 h =>
C1 (
w_WW h l)
end
end
end.
Definition ww_add_carry x y :=
match x,
y with
|
W0,
W0 =>
ww_1
|
W0,
WW yh yl =>
ww_succ (
WW yh yl)
|
WW xh xl,
W0 =>
ww_succ (
WW xh xl)
|
WW xh xl,
WW yh yl =>
match w_add_carry_c xl yl with
|
C0 l =>
WW (
w_add xh yh)
l
|
C1 l =>
WW (
w_add_carry xh yh)
l
end
end.
Variable w_digits :
positive.
Variable w_to_Z :
w ->
Z.
Notation wB := (
base w_digits).
Notation wwB := (
base (
ww_digits w_digits)).
Notation "[| x |]" := (
w_to_Z x) (
at level 0,
x at level 99).
Notation "[+| c |]" :=
(
interp_carry 1
wB w_to_Z c) (
at level 0,
x at level 99).
Notation "[-| c |]" :=
(
interp_carry (-1)
wB w_to_Z c) (
at level 0,
x at level 99).
Notation "[[ x ]]" := (
ww_to_Z w_digits w_to_Z x)(
at level 0,
x at level 99).
Notation "[+[ c ]]" :=
(
interp_carry 1
wwB (
ww_to_Z w_digits w_to_Z)
c)
(
at level 0,
x at level 99).
Notation "[-[ c ]]" :=
(
interp_carry (-1)
wwB (
ww_to_Z w_digits w_to_Z)
c)
(
at level 0,
x at level 99).
Variable spec_w_0 :
[|w_0|] = 0.
Variable spec_w_1 :
[|w_1|] = 1.
Variable spec_ww_1 :
[[ww_1]] = 1.
Variable spec_to_Z :
forall x, 0
<= [|x|] < wB.
Variable spec_w_WW :
forall h l,
[[w_WW h l]] = [|h|] * wB + [|l|].
Variable spec_w_W0 :
forall h,
[[w_W0 h]] = [|h|] * wB.
Variable spec_w_succ_c :
forall x,
[+|w_succ_c x|] = [|x|] + 1.
Variable spec_w_add_c :
forall x y,
[+|w_add_c x y|] = [|x|] + [|y|].
Variable spec_w_add_carry_c :
forall x y,
[+|w_add_carry_c x y|] = [|x|] + [|y|] + 1.
Variable spec_w_succ :
forall x,
[|w_succ x|] = ([|x|] + 1
) mod wB.
Variable spec_w_add :
forall x y,
[|w_add x y|] = ([|x|] + [|y|]) mod wB.
Variable spec_w_add_carry :
forall x y,
[|w_add_carry x y|] = ([|x|] + [|y|] + 1
) mod wB.
Lemma spec_ww_succ_c :
forall x,
[+[ww_succ_c x]] = [[x]] + 1.
Lemma spec_ww_add_c :
forall x y,
[+[ww_add_c x y]] = [[x]] + [[y]].
Section Cont.
Variable P :
zn2z w ->
zn2z w ->
R ->
Prop.
Variable x y :
zn2z w.
Variable spec_f0 :
forall r,
[[r]] = [[x]] + [[y]] ->
P x y (
f0 r).
Variable spec_f1 :
forall r,
wwB + [[r]] = [[x]] + [[y]] ->
P x y (
f1 r).
Lemma spec_ww_add_c_cont :
P x y (
ww_add_c_cont x y).
End Cont.
Lemma spec_ww_add_carry_c :
forall x y,
[+[ww_add_carry_c x y]] = [[x]] + [[y]] + 1.
Lemma spec_ww_succ :
forall x,
[[ww_succ x]] = ([[x]] + 1
) mod wwB.
Lemma spec_ww_add :
forall x y,
[[ww_add x y]] = ([[x]] + [[y]]) mod wwB.
Lemma spec_ww_add_carry :
forall x y,
[[ww_add_carry x y]] = ([[x]] + [[y]] + 1
) mod wwB.
End DoubleAdd.