The dyadic rationals are numbers of the shape m * 2 ^ e with m : Z and e : Z for some Integers implementation Z. These numbers form a ring and can be embedded into any Rationals implementation Q.
Require Import
Ring RelationClasses
abstract_algebra
interfaces.integers interfaces.naturals interfaces.rationals
orders.minmax orders.integers orders.rationals
nonneg_integers_naturals stdlib_rationals
theory.rationals theory.shiftl theory.int_pow theory.nat_pow theory.abs.

Implicit Arguments mant [[Z]].
Implicit Arguments expo [[Z]].

Infix "\$" := dyadic (at level 80).

Context `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder Zle Zlt}
`{equiv_dec : (x y : Z), Decision (x = y)}
`{le_dec : (x y : Z), Decision (x y)}
`{!ShiftLSpec Z (Z⁺) sl}.

Global Program Instance dy_plus: RingPlus Dyadic := λ x y,
if decide_rel (≤) (expo x) (expo y)
then mant x + mant y (expo y - expo x)↾_ \$ min (expo x) (expo y)
else mant x (expo x - expo y)↾_ + mant y \$ min (expo x) (expo y).

Global Instance dy_inject: Coerce Z Dyadic := λ x, x \$ 0.
Global Instance dy_opp: GroupInv Dyadic := λ x, -mant x \$ expo x.
Global Instance dy_mult: RingMult Dyadic := λ x y, mant x * mant y \$ expo x + expo y.

Section DtoQ_slow.
Context `{Rationals Q} `{Pow Q Z} (ZtoQ: Z Q).
Definition DtoQ_slow (x : Dyadic) := ZtoQ (mant x) * 2 ^ (expo x).
End DtoQ_slow.

Section with_rationals.
Context `{Rationals Q} `{!IntPowSpec Q Z ipw} `{!SemiRing_Morphism (ZtoQ: Z Q)}.

Notation DtoQ_slow' := (DtoQ_slow ZtoQ).

Lemma ZtoQ_shift (x n : Z) Pn : ZtoQ (x nPn) = ZtoQ x * 2 ^ n.

Lemma DtoQ_slow_preserves_plus x y : DtoQ_slow' (x + y) = DtoQ_slow' x + DtoQ_slow' y.

Lemma DtoQ_slow_preserves_opp x : DtoQ_slow' (-x) = -DtoQ_slow' x.

Lemma DtoQ_slow_preserves_mult x y : DtoQ_slow' (x * y) = DtoQ_slow' x * DtoQ_slow' y.

Lemma DtoQ_slow_preserves_0 : DtoQ_slow' 0 = 0.

Lemma DtoQ_slow_preserves_1 : DtoQ_slow' 1 = 1.
End with_rationals.

Notation StdQ := QArith_base.Q.
Notation ZtoStdQ := (integers.integers_to_ring Z StdQ).
Notation DtoStdQ := (DtoQ_slow ZtoStdQ).

Add Ring StdQ : (rings.stdlib_ring_theory StdQ).

Global Instance dy_equiv: Equiv Dyadic := λ x y, DtoStdQ x = DtoStdQ y.

Instance: Proper ((=) ==> (=)) DtoStdQ.

Instance: Injective DtoStdQ.

Instance: SemiRing_Morphism DtoStdQ.

Instance: Setoid_Morphism dy_inject.

Global Instance: Injective dy_inject.

Global Instance: SemiRing_Morphism dy_inject.

Lemma dy_eq_dec_aux (x y : Dyadic) p :
mant x = mant y (expo y - expo x)↾p x = y.

Lemma dy_eq_dec_aux_neg (x y : Dyadic) p :
mant x mant y (expo y - expo x)↾p x y.

Global Program Instance dy_eq_dec : (x y: Dyadic), Decision (x = y) := λ x y,
if decide_rel (≤) (expo x) (expo y)
then if decide_rel (=) (mant x) (mant y (expo y - expo x)↾_) then left _ else right _
else if decide_rel (=) (mant x (expo x - expo y)↾_) (mant y) then left _ else right _.

Global Instance dy_pow `{!Pow Z (Z⁺)} : Pow Dyadic (Z⁺) := λ x n, (mant x) ^ n \$ 'n * expo x.

Global Instance dy_pow_spec `{!NatPowSpec Z (Z⁺) pw} : NatPowSpec Dyadic (Z⁺) dy_pow.

Global Instance dy_shiftl: ShiftL Dyadic Z := λ x n, mant x \$ n + expo x.

Global Instance: ShiftLSpec Dyadic Z dy_shiftl.

Global Instance dy_le: Le Dyadic := λ x y, DtoStdQ x DtoStdQ y.
Global Instance dy_lt: Lt Dyadic := orders.dec_lt.

Instance: Proper ((=) ==> (=) ==> iff) dy_le.

Instance: OrderEmbedding DtoStdQ.

Instance: SemiRingOrder dy_le.

Instance: TotalRelation dy_le.

Global Instance: FullPseudoSemiRingOrder dy_le dy_lt.

Lemma nonneg_mant (x : Dyadic) : 0 x 0 mant x.

Lemma nonpos_mant (x : Dyadic) : x 0 mant x 0.

Global Program Instance dy_abs `{!Abs Z} : Abs Dyadic := λ x, abs (mant x) \$ expo x.

Lemma dy_le_dec_aux (x y : Dyadic) p :
mant x mant y (expo y - expo x)↾p x y.

Local Obligation Tactic := idtac.
Global Program Instance dy_le_dec : (x y: Dyadic), Decision (x y) := λ x y,
if decide_rel (≤) (expo x) (expo y)
then if decide_rel (≤) (mant x) (mant y (expo y - expo x)↾_) then left _ else right _
else if decide_rel (≤) (mant x (expo x - expo y)↾_) (mant y) then left _ else right _.

Section DtoQ.
Context `{Rationals Q} (ZtoQ: Z Q) `{!SemiRing_Morphism (ZtoQ: Z Q)}.

Local Obligation Tactic := program_simpl.
Program Definition DtoQ (x : Dyadic) : Q :=
if decide_rel (≤) 0 (expo x)
then ZtoQ (mant x (expo x)↾_)
else ZtoQ (mant x) / ZtoQ (1 (-expo x)↾_).
End DtoQ.

Section embed_rationals.
Context `{Rationals Q} `{!IntPowSpec Q Z ipw} `{!SemiRing_Morphism (ZtoQ: Z Q)}.
Context `{Apart Q} `{!TrivialApart Q} `{!FullPseudoSemiRingOrder Qlt Qle}.

Add Ring Q2 : (rings.stdlib_ring_theory Q).

Notation DtoQ' := (DtoQ ZtoQ).
Notation DtoQ_slow' := (DtoQ_slow ZtoQ).
Notation StdQtoQ := (rationals_to_rationals StdQ Q).

Lemma DtoQ_slow_correct : DtoQ_slow' = StdQtoQ DtoStdQ.

Global Instance: SemiRing_Morphism DtoQ_slow'.

Global Instance: Injective DtoQ_slow'.

Global Instance: OrderEmbedding DtoQ_slow'.

Lemma DtoQ_correct : DtoQ' = DtoQ_slow'.

Global Instance: SemiRing_Morphism DtoQ'.

Global Instance: Injective DtoQ'.

Global Instance: OrderEmbedding DtoQ'.
End embed_rationals.