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).
Require Import Arith.
(* 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)).
Intros p; Elim p; Simpl; Auto with arith.
Intros n0 H' q; Rewrite mult_assoc_r; Rewrite <- H'; Auto.
Qed.

Theorem expLess: (q:nat)(lt O (exp q)).
Intros q; Elim q; Simpl; Auto with arith.
Generalize nMoreThan1; Case n; Simpl; Auto with arith.
Qed.
Hints Resolve expLess :arith.

Theorem expBound: (q:nat)(lt q (exp q)).
Intros q; Elim q; Simpl; Auto with arith.
Intros n0 H'; Apply le_lt_trans with m := (plus (exp n0) n0); Auto with arith.
Apply lt_le_trans with m := (plus (exp n0) (exp n0)); Auto with arith.
Generalize nMoreThan1; Case n; Simpl; Auto with arith.
Intros H'0; Inversion H'0.
Intros n1; Case n1; Simpl; Auto with arith.
Intros H'0; Inversion H'0.
Inversion H0.
Qed.
Hints Resolve expBound :arith.

Theorem exp_monotone_lt: (p, q:nat) (lt p q) ->(lt (exp p) (exp q)).
Intros p q H'; Elim H'; Simpl; Auto.
Generalize nMoreThan1; Case n; Simpl; Auto with arith.
Intros H'1; Inversion H'1.
Intros n0; Case n0; Simpl; Auto with arith.
Intros H'1; Inversion H'1.
Inversion H0.
Intros n1 H'0; Generalize (expLess p); Case (exp p); Auto with arith.
Intros n2 H'1; Pattern 1 (S n2); Replace (S n2) with (plus (S n2) O);
Auto with arith.
Intros m H'0; Generalize nMoreThan1; Case n; Simpl; Auto with arith.
Intros H'1; Inversion H'1.
Qed.
Hints Resolve exp_monotone_lt :arith.

Theorem exp_anti_monotone_lt: (p, q:nat) (lt (exp p) (exp q)) ->(lt p q).
Intros p q H'.
Case (le_or_lt q p); Auto; (Intros H'1; Generalize H'; Case H'1).
Intros H'0; Contradict H'0; Auto with arith.
Intros m H'0 H'2; Contradict H'2; Auto with arith.
Apply lt_not_sym; Auto with arith.
Qed.

Theorem exp_monotone_le: (p, q:nat) (le p q) ->(le (exp p) (exp q)).
Intros p q H'; Case (le_lt_or_eq ? ? H'); Auto with arith.
Intros H'0.
Apply lt_le_weak.
Apply exp_monotone_lt; Auto.
Intros H'0; Rewrite H'0; Auto.
Qed.

Theorem exp_anti_monotone_le: (p, q:nat) (le (exp p) (exp q)) ->(le p q).
Intros p q H'; Case (le_or_lt p q); Intros H'0; Auto with arith.
Contradict H'; Auto with arith.
Qed.

Theorem exp_anti_eq: (p, q:nat) (exp p)=(exp q) ->p=q.
Intros p q H'; Apply le_antisym; Apply exp_anti_monotone_le; Rewrite H'; Auto.
Qed.

Theorem exp_pred_minus1:
  (m:nat) (lt (1) n) -> ~ m=O ->(le (exp (pred m)) (minus (exp m) (1))).
Intros m; Case m; Simpl.
Intros H' H'0; Contradict H'0; Auto with arith.
Intros n0 H' H'0.
Apply simpl_le_plus_l with p := (1); Auto.
Rewrite le_plus_minus_r; Auto.
2:Replace (1) with (mult (1) (1)); Auto with arith.
Replace (mult n (exp n0)) with (plus (mult (pred n) (exp n0)) (exp n0)).
Apply le_reg_r; Replace (1) with (mult (1) (1)); Auto with arith.
Generalize H'; Case n; Simpl.
Intros H'1; Inversion H'1.
Intros n1 H'1; Apply plus_sym; Auto.
Qed.
(* 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)).
Hints Unfold digit.

Theorem digitAuxLess: (v, q:nat) (lt O v) ->(le (exp (pred (digitAux v q))) v).
Intros v q; Elim q; Simpl; Auto.
Intros q1 H' H'0; Case (le_lt_dec (exp q1) v); Auto.
Qed.
(* digit is correct (first part) *)

Theorem digitLess: (q:nat) (lt O q) ->(le (exp (pred (digit q))) q).
Intros q H'; Unfold digit; Apply digitAuxLess; Auto.
Qed.
Hints Resolve digitLess :arith.

Theorem digitAuxMore:
  (v, q:nat) (lt (digitAux v q) q) ->(lt v (exp (digitAux v q))).
Intros v q; Elim q; Simpl.
Intros H; Inversion H.
Intros q1 H'; Case (le_lt_dec (exp q1) v); Simpl; Auto with arith.
Intros H'0 H'1; Contradict H'1; Auto with arith.
Intros H'0 H'1; Case (le_lt_or_eq ? ? H'1); Intros H'2; Auto with arith.
Replace (digitAux v q1) with q1; Auto.
Inversion H'2; Auto.
Qed.
(* digit is correct (second part) *)

Theorem digitMore: (q:nat)(lt q (exp (digit q))).
Intros q; Case q.
Simpl; Auto with arith.
Intros q'; Unfold digit; Apply digitAuxMore; Auto with arith.
CaseEq (digitAux (S q') (S (S q'))); Auto with arith.
Intros n0 H'.
Apply lt_n_S.
Replace n0 with (pred (digitAux (S q') (S (S q')))).
Apply exp_anti_monotone_lt; Auto with arith.
Apply le_lt_trans with m := (S q'); Auto with arith.
Apply digitAuxLess; Auto with arith.
Rewrite H'; Auto.
Qed.
Hints Resolve digitMore :arith.
(* 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.
Intros q r H' H'0; Case (le_or_lt (digit q) r).
Intros H'1; Case (le_lt_or_eq ? ? H'1); Auto; Intros H'2.
Absurd (lt q (exp (digit q))); Auto with arith.
Apply le_not_lt; Auto with arith.
Apply le_trans with m := (exp (pred r)); Auto with arith.
Apply exp_monotone_le.
Generalize H'2; Case r; Auto with arith.
Intros H'1.
Absurd (le (exp (pred (digit q))) q); Auto with arith.
Apply lt_not_le; Auto with arith.
Apply lt_le_trans with m := (exp r); Auto.
Apply exp_monotone_le.
Generalize H'1; Case (digit q); Auto with arith.
Apply digitLess; Auto.
Generalize H'1; Case q; Unfold digit; Simpl; Auto with arith.
Case (le_lt_dec (1) O); Auto with arith.
Intros H'2 H'3; Inversion H'3.
Qed.

Theorem digitO: (digit O)=O.
Unfold digit; Simpl.
Case (le_lt_dec (1) O); Auto with arith.
Qed.

Theorem digit1: (digit (1))=(1).
Unfold digit; Simpl.
Case (le_lt_dec (mult n (1)) (1)); Auto with arith.
Intros H'; Contradict H'; Auto with arith.
Apply lt_not_le; Auto with arith.
Rewrite mult_sym; Simpl; Auto with arith.
Case (le_lt_dec (1) (1)); Auto with arith.
Intros H'; Contradict H'; Auto with arith.
Qed.

Theorem digit_S_monotone: (m:nat)(le (digit m) (digit (S m))).
Intros m.
Case (le_lt_or_eq (S m) (exp (digit m))); Auto with arith.
Intros H'.
Rewrite (digitInv (S m) (digit m)); Auto with arith.
Case m; Simpl; Auto with arith.
Rewrite digitO; Simpl; Auto with arith.
Intros H'.
Rewrite (digitInv (S m) (S (digit m))); Auto with arith.
Rewrite H'; Auto.
Rewrite H'; Auto with arith.
Qed.
(* digit is monotone *)

Theorem digit_monotone: (p, q:nat) (le p q) ->(le (digit p) (digit q)).
Intros p q H'0; Elim H'0; Auto.
Intros m H'1 H'2.
Apply le_trans with m := (digit m); Auto.
Apply digit_S_monotone; Auto.
Qed.
Hints Resolve digit_monotone :arith.
(* if the number is not null so is the number of digits *)

Theorem digitNotZero: (q:nat) (lt O q) ->(lt O (digit q)).
Intros q H'.
Apply lt_le_trans with m := (digit (1)); Auto with arith.
Rewrite digit1; Auto with arith.
Qed.

Theorem digitAdd:
  (q, r:nat) (lt O q) ->(digit (mult q (exp r)))=(plus (digit q) r).
Intros q r H0.
Apply digitInv; Auto with arith.
Replace (pred (plus (digit q) r)) with (plus (pred (digit q)) r);
Auto with arith.
Rewrite expPlus; Auto with arith.
Generalize (digitNotZero ? H0); Case (digit q); Auto with arith.
Intros H'; Inversion H'.
Rewrite expPlus; Auto with arith.
Qed.

Theorem digit_minus1: (p:nat)(digit (minus (exp p) (1)))=p.
Intros p; Case p; Auto.
Simpl; Rewrite digitO; Auto.
Intros n0; Apply digitInv; Auto.
Apply lt_n_Sm_le; Auto.
Rewrite minus_Sn_m; Auto with arith.
Replace (minus (S (exp (S n0))) (1)) with (exp (S n0)).
Apply exp_monotone_lt; Auto.
Simpl; Auto with arith.
Generalize (expLess (S n0)); Case (exp (S n0)); Auto with arith.
Qed.

Theorem digit_bound:
  (x, y, z, n:nat) (le x y) -> (le y z) -> (digit x)=n -> (digit z)=n ->
  (digit y)=n.
Intros x y z n0 H' H'0 H'1 H'2; Apply le_antisym.
Rewrite <- H'2; Auto with arith.
Rewrite <- H'1; Auto with arith.
Qed.
(* 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).
Intros H' p q H'0.
Case (le_or_lt q p); Auto; Intros H'1.
Contradict H'0.
Case (le_lt_or_eq ? ? H'1); Intros H'2.
Apply le_not_lt; Auto with arith.
Rewrite <- H'2; Auto with arith.
Qed.
End Pdigit.
Hints Resolve expLess :arith.
Hints Resolve expBound :arith.
Hints Resolve exp_monotone_lt :arith.
Hints Resolve exp_monotone_le :arith.
Hints Resolve exp_pred_minus1 :arith.
Hints Unfold digit.
Hints Resolve digitLess :arith.
Hints Resolve digitMore :arith.
Hints Resolve digit_monotone :arith.

22/10/100, 19:38