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