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