Library Interval.Float.Specific_bigint

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/

This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/

As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import Bool ZArith Reals Psatz.
From Bignums Require Import BigN BigZ.
From Flocq Require Import Zaux Raux Digits.

Require Import Basic.
Require Import Generic.
Require Import Generic_proof.
Require Import Specific_sig.

Module BigIntRadix2 <: FloatCarrier.

Definition radix := radix2.
Definition radix_correct := refl_equal Lt.
Definition smantissa_type := BigZ.t.
Definition mantissa_type := BigN.t.
Definition exponent_type := BigZ.t.

Definition MtoZ := BigZ.to_Z.
Definition ZtoM := BigZ.of_Z.
Definition MtoP v := match BigN.to_Z v with Zpos w ⇒ w | _ ⇒ xH end.
Definition PtoM := BigN.of_pos.
Definition EtoZ := BigZ.to_Z.
Definition ZtoE := BigZ.of_Z.

Definition valid_mantissa v := ∃ p , BigN.to_Z v = Zpos p.

Definition exponent_zero := 0%bigZ.
Definition exponent_one := 1%bigZ.
Definition exponent_neg := BigZ.opp.
Definition exponent_add := BigZ.add.
Definition exponent_sub := BigZ.sub.
Definition exponent_cmp := BigZ.compare.
Definition mantissa_zero := 0%bigZ.
Definition mantissa_one := 1%bigN.
Definition mantissa_add := BigN.add.
Definition mantissa_sub := BigN.sub.
Definition mantissa_mul := BigN.mul.
Definition mantissa_cmp := BigN.compare.
Definition mantissa_pos := BigZ.Pos.
Definition mantissa_neg := BigZ.Neg.

Definition mantissa_sign m :=
  if BigZ.eqb m 0%bigZ then Mzero
  else
    match m with
    | BigZ.Pos p ⇒ Mnumber false p
    | BigZ.Neg p ⇒ Mnumber true p
    end.

Definition mantissa_shl m d :=
  BigN.shiftl m (BigZ.to_N d).

Definition mantissa_scale2 (m : mantissa_type) (d : exponent_type) := (m , d ).

Definition mantissa_digits m :=
  BigZ.Pos (BigN.Ndigits m - BigN.head0 m)%bigN.

Definition mantissa_even m := BigN.even m.

Definition mantissa_split_div m d pos :=
  let (q, r) := BigN.div_eucl m d in (q ,
  if BigN.eqb r 0%bigN then
    match pos with pos_Eq ⇒ pos_Eq | _ ⇒ pos_Lo end
  else
    match BigN.compare (BigN.shiftl r 1%bigN) d with
    | Lt ⇒ pos_Lo
    | Eq ⇒ match pos with pos_Eq ⇒ pos_Mi | _ ⇒ pos_Up end
    | Gt ⇒ pos_Up
    end).

Definition mantissa_div :=
  fun m d ⇒ mantissa_split_div m d pos_Eq.

Definition mantissa_shr m d pos :=
  let dd := BigZ.to_N d in
  (BigN.shiftr m dd ,
  let d1 := BigN.pred dd in
  match BigN.compare (BigN.tail0 m) d1 with
  | Gt ⇒ match pos with pos_Eq ⇒ pos_Eq | _ ⇒ pos_Lo end
  | Eq ⇒ match pos with pos_Eq ⇒ pos_Mi | _ ⇒ pos_Up end
  | Lt ⇒
    if BigN.even (BigN.shiftr m d1) then pos_Lo
    else pos_Up
  end).

Definition mantissa_shrp m d pos :=
  match pos with
  | pos_Eq ⇒
        let dd := BigZ.to_N d in
         match BigN.compare (BigN.shiftl m 1) (BigN.shiftl 1 dd) with
        | Eq ⇒ pos_Mi
        | _ ⇒ pos_Up
        end
  | _ ⇒ pos_Up
  end.

Definition exponent_div2_floor e :=
  match e with
  | BigZ.Pos p ⇒
    (BigZ.Pos (BigN.shiftr p 1%bigN), negb (BigN.even p))
  | BigZ.Neg p ⇒
    let q := BigN.shiftr p 1%bigN in
    if BigN.even p then (BigZ.Neg q , false )
    else (BigZ.Neg (BigN.succ q), true )
  end.

Definition mantissa_sqrt m :=
  let s := BigN.sqrt m in
  let r := BigN.sub m (BigN.square s) in (s ,
  if BigN.eqb r 0%bigN then pos_Eq
  else match BigN.compare r s with Gt ⇒ pos_Up | _ ⇒ pos_Lo end).

Definition exponent_zero_correct := refl_equal Z0.
Definition exponent_one_correct := refl_equal 1%Z.
Definition mantissa_zero_correct := refl_equal Z0.

Definition ZtoM_correct := BigZ.spec_of_Z.
Definition ZtoE_correct := BigZ.spec_of_Z.
Definition exponent_neg_correct := BigZ.spec_opp.
Definition exponent_add_correct := BigZ.spec_add.
Definition exponent_sub_correct := BigZ.spec_sub.

Lemma exponent_div2_floor_correct :
  ∀ e, let (e',b) := exponent_div2_floor e in
  EtoZ e = (2 × EtoZ e' + if b then 1 else 0)%Z.

Lemma PtoM_correct :
  ∀ n, MtoP (PtoM n) = n.

Lemma mantissa_pos_correct :
  ∀ x, valid_mantissa x →
  MtoZ (mantissa_pos x) = Zpos (MtoP x).

Lemma mantissa_neg_correct :
  ∀ x, valid_mantissa x →
  MtoZ (mantissa_neg x) = Zneg (MtoP x).

Lemma mantissa_even_correct :
  ∀ x, valid_mantissa x →
  mantissa_even x = Z.even (Zpos (MtoP x)).

Lemma mantissa_one_correct :
  MtoP mantissa_one = xH ∧ valid_mantissa mantissa_one.

Lemma mantissa_add_correct :
  ∀ x y, valid_mantissa x → valid_mantissa y →
  MtoP (mantissa_add x y) = (MtoP x + MtoP y)%positive ∧
  valid_mantissa (mantissa_add x y).

Lemma mantissa_sub_correct :
  ∀ x y, valid_mantissa x → valid_mantissa y →
  (MtoP y < MtoP x)%positive →
  MtoP (mantissa_sub x y) = (MtoP x - MtoP y)%positive ∧
  valid_mantissa (mantissa_sub x y).

Lemma mantissa_mul_correct :
  ∀ x y, valid_mantissa x → valid_mantissa y →
  MtoP (mantissa_mul x y) = (MtoP x × MtoP y)%positive ∧
  valid_mantissa (mantissa_mul x y).

Lemma mantissa_cmp_correct :
  ∀ x y, valid_mantissa x → valid_mantissa y →
  mantissa_cmp x y = Z.compare (Zpos (MtoP x)) (Zpos (MtoP y)).

Lemma exponent_cmp_correct :
  ∀ x y, exponent_cmp x y = Z.compare (MtoZ x) (MtoZ y).

Lemma mantissa_digits_correct :
  ∀ x, valid_mantissa x →
  EtoZ (mantissa_digits x) = Zpos (count_digits radix (MtoP x)).

Lemma mantissa_scale2_correct :
  ∀ x d, valid_mantissa x →
  let (x',d') := mantissa_scale2 x d in
  (IZR (Zpos (MtoP x')) × bpow radix (EtoZ d') = IZR (Zpos (MtoP x)) × bpow radix2 (EtoZ d))%R ∧
  valid_mantissa x'.

Lemma mantissa_shl_correct :
  ∀ x y z, valid_mantissa y →
  EtoZ z = Zpos x →
  MtoP (mantissa_shl y z) = shift radix (MtoP y) x ∧ valid_mantissa (mantissa_shl y z).

Lemma mantissa_sign_correct :
  ∀ x,
  match mantissa_sign x with
  | Mzero ⇒ MtoZ x = Z0
  | Mnumber s p ⇒ MtoZ x = (if s then Zneg else Zpos) (MtoP p) ∧ valid_mantissa p
  end.

Lemma mantissa_shr_correct :
  ∀ x y z k, valid_mantissa y → EtoZ z = Zpos x →
  (Zpos (shift radix 1 x) ≤ Zpos (MtoP y))%Z →
  let (sq,l) := mantissa_shr y z k in
  let (q,r) := Z.div_eucl (Zpos (MtoP y)) (Zpos (shift radix 1 x)) in
  Zpos (MtoP sq) = q ∧
  l = adjust_pos r (shift radix 1 x) k ∧
  valid_mantissa sq.

Lemma mantissa_shrp_correct :
  ∀ x y z k, valid_mantissa y → EtoZ z = Zpos x →
  (Zpower radix (Zpos x - 1) ≤ Zpos (MtoP y) < Zpos (shift radix 1 x))%Z →
  let l := mantissa_shrp y z k in
  l = adjust_pos (Zpos (MtoP y)) (shift radix 1 x) k.

Lemma mantissa_div_correct :
  ∀ x y, valid_mantissa x → valid_mantissa y →
  (Zpos (MtoP y) ≤ Zpos (MtoP x))%Z →
  let (q,l) := mantissa_div x y in
  Zpos (MtoP q) = (Zpos (MtoP x) / Zpos (MtoP y))%Z ∧
  Bracket.inbetween_int (Zpos (MtoP q)) (IZR (Zpos (MtoP x)) / IZR (Zpos (MtoP y)))%R (convert_location_inv l) ∧
  valid_mantissa q.

Lemma mantissa_sqrt_correct :
  ∀ x, valid_mantissa x →
  let (q,l) := mantissa_sqrt x in
  let (s,r) := Z.sqrtrem (Zpos (MtoP x)) in
  Zpos (MtoP q) = s ∧
  match l with pos_Eq ⇒ r = Z0 | pos_Lo ⇒ (0 < r ≤ s)%Z | pos_Mi ⇒ False | pos_Up ⇒ (s < r)%Z end ∧
  valid_mantissa q.

End BigIntRadix2.