proposition: Lemma to_of (d:decimal) : to_decimal (of_decimal d) = Some (dnorm d).
proof: Proof. case d as [i f|i f e]. - unfold of_decimal; simpl. case (uint_eq_dec f Nil); intro Hf. + rewrite Hf; clear f Hf. unfold to_decimal; simpl. rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. case i as [i|i]; [now simpl|]; simpl. rewrite app_nil_r. case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. + set (r := IRQ _). set (m := match f with Nil => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. unfold to_decimal; simpl. unfold IQmake_to_decimal; simpl. set (n := Nat.iter _ _ _). case (Pos.eq_dec n 1); intro Hn. { exfalso; apply Hf. now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } clear m; set (m := match n with 1%positive | _ => _ end). replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). 2:{ now unfold m; revert Hn; case n. } unfold QArith_base.IQmake_to_decimal, n; simpl. rewrite nztail_to_uint_pow10. clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. rewrite DecimalZ.to_of, abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnf. * rewrite (del_tail_app_int_exact _ _ Hnf). rewrite (del_head_app_int_exact _ _ Hnf). now rewrite (dnorm_i_exact _ _ Hnf). * rewrite (unorm_app_r _ _ Hnf). rewrite (iter_D0_unorm _ Hf). now rewrite dnorm_i_exact'. - unfold of_decimal; simpl. rewrite <-(DecimalZ.to_of e). case (Z.of_int e); clear e; [|intro e..]; simpl. + case (uint_eq_dec f Nil); intro Hf. * rewrite Hf; clear f Hf. unfold to_decimal; simpl. rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. case i as [i|i]; [now simpl|]; simpl. rewrite app_nil_r. case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. * set (r := IRQ _). set (m := match f with Nil => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. unfold to_decimal; simpl. unfold IQmake_to_decimal; simpl. set (n := Nat.iter _ _ _). case (Pos.eq_dec n 1); intro Hn. { exfalso; apply Hf. now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } clear m; set (m := match n with 1%positive | _ => _ end). replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). 2:{ now unfold m; revert Hn; case n. } unfold QArith_base.IQmake_to_decimal, n; simpl. rewrite nztail_to_uint_pow10. clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. rewrite DecimalZ.to_of, abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnf. -- rewrite (del_tail_app_int_exact _ _ Hnf). rewrite (del_head_app_int_exact _ _ Hnf). now rewrite (dnorm_i_exact _ _ Hnf). -- rewrite (unorm_app_r _ _ Hnf). rewrite (iter_D0_unorm _ Hf). now rewrite dnorm_i_exact'. + set (i' := match i with Pos _ => _ | _ => _ end). set (m := match Pos.to_uint e with Nil => _ | _ => _ end). replace m with (DecimalExp i' f (Pos (Pos.to_uint e))). 2:{ unfold m; generalize (Unsigned.to_uint_nonzero e). now case Pos.to_uint; [|intro u; case u|..]. } unfold i'; clear i' m. case (uint_eq_dec f Nil); intro Hf. * rewrite Hf; clear f Hf. unfold to_decimal; simpl. rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. case i as [i|i]; [now simpl|]; simpl. rewrite app_nil_r. case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. * set (r := IRQ _). set (m := match f with Nil => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. unfold to_decimal; simpl. unfold IQmake_to_decimal; simpl. set (n := Nat.iter _ _ _). case (Pos.eq_dec n 1); intro Hn. { exfalso; apply Hf. now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } clear m; set (m := match n with 1%positive | _ => _ end). replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). 2:{ now unfold m; revert Hn; case n. } unfold QArith_base.IQmake_to_decimal, n; simpl. rewrite nztail_to_uint_pow10. clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. rewrite DecimalZ.to_of, abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnf. -- rewrite (del_tail_app_int_exact _ _ Hnf). rewrite (del_head_app_int_exact _ _ Hnf). now rewrite (dnorm_i_exact _ _ Hnf). -- rewrite (unorm_app_r _ _ Hnf). rewrite (iter_D0_unorm _ Hf). now rewrite dnorm_i_exact'. + case (uint_eq_dec f Nil); intro Hf. * rewrite Hf; clear f Hf. unfold to_decimal; simpl. rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of. case i as [i|i]; [now simpl|]; simpl. rewrite app_nil_r. case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi]. now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead. * set (r := IRQ _). set (m := match f with Nil => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. unfold to_decimal; simpl. unfold IQmake_to_decimal; simpl. set (n := Nat.iter _ _ _). case (Pos.eq_dec n 1); intro Hn. { exfalso; apply Hf. now apply nb_digits_0; revert Hn; unfold n; case nb_digits. } clear m; set (m := match n with 1%positive | _ => _ end). replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n). 2:{ now unfold m; revert Hn; case n. } unfold QArith_base.IQmake_to_decimal, n; simpl. rewrite nztail_to_uint_pow10. clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _). clear m; set (m := match nb_digits f with 0 => _ | _ => _ end). replace m with r; [unfold r|now unfold m; revert Hf; case f]. rewrite DecimalZ.to_of, abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnf. -- rewrite (del_tail_app_int_exact _ _ Hnf). rewrite (del_head_app_int_exact _ _ Hnf). now rewrite (dnorm_i_exact _ _ Hnf). -- rewrite (unorm_app_r _ _ Hnf). rewrite (iter_D0_unorm _ Hf). now rewrite dnorm_i_exact'. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalZ DecimalQ Rdefinitions