implementations.dyadics

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
  interfaces.additional_operations interfaces.orders
  orders.minmax orders.integers orders.rationals
  nonneg_integers_naturals stdlib_rationals
  theory.rationals theory.shiftl theory.int_pow theory.nat_pow theory.abs.

Record Dyadic Z := dyadic { mant: Z; expo: Z }.
Implicit Arguments dyadic [[Z]].
Implicit Arguments mant [[Z]].
Implicit Arguments expo [[Z]].

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

Section dyadics.
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}.

Notation Dyadic := (Dyadic Z).
Add Ring Z: (rings.stdlib_ring_theory Z).

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.
Global Instance dy_0: RingZero Dyadic := ('0 : Dyadic).
Global Instance dy_1: RingOne Dyadic := ('1 : Dyadic).

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)}.
  Add Ring Q: (rings.stdlib_ring_theory 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: Setoid Dyadic.

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

Instance: Injective DtoStdQ.

Global Instance: Ring Dyadic.

Global Instance dyadic_proper: Proper ((=) ==> (=) ==> (=)) dyadic.

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: ZeroProduct Dyadic.

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.

End dyadics.