proposition: Lemma of_to (q:IR) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q.
proof: Proof. intro d. case q as [z|q|r r'|r r']; simpl. - case z as [z p| |p|p]. + now simpl. + now simpl; injection 1 as <-. + simpl; injection 1 as <-. now unfold of_hexadecimal; simpl; unfold Z.of_hex_uint; rewrite Unsigned.of_to. + simpl; injection 1 as <-. now unfold of_hexadecimal; simpl; unfold Z.of_hex_uint; rewrite Unsigned.of_to. - case q as [num den]. generalize (of_IQmake_to_hexadecimal num den). case IQmake_to_hexadecimal as [d'|]; [|now simpl]. case d' as [i f|]; [|now simpl]. now intros H; injection 1 as <-. - case r as [z|q| |]; [|case q as[num den]|now simpl..]; (case r' as [z'| | |]; [|now simpl..]); (case z' as [p e| | |]; [|now simpl..]). + case (Z.eq_dec p 2); [intros->|intro Hp]. 2:{ now revert Hp; case p; [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } case z as [| |p|p]; [now simpl|..]; injection 1 as <-. * now unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. now unfold Z.of_hex_uint; rewrite Unsigned.of_to. * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. now unfold Z.of_hex_uint; rewrite Unsigned.of_to. + case (Z.eq_dec p 2); [intros->|intro Hp]. 2:{ now revert Hp; case p; [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } generalize (of_IQmake_to_hexadecimal num den). case IQmake_to_hexadecimal as [d'|]; [|now simpl]. case d' as [i f|]; [|now simpl]. intros H; injection 1 as <-. unfold of_hexadecimal; simpl. change (match f with Nil => _ | _ => _ end) with (of_hexadecimal (Hexadecimal i f)). rewrite H; clear H. now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. - case r as [z|q| |]; [|case q as[num den]|now simpl..]; (case r' as [z'| | |]; [|now simpl..]); (case z' as [p e| | |]; [|now simpl..]). + case (Z.eq_dec p 2); [intros->|intro Hp]. 2:{ now revert Hp; case p; [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } case z as [| |p|p]; [now simpl|..]; injection 1 as <-. * now unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. now unfold Z.of_hex_uint; rewrite Unsigned.of_to. * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. now unfold Z.of_hex_uint; rewrite Unsigned.of_to. + case (Z.eq_dec p 2); [intros->|intro Hp]. 2:{ now revert Hp; case p; [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. } generalize (of_IQmake_to_hexadecimal num den). case IQmake_to_hexadecimal as [d'|]; [|now simpl]. case d' as [i f|]; [|now simpl]. intros H; injection 1 as <-. unfold of_hexadecimal; simpl. change (match f with Nil => _ | _ => _ end) with (of_hexadecimal (Hexadecimal i f)). rewrite H; clear H. now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. Qed.
imports: Decimal DecimalFacts Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ HexadecimalQ Rdefinitions