proposition: Lemma of_IQmake_to_hexadecimal num den : match IQmake_to_hexadecimal num den with | None => True | Some (HexadecimalExp _ _ _) => False | Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IQmake (IZ_of_Z num) den end.
proof: Proof. unfold IQmake_to_hexadecimal. generalize (Unsigned.nztail_to_hex_uint den). case Hexadecimal.nztail; intros den' e_den'. case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'. case den'; [ |now simpl..]; clear den'. case e_den' as [|e_den']; simpl; injection 1 as ->. { now unfold of_hexadecimal; simpl; rewrite app_int_nil_r, HexadecimalZ.of_to. } replace (16 ^ _)%positive with (Nat.iter (S e_den') (Pos.mul 16) 1%positive). 2:{ induction e_den' as [|n IHn]; [now simpl| ]. now rewrite SuccNat2Pos.inj_succ, Pos.pow_succ_r, <-IHn. } case Nat.ltb_spec; intro He_den'. - unfold of_hexadecimal; simpl. rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl]. rewrite HexadecimalZ.of_to. now rewrite nb_digits_del_head_sub; [|now apply Nat.lt_le_incl]. - unfold of_hexadecimal; simpl. rewrite nb_digits_iter_D0. apply f_equal2. + apply f_equal, HexadecimalZ.to_int_inj. rewrite HexadecimalZ.to_of. rewrite <-(HexadecimalZ.of_to num), HexadecimalZ.to_of. case (Z.to_hex_int num); clear He_den' num; intro num; simpl. * unfold app; simpl. now rewrite unorm_D0, unorm_iter_D0, unorm_involutive. * case (uint_eq_dec (nzhead num) Nil); [|intro Hn]. { intros->; simpl; unfold app; simpl. now rewrite unorm_D0, unorm_iter_D0. } replace (match nzhead num with Nil => _ | _ => _ end) with (Neg (nzhead num)); [|now revert Hn; case nzhead]. simpl. rewrite nzhead_iter_D0, nzhead_involutive. now revert Hn; case nzhead. + revert He_den'; case nb_digits as [|n]; [now simpl; rewrite Nat.add_0_r|]. intro Hn. rewrite Nat.add_succ_r, Nat.sub_add; [|apply le_S_n]; auto. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith