DecimalQ

Proofs that conversions between decimal numbers and Q are bijections.

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

Some consequences