Require Import Decimal DecimalFacts PArith NArith.

Module Unsigned.

Local Open Scope N.

Fixpoint of_lu (d:uint) : N :=
  match d with
  | Nil => 0
  | D0 d => 10 * of_lu d
  | D1 d => 1 + 10 * of_lu d
  | D2 d => 2 + 10 * of_lu d
  | D3 d => 3 + 10 * of_lu d
  | D4 d => 4 + 10 * of_lu d
  | D5 d => 5 + 10 * of_lu d
  | D6 d => 6 + 10 * of_lu d
  | D7 d => 7 + 10 * of_lu d
  | D8 d => 8 + 10 * of_lu d
  | D9 d => 9 + 10 * of_lu d
  end.

Definition hd d :=
match d with
 | Nil => 0
 | D0 _ => 0
 | D1 _ => 1
 | D2 _ => 2
 | D3 _ => 3
 | D4 _ => 4
 | D5 _ => 5
 | D6 _ => 6
 | D7 _ => 7
 | D8 _ => 8
 | D9 _ => 9
end.

Definition tl d :=
 match d with
 | Nil => d
 | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d
end.

Lemma of_lu_eqn d :
 of_lu d = hd d + 10 * (of_lu (tl d)).

Ltac simpl_of_lu :=
 match goal with
 | |- context [ of_lu (?f ?x) ] =>
   rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
 end.

Fixpoint usize (d:uint) : N :=
  match d with
  | Nil => 0
  | D0 d => N.succ (usize d)
  | D1 d => N.succ (usize d)
  | D2 d => N.succ (usize d)
  | D3 d => N.succ (usize d)
  | D4 d => N.succ (usize d)
  | D5 d => N.succ (usize d)
  | D6 d => N.succ (usize d)
  | D7 d => N.succ (usize d)
  | D8 d => N.succ (usize d)
  | D9 d => N.succ (usize d)
  end.

Lemma of_lu_revapp d d' :
 of_lu (revapp d d') =
  of_lu (rev d) + of_lu d' * 10^usize d.

Definition Nadd n p :=
 match n with
 | N0 => p
 | Npos p0 => (p0+p)%positive
 end.

Lemma Nadd_simpl n p q : Npos (Nadd n (p * q)) = n + Npos p * Npos q.

Lemma of_uint_acc_eqn d acc : d<>Nil ->
 Pos.of_uint_acc d acc = Pos.of_uint_acc (tl d) (Nadd (hd d) (10*acc)).

Lemma of_uint_acc_rev d acc :
 Npos (Pos.of_uint_acc d acc) =
  of_lu (rev d) + (Npos acc) * 10^usize d.

Lemma of_uint_alt d : Pos.of_uint d = of_lu (rev d).

Lemma of_lu_rev d : Pos.of_uint (rev d) = of_lu d.

Lemma of_lu_double_gen d :
  of_lu (Little.double d) = N.double (of_lu d) /\
  of_lu (Little.succ_double d) = N.succ_double (of_lu d).

Lemma of_lu_double d :
  of_lu (Little.double d) = N.double (of_lu d).

Lemma of_lu_succ_double d :
  of_lu (Little.succ_double d) = N.succ_double (of_lu d).

Lemma of_to (p:positive) : Pos.of_uint (Pos.to_uint p) = Npos p.

Definition to_lu n :=
  match n with
  | N0 => Decimal.zero
  | Npos p => Pos.to_little_uint p
  end.

Lemma succ_double_alt d :
  Little.succ_double d = Little.succ (Little.double d).

Lemma double_succ d :
  Little.double (Little.succ d) =
  Little.succ (Little.succ_double d).

Lemma to_lu_succ n :
 to_lu (N.succ n) = Little.succ (to_lu n).

Lemma nat_iter_S n {A} (f:A->A) i :
 Nat.iter (S n) f i = f (Nat.iter n f i).

Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i.

Lemma to_ldec_tenfold p :
 to_lu (10 * Npos p) = D0 (to_lu (Npos p)).

Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.

Lemma to_of_lu_tenfold d :
 to_lu (of_lu d) = lnorm d ->
 to_lu (10 * of_lu d) = lnorm (D0 d).

Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m.

Ltac simpl_to_nat := simpl N.to_nat; unfold Pos.to_nat; simpl Pos.iter_op.

Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.

Lemma to_of (d:uint) : N.to_uint (Pos.of_uint d) = unorm d.

Lemma to_uint_nonzero p : Pos.to_uint p <> zero.

Lemma to_uint_nonnil p : Pos.to_uint p <> Nil.

Lemma to_uint_inj p p' : Pos.to_uint p = Pos.to_uint p' -> p = p'.

Lemma to_uint_pos_surj d :
 unorm d<>zero -> exists p, Pos.to_uint p = unorm d.

Lemma of_uint_norm d : Pos.of_uint (unorm d) = Pos.of_uint d.

Lemma of_inj d d' :
 Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'.

Lemma of_iff d d' : Pos.of_uint d = Pos.of_uint d' <-> unorm d = unorm d'.

End Unsigned.

Module Signed.

Lemma of_to (p:positive) : Pos.of_int (Pos.to_int p) = Some p.

Lemma to_of (d:int)(p:positive) :
 Pos.of_int d = Some p -> Pos.to_int p = norm d.

Lemma to_int_inj p p' : Pos.to_int p = Pos.to_int p' -> p = p'.

Lemma to_int_pos_surj d :
 unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d).

Lemma of_int_norm d : Pos.of_int (norm d) = Pos.of_int d.

Lemma of_inj_pos d d' :
 Pos.of_int (Pos d) = Pos.of_int (Pos d') -> unorm d = unorm d'.

End Signed.