(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** * Functions for computing the number of digits of integers and related theorems. *)

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_digits.

Section Fcalc_digits.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Theorem Zdigits_ln_beta :
  forall n,
  n <> Z0 ->
  Zdigits beta n = ln_beta beta (Z2R n).
Proof.
(* Goal: forall (n : Z) (_ : not (@eq Z n Z0)), @eq Z (Zdigits beta n) (ln_beta_val beta (Z2R n) (ln_beta beta (Z2R n))) *)
intros n Hn.
(* Goal: @eq Z (Zdigits beta n) (ln_beta_val beta (Z2R n) (ln_beta beta (Z2R n))) *)
destruct (ln_beta beta (Z2R n)) as (e, He) ; simpl.
(* Goal: @eq Z (Zdigits beta n) e *)
specialize (He (Z2R_neq _ _ Hn)).
(* Goal: @eq Z (Zdigits beta n) e *)
rewrite <- Z2R_abs in He.
(* Goal: @eq Z (Zdigits beta n) e *)
assert (Hd := Zdigits_correct beta n).
(* Goal: @eq Z (Zdigits beta n) e *)
assert (Hd' := Zdigits_gt_0 beta n).
(* Goal: @eq Z (Zdigits beta n) e *)
apply Zle_antisym ; apply (bpow_lt_bpow beta).
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub (Zdigits beta n) (Zpos xH))) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Zdigits beta n)) *)
apply Rle_lt_trans with (2 := proj2 He).
(* Goal: Rlt (Z2R (Z.abs n)) (Fcore_Raux.bpow beta (Zdigits beta n)) *)
rewrite <- Z2R_Zpower by omega.
(* Goal: Rle (Z2R (Z.pow (radix_val beta) (Z.sub (Zdigits beta n) (Zpos xH)))) (Z2R (Z.abs n)) *)
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Zdigits beta n)) *)
now apply Z2R_le.
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub e (Zpos xH))) (Fcore_Raux.bpow beta (Zdigits beta n)) *)
apply Rle_lt_trans with (1 := proj1 He).
(* Goal: Rlt (Z2R (Z.abs n)) (Fcore_Raux.bpow beta (Zdigits beta n)) *)
rewrite <- Z2R_Zpower by omega.
(* Goal: Rlt (Z2R (Z.abs n)) (Z2R (Z.pow (radix_val beta) (Zdigits beta n))) *)
now apply Z2R_lt.
Qed.

Theorem ln_beta_F2R_Zdigits :
  forall m e, m <> Z0 ->
  (ln_beta beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (Zdigits beta m) e) *)
intros m e Hm.
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (Zdigits beta m) e) *)
rewrite ln_beta_F2R with (1 := Hm).
(* Goal: @eq Z (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) (Z.add (Zdigits beta m) e) *)
apply (f_equal (fun v => Zplus v e)).
(* Goal: @eq Z (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) (Zdigits beta m) *)
apply sym_eq.
(* Goal: @eq Z (Zdigits beta m) (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) *)
now apply Zdigits_ln_beta.
Qed.

End Fcalc_digits.
