# 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.