Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleSub
Set Implicit Arguments.
Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Local Open Scope Z_scope.
Section DoubleSub.
Variable w :
Type.
Variable w_0 :
w.
Variable w_Bm1 :
w.
Variable w_WW :
w ->
w ->
zn2z w.
Variable ww_Bm1 :
zn2z w.
Variable w_opp_c :
w ->
carry w.
Variable w_opp_carry :
w ->
w.
Variable w_pred_c :
w ->
carry w.
Variable w_sub_c :
w ->
w ->
carry w.
Variable w_sub_carry_c :
w ->
w ->
carry w.
Variable w_opp :
w ->
w.
Variable w_pred :
w ->
w.
Variable w_sub :
w ->
w ->
w.
Variable w_sub_carry :
w ->
w ->
w.
Definition ww_opp_c x :=
match x with
|
W0 =>
C0 W0
|
WW xh xl =>
match w_opp_c xl with
|
C0 _ =>
match w_opp_c xh with
|
C0 h =>
C0 W0
|
C1 h =>
C1 (
WW h w_0)
end
|
C1 l =>
C1 (
WW (
w_opp_carry xh)
l)
end
end.
Definition ww_opp x :=
match x with
|
W0 =>
W0
|
WW xh xl =>
match w_opp_c xl with
|
C0 _ =>
WW (
w_opp xh)
w_0
|
C1 l =>
WW (
w_opp_carry xh)
l
end
end.
Definition ww_opp_carry x :=
match x with
|
W0 =>
ww_Bm1
|
WW xh xl =>
w_WW (
w_opp_carry xh) (
w_opp_carry xl)
end.
Definition ww_pred_c x :=
match x with
|
W0 =>
C1 ww_Bm1
|
WW xh xl =>
match w_pred_c xl with
|
C0 l =>
C0 (
w_WW xh l)
|
C1 _ =>
match w_pred_c xh with
|
C0 h =>
C0 (
WW h w_Bm1)
|
C1 _ =>
C1 ww_Bm1
end
end
end.
Definition ww_pred x :=
match x with
|
W0 =>
ww_Bm1
|
WW xh xl =>
match w_pred_c xl with
|
C0 l =>
w_WW xh l
|
C1 l =>
WW (
w_pred xh)
w_Bm1
end
end.
Definition ww_sub_c x y :=
match y,
x with
|
W0,
_ =>
C0 x
|
WW yh yl,
W0 =>
ww_opp_c (
WW yh yl)
|
WW yh yl,
WW xh xl =>
match w_sub_c xl yl with
|
C0 l =>
match w_sub_c xh yh with
|
C0 h =>
C0 (
w_WW h l)
|
C1 h =>
C1 (
WW h l)
end
|
C1 l =>
match w_sub_carry_c xh yh with
|
C0 h =>
C0 (
WW h l)
|
C1 h =>
C1 (
WW h l)
end
end
end.
Definition ww_sub x y :=
match y,
x with
|
W0,
_ =>
x
|
WW yh yl,
W0 =>
ww_opp (
WW yh yl)
|
WW yh yl,
WW xh xl =>
match w_sub_c xl yl with
|
C0 l =>
w_WW (
w_sub xh yh)
l
|
C1 l =>
WW (
w_sub_carry xh yh)
l
end
end.
Definition ww_sub_carry_c x y :=
match y,
x with
|
W0,
W0 =>
C1 ww_Bm1
|
W0,
WW xh xl =>
ww_pred_c (
WW xh xl)
|
WW yh yl,
W0 =>
C1 (
ww_opp_carry (
WW yh yl))
|
WW yh yl,
WW xh xl =>
match w_sub_carry_c xl yl with
|
C0 l =>
match w_sub_c xh yh with
|
C0 h =>
C0 (
w_WW h l)
|
C1 h =>
C1 (
WW h l)
end
|
C1 l =>
match w_sub_carry_c xh yh with
|
C0 h =>
C0 (
w_WW h l)
|
C1 h =>
C1 (
w_WW h l)
end
end
end.
Definition ww_sub_carry x y :=
match y,
x with
|
W0,
W0 =>
ww_Bm1
|
W0,
WW xh xl =>
ww_pred (
WW xh xl)
|
WW yh yl,
W0 =>
ww_opp_carry (
WW yh yl)
|
WW yh yl,
WW xh xl =>
match w_sub_carry_c xl yl with
|
C0 l =>
w_WW (
w_sub xh yh)
l
|
C1 l =>
w_WW (
w_sub_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_Bm1 :
[|w_Bm1|] = wB - 1.
Variable spec_ww_Bm1 :
[[ww_Bm1]] = wwB - 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_opp_c :
forall x,
[-|w_opp_c x|] = -[|x|].
Variable spec_opp :
forall x,
[|w_opp x|] = (-[|x|]) mod wB.
Variable spec_opp_carry :
forall x,
[|w_opp_carry x|] = wB - [|x|] - 1.
Variable spec_pred_c :
forall x,
[-|w_pred_c x|] = [|x|] - 1.
Variable spec_sub_c :
forall x y,
[-|w_sub_c x y|] = [|x|] - [|y|].
Variable spec_sub_carry_c :
forall x y,
[-|w_sub_carry_c x y|] = [|x|] - [|y|] - 1.
Variable spec_pred :
forall x,
[|w_pred x|] = ([|x|] - 1
) mod wB.
Variable spec_sub :
forall x y,
[|w_sub x y|] = ([|x|] - [|y|]) mod wB.
Variable spec_sub_carry :
forall x y,
[|w_sub_carry x y|] = ([|x|] - [|y|] - 1
) mod wB.
Lemma spec_ww_opp_c :
forall x,
[-[ww_opp_c x]] = -[[x]].
Lemma spec_ww_opp :
forall x,
[[ww_opp x]] = (-[[x]]) mod wwB.
Lemma spec_ww_opp_carry :
forall x,
[[ww_opp_carry x]] = wwB - [[x]] - 1.
Lemma spec_ww_pred_c :
forall x,
[-[ww_pred_c x]] = [[x]] - 1.
Lemma spec_ww_sub_c :
forall x y,
[-[ww_sub_c x y]] = [[x]] - [[y]].
Lemma spec_ww_sub_carry_c :
forall x y,
[-[ww_sub_carry_c x y]] = [[x]] - [[y]] - 1.
Lemma spec_ww_pred :
forall x,
[[ww_pred x]] = ([[x]] - 1
) mod wwB.
Lemma spec_ww_sub :
forall x y,
[[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.
Lemma spec_ww_sub_carry :
forall x y,
[[ww_sub_carry x y]] = ([[x]] - [[y]] - 1
) mod wwB.
End DoubleSub.