Library Interval.Float.Specific_stdz

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 ZArith Reals Psatz Bool.
From Flocq Require Import Zaux Raux.

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

Module StdZRadix2 <: FloatCarrier.

Definition radix := radix2.
Definition radix_correct := refl_equal Lt.
Definition smantissa_type := Z.
Definition mantissa_type := positive.
Definition exponent_type := Z.

Definition MtoP := fun (m : positive) ⇒ m.
Definition PtoM := fun (m : positive) ⇒ m.
Definition MtoZ := fun (m : Z) ⇒ m.
Definition ZtoM := fun (m : Z) ⇒ m.
Definition EtoZ := fun (e : Z) ⇒ e.
Definition ZtoE := fun (e : Z) ⇒ e.

Definition exponent_zero := Z0.
Definition exponent_one := Zpos xH.
Definition exponent_neg := Z.opp.
Definition exponent_add := Zplus.
Definition exponent_sub := Zminus.
Definition exponent_cmp := Z.compare.
Definition mantissa_zero := Z0.
Definition mantissa_one := xH.
Definition mantissa_add := Pplus.
Definition mantissa_sub := Pminus.
Definition mantissa_mul := Pmult.
Definition mantissa_cmp x y := Pcompare x y Eq.
Definition mantissa_pos := Zpos.
Definition mantissa_neg := Zneg.

Definition valid_mantissa := fun (m : positive) ⇒ True.

Definition mantissa_sign m :=
  match m with
  | Zneg p ⇒ Mnumber true p
  | Z0 ⇒ Mzero
  | Zpos p ⇒ Mnumber false p
  end.

Definition mantissa_even m :=
  match m with
  | xO _ ⇒ true
  | _ ⇒ false
  end.

Definition mantissa_shl m d :=
  match d with Zpos nb ⇒ iter_pos (fun x ⇒ xO x) nb m | _ ⇒ xH end.

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

Fixpoint digits_aux m nb { struct m } :=
  match m with
  | xH ⇒ nb
  | xO p ⇒ digits_aux p (Pos.succ nb)
  | xI p ⇒ digits_aux p (Pos.succ nb)
  end.

Definition mantissa_digits m := Zpos (digits_aux m xH).

Definition mantissa_split_div m d pos :=
  match Zfast_div_eucl (Zpos m) (Zpos d) with
  | (Zpos q, r) ⇒ (q, adjust_pos r d pos )
  | _ ⇒ (xH , pos_Eq )
  end.

Definition mantissa_shr_aux v :=
  match v with
  | (xO p, pos_Eq ) ⇒ (p, pos_Eq )
  | (xO p, _) ⇒ (p, pos_Lo )
  | (xI p, pos_Eq ) ⇒ (p, pos_Mi )
  | (xI p, _) ⇒ (p, pos_Up )
  | _ ⇒ (xH , pos_Eq )
  end.

Definition mantissa_shr m d pos :=
  match d with
  | Zpos nb ⇒
    iter_pos mantissa_shr_aux nb (m , pos )
  | _ ⇒ (xH , pos_Eq )
  end.

Fixpoint mantissa_shrp_aux m d :=
  match m with
  | xO m1 ⇒
      if (d =? 1)%positive then pos_Up else mantissa_shrp_aux m1 (Pos.pred d)
  | xI m1 ⇒ pos_Up
  | xH ⇒
      if (d =? 1)%positive then pos_Mi else pos_Up
  end.

Lemma mantissa_shrp_aux_correct m d :
   mantissa_shrp_aux m (Pos.succ d) =
   match (m ?= shift radix 1 d)%positive with
        | Eq ⇒ pos_Mi
        | _ ⇒ pos_Up
        end.

Definition mantissa_shrp m d pos :=
  match pos with
  | pos_Eq ⇒ mantissa_shrp_aux m (Z.to_pos d)
  | _ ⇒ pos_Up
  end.

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

Definition exponent_div2_floor n :=
  match n with
  | Z0 ⇒ (Z0 , false )
  | Zpos xH ⇒ (Z0 , true )
  | Zneg xH ⇒ (Zneg xH , true )
  | Zpos (xO p) ⇒ (Zpos p, false )
  | Zneg (xO p) ⇒ (Zneg p, false )
  | Zpos (xI p) ⇒ (Zpos p, true )
  | Zneg (xI p) ⇒ (Zneg (Pos.succ p), true )
  end.

Definition mantissa_sqrt m :=
  match Z.sqrtrem (Zpos m) with
  | (Zpos s, r) ⇒
    let pos :=
      match r with
      | Z0 ⇒ pos_Eq
      | Zpos r ⇒
        match Pos.compare r s with
        | Gt ⇒ pos_Up
        | _ ⇒ pos_Lo
        end
      | Zneg _ ⇒ pos_Eq
      end in
    (s, pos )
  | _ ⇒ (xH , pos_Eq )
  end.

Definition PtoM_correct := fun x : positive ⇒ refl_equal x.
Definition ZtoM_correct := fun x : Z ⇒ refl_equal x.
Definition ZtoE_correct := fun x : Z ⇒ refl_equal x.

Definition exponent_zero_correct := refl_equal Z0.
Definition exponent_one_correct := refl_equal 1%Z.
Definition exponent_neg_correct := fun x ⇒ refl_equal (- EtoZ x)%Z.
Definition exponent_add_correct := fun x y ⇒ refl_equal (EtoZ x + EtoZ y)%Z.
Definition exponent_sub_correct := fun x y ⇒ refl_equal (EtoZ x - EtoZ y)%Z.
Definition exponent_cmp_correct := fun x y ⇒ refl_equal (EtoZ x ?= EtoZ y)%Z.

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.

Definition mantissa_zero_correct := refl_equal Z0.
Definition mantissa_pos_correct :=
  fun (x : positive) (_ : True) ⇒ refl_equal (Zpos x).
Definition mantissa_neg_correct :=
  fun (x : positive) (_ : True) ⇒ refl_equal (Zneg x).
Definition mantissa_one_correct := conj (refl_equal xH) I.
Definition mantissa_add_correct :=
  fun x y (_ _ : True) ⇒ conj (refl_equal (MtoP x + MtoP y)%positive) I.
Definition mantissa_sub_correct :=
  fun x y (_ _ : True) (_ : (MtoP y < MtoP x)%positive) ⇒ conj (refl_equal (MtoP x - MtoP y)%positive) I.
Definition mantissa_mul_correct :=
  fun x y (Hx Hy : True) ⇒ conj (refl_equal (MtoP x × MtoP y)%positive) I.
Definition mantissa_cmp_correct :=
  fun x y (Hx Hy : True) ⇒ refl_equal (Zpos (MtoP x) ?= Zpos (MtoP y))%Z.
Definition mantissa_even_correct :=
  fun x (_ : True) ⇒ refl_equal (Z.even (Zpos x)).

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_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 →
  z = Zpos x →
  MtoP (mantissa_shl y z) = shift radix (MtoP y) x ∧
  valid_mantissa (mantissa_shl y z).

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 StdZRadix2.