Digit.v

(****************************************************************************                                                                                         IEEE754  :  Digit                                                                                                                                           Laurent Thery                                                                                                                                     ***************************************************************************** Gives the number of digits necessary to write a number in a given base *)
Require Import Arith.
Require Import Compare_dec.
Require Import Faux.
Require Import sTactic.
Section Pdigit.

(* n is the base *)
Variable n:nat.

(* and it is greater or equal to 2 *)
Hypothesis nMoreThan1:(lt (S O) n).
(* Usual definition of the exponential *)

Fixpoint exp[q:nat]: nat :=
   Cases q of
       O => (S O)
      | (S q') => (mult n (exp q'))
   end.
(* Some basic properties of exponential *)

Theorem expPlus: (p, q:nat)(exp (plus p q))=(mult (exp p) (exp q)).

Theorem expLess: (q:nat)(lt O (exp q)).

Theorem expBound: (q:nat)(lt q (exp q)).

Theorem exp_monotone_lt: (p, q:nat) (lt p q) ->(lt (exp p) (exp q)).

Theorem exp_anti_monotone_lt: (p, q:nat) (lt (exp p) (exp q)) ->(lt p q).

Theorem exp_monotone_le: (p, q:nat) (le p q) ->(le (exp p) (exp q)).

Theorem exp_anti_monotone_le: (p, q:nat) (le (exp p) (exp q)) ->(le p q).

Theorem exp_anti_eq: (p, q:nat) (exp p)=(exp q) ->p=q.

Theorem exp_pred_minus1:
  (m:nat) (lt (1) n) -> ~ m=O ->(le (exp (pred m)) (minus (exp m) (1))).
(* To compute the number of digits structurally, we suppose that    we know already an upper bound q. So we start from q down    to 0 to find the bigger exponent r such that n^(r-1) < v *)

Fixpoint digitAux[v, q:nat]: nat :=
   Cases q of
       O => O
      | (S q') => Cases (le_lt_dec (exp q') v) of
                      (left _) => q
                     | (right _) => (digitAux v q')
                  end
   end.

(* As we know that q < n^(q+1) we can define our function digit *)

Definition digit := [q:nat](digitAux q (S q)).

Theorem digitAuxLess: (v, q:nat) (lt O v) ->(le (exp (pred (digitAux v q))) v).
(* digit is correct (first part) *)

Theorem digitLess: (q:nat) (lt O q) ->(le (exp (pred (digit q))) q).

Theorem digitAuxMore:
  (v, q:nat) (lt (digitAux v q) q) ->(lt v (exp (digitAux v q))).
(* digit is correct (second part) *)

Theorem digitMore: (q:nat)(lt q (exp (digit q))).
(* if we find an r such that n^(r-1) =< q < n^r    then r is the number of digits *)

Theorem digitInv:
  (q, r:nat) (le (exp (pred r)) q) -> (lt q (exp r)) ->(digit q)=r.

Theorem digitO: (digit O)=O.

Theorem digit1: (digit (1))=(1).

Theorem digit_S_monotone: (m:nat)(le (digit m) (digit (S m))).
(* digit is monotone *)

Theorem digit_monotone: (p, q:nat) (le p q) ->(le (digit p) (digit q)).
(* if the number is not null so is the number of digits *)

Theorem digitNotZero: (q:nat) (lt O q) ->(lt O (digit q)).

Theorem digitAdd:
  (q, r:nat) (lt O q) ->(digit (mult q (exp r)))=(plus (digit q) r).

Theorem digit_minus1: (p:nat)(digit (minus (exp p) (1)))=p.

Theorem digit_bound:
  (x, y, z, n:nat) (le x y) -> (le y z) -> (digit x)=n -> (digit z)=n ->
  (digit y)=n.
(* Strict comparison on the number of digits gives comparison on the numbers *)

Theorem digit_anti_monotone_lt:
  (lt (1) n) ->(p, q:nat) (lt (digit p) (digit q)) ->(lt p q).
End Pdigit.

30/05/01, 17:29