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.