proposition: Lemma to_of (d:hexadecimal) : to_hexadecimal (of_hexadecimal d) = Some (dnorm d).
proof: Proof. case d as [i f|i f e]. - unfold of_hexadecimal; simpl; unfold IQmake_to_hexadecimal'. rewrite IZ_to_Z_IZ_of_Z. unfold IQmake_to_hexadecimal; simpl. change (fun _ : positive => _) with (Pos.mul 16). rewrite nztail_to_hex_uint_pow16, to_of. case_eq (nb_digits f); [|intro nb]; intro Hnb. + rewrite (nb_digits_0 _ Hnb), app_int_nil_r. case i as [ni|ni]; [now simpl|]. rewrite app_nil_r; simpl; unfold unorm. now case (nzhead ni). + rewrite <-Hnb. rewrite abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnb'. * rewrite (del_tail_app_int_exact _ _ Hnb'). rewrite (del_head_app_int_exact _ _ Hnb'). now rewrite (dnorm_i_exact _ _ Hnb'). * rewrite (unorm_app_r _ _ Hnb'). rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. now rewrite dnorm_i_exact'. - unfold of_hexadecimal; simpl. rewrite <-DecimalZ.to_of. case (Z.of_int e); clear e; [|intro e..]; simpl. + unfold IQmake_to_hexadecimal'. rewrite IZ_to_Z_IZ_of_Z. unfold IQmake_to_hexadecimal; simpl. change (fun _ : positive => _) with (Pos.mul 16). rewrite nztail_to_hex_uint_pow16, to_of. case_eq (nb_digits f); [|intro nb]; intro Hnb. * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. case i as [ni|ni]; [now simpl|]. rewrite app_nil_r; simpl; unfold unorm. now case (nzhead ni). * rewrite <-Hnb. rewrite abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnb'. -- rewrite (del_tail_app_int_exact _ _ Hnb'). rewrite (del_head_app_int_exact _ _ Hnb'). now rewrite (dnorm_i_exact _ _ Hnb'). -- rewrite (unorm_app_r _ _ Hnb'). rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. now rewrite dnorm_i_exact'. + unfold IQmake_to_hexadecimal'. rewrite IZ_to_Z_IZ_of_Z. unfold IQmake_to_hexadecimal; simpl. change (fun _ : positive => _) with (Pos.mul 16). rewrite nztail_to_hex_uint_pow16, to_of. generalize (DecimalPos.Unsigned.to_uint_nonzero e); intro He. set (dnorm_i := match i with Pos _ => _ | _ => _ end). set (m := match Pos.to_uint e with Decimal.Nil => _ | _ => _ end). replace m with (HexadecimalExp dnorm_i f (Decimal.Pos (Pos.to_uint e))). 2:{ now unfold m; revert He; case (Pos.to_uint e); [|intro u; case u|..]. } clear m; unfold dnorm_i. case_eq (nb_digits f); [|intro nb]; intro Hnb. * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. case i as [ni|ni]; [now simpl|]. rewrite app_nil_r; simpl; unfold unorm. now case (nzhead ni). * rewrite <-Hnb. rewrite abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnb'. -- rewrite (del_tail_app_int_exact _ _ Hnb'). rewrite (del_head_app_int_exact _ _ Hnb'). now rewrite (dnorm_i_exact _ _ Hnb'). -- rewrite (unorm_app_r _ _ Hnb'). rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. now rewrite dnorm_i_exact'. + unfold IQmake_to_hexadecimal'. rewrite IZ_to_Z_IZ_of_Z. unfold IQmake_to_hexadecimal; simpl. change (fun _ : positive => _) with (Pos.mul 16). rewrite nztail_to_hex_uint_pow16, to_of. case_eq (nb_digits f); [|intro nb]; intro Hnb. * rewrite (nb_digits_0 _ Hnb), app_int_nil_r. case i as [ni|ni]; [now simpl|]. rewrite app_nil_r; simpl; unfold unorm. now case (nzhead ni). * rewrite <-Hnb. rewrite abs_norm, abs_app_int. case Nat.ltb_spec; intro Hnb'. -- rewrite (del_tail_app_int_exact _ _ Hnb'). rewrite (del_head_app_int_exact _ _ Hnb'). now rewrite (dnorm_i_exact _ _ Hnb'). -- rewrite (unorm_app_r _ _ Hnb'). rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb]. now rewrite dnorm_i_exact'. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith