Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith.

Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q.

Definition dnorme (d:decimal) : decimal :=
  let '(i, f, e) :=
    match d with
    | Decimal i f => (i, f, Pos Nil)
    | DecimalExp i f e => (i, f, e)
    end in
  let i := norm (app_int i f) in
  let e := norm (Z.to_int (Z.of_int e - Z.of_nat (nb_digits f))) in
  match e with
  | Pos zero => Decimal i Nil
  | _ => DecimalExp i Nil e
  end.

Definition dnormf (d:decimal) : decimal :=
  match dnorme d with
  | Decimal i _ => Decimal i Nil
  | DecimalExp i _ e =>
    match Z.of_int e with
    | Z0 => Decimal i Nil
    | Zpos e => Decimal (norm (app_int i (Pos.iter D0 Nil e))) Nil
    | Zneg e =>
      let ne := Pos.to_nat e in
      let ai := match i with Pos d | Neg d => d end in
      let ni := nb_digits ai in
      if ne <? ni then
        Decimal (del_tail_int ne i) (del_head (ni - ne) ai)
      else
        let z := match i with Pos _ => Pos zero | Neg _ => Neg zero end in
        Decimal z (Nat.iter (ne - ni) D0 ai)
    end
  end.

Lemma dnorme_spec d :
  match dnorme d with
  | Decimal i Nil => i = norm i
  | DecimalExp i Nil e => i = norm i /\ e = norm e /\ e <> Pos zero
  | _ => False
  end.

Lemma dnormf_spec d :
  match dnormf d with
  | Decimal i f => i = Neg zero \/ i = norm i
  | _ => False
  end.

Lemma dnorme_invol d : dnorme (dnorme d) = dnorme d.

Lemma dnormf_invol d : dnormf (dnormf d) = dnormf d.

Lemma to_of (d:decimal) :
  to_decimal (of_decimal d) = Some (dnorme d)
  \/ to_decimal (of_decimal d) = Some (dnormf d).

Lemma to_decimal_inj q q' :
  to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'.

Lemma to_decimal_surj d :
  exists q, to_decimal q = Some (dnorme d) \/ to_decimal q = Some (dnormf d).

Lemma of_decimal_dnorme d : of_decimal (dnorme d) = of_decimal d.

Lemma of_decimal_dnormf d : of_decimal (dnormf d) = of_decimal d.