(****************************************************************************
                                                                             
          IEEE754  :  Digit                                                  
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  Gives the number of digits necessary to write a number in a given base *)
Require Export ZArithRing.
Require Export Omega.
Require Export Faux.
Section Pdigit.
(* n is the base *)
Variable n : Z.
(* and it is greater or equal to 2 *)
Hypothesis nMoreThan1 : (1 < n)%Z.
 
Let nMoreThanOne := Zlt_1_O _ (Zlt_le_weak _ _ nMoreThan1).
Hint Resolve nMoreThanOne: zarith.
 
Theorem Zpower_nat_less : forall q : nat, (0 < Zpower_nat n q)%Z.
intros q; elim q; simpl in |- *;
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
auto with zarith.
Qed.
Hint Resolve Zpower_nat_less: zarith.
 
Theorem Zpower_nat_monotone_S :
 forall p : nat, (Zpower_nat n p < Zpower_nat n (S p))%Z.
intros p; rewrite <- (Zmult_1_l (Zpower_nat n p)); replace (S p) with (1 + p);
 [ rewrite Zpower_nat_is_exp | auto with zarith ].
(* Goal: Z.lt (Z.mul (Zpos xH) (Zpower_nat n p)) (Z.mul (Zpower_nat n (S O)) (Zpower_nat n p)) *)
rewrite Zpower_nat_1; auto with zarith.
(* Goal: Z.lt (Z.mul (Zpos xH) (Zpower_nat n p)) (Z.mul n (Zpower_nat n p)) *)
apply Zmult_gt_0_lt_compat_r; auto with zarith.
(* Goal: Z.gt (Zpower_nat n p) Z0 *)
apply Zlt_gt; auto with zarith.
Qed.
 
Theorem Zpower_nat_monotone_lt :
 forall p q : nat, p < q -> (Zpower_nat n p < Zpower_nat n q)%Z.
(* Goal: forall (p q : nat) (_ : lt p q), Z.lt (Zpower_nat n p) (Zpower_nat n q) *)
intros p q H'; elim H'; simpl in |- *; auto.
(* Goal: Z.lt (Zpower_nat n m) (Z.mul n (Zpower_nat n m)) *)
apply Zpower_nat_monotone_S.
(* Goal: forall (m : nat) (_ : le (S p) m) (_ : Z.lt (Zpower_nat n p) (Zpower_nat n m)), Z.lt (Zpower_nat n p) (Z.mul n (Zpower_nat n m)) *)
intros m H H0; apply Zlt_trans with (1 := H0).
(* Goal: Z.lt (Zpower_nat n m) (Z.mul n (Zpower_nat n m)) *)
apply Zpower_nat_monotone_S.
Qed.
Hint Resolve Zpower_nat_monotone_lt: zarith.
 
Theorem Zpower_nat_anti_monotone_lt :
 forall p q : nat, (Zpower_nat n p < Zpower_nat n q)%Z -> p < q.
(* Goal: forall (p q : nat) (_ : Z.lt (Zpower_nat n p) (Zpower_nat n q)), lt p q *)
intros p q H'.
(* Goal: lt p q *)
case (le_or_lt q p); auto; (intros H'1; generalize H'; case H'1).
(* Goal: forall _ : Z.lt (Zpower_nat n q) (Zpower_nat n q), lt q q *)
(* Goal: forall (m : nat) (_ : le q m) (_ : Z.lt (Zpower_nat n (S m)) (Zpower_nat n q)), lt (S m) q *)
intros H'0; Contradict H'0; auto with zarith.
(* Goal: forall (m : nat) (_ : le q m) (_ : Z.lt (Zpower_nat n (S m)) (Zpower_nat n q)), lt (S m) q *)
intros m H'0 H'2; Contradict H'2; auto with zarith.
Qed.
 
Theorem Zpower_nat_monotone_le :
 forall p q : nat, p <= q -> (Zpower_nat n p <= Zpower_nat n q)%Z.
(* Goal: forall (p q : nat) (_ : le p q), Z.le (Zpower_nat n p) (Zpower_nat n q) *)
intros p q H'; case (le_lt_or_eq _ _ H'); auto with zarith.
(* Goal: forall _ : @eq nat p q, Z.le (Zpower_nat n p) (Zpower_nat n q) *)
intros H1; rewrite H1; auto with zarith.
Qed.
 
Theorem Zpower_nat_anti_monotone_le :
 forall p q : nat, (Zpower_nat n p <= Zpower_nat n q)%Z -> p <= q.
(* Goal: forall (p q : nat) (_ : Z.le (Zpower_nat n p) (Zpower_nat n q)), le p q *)
intros p q H'; case (le_or_lt p q); intros H'0; auto with arith.
(* Goal: le p q *)
Contradict H'; auto with zarith.
Qed.
 
Theorem Zpower_nat_anti_eq :
 forall p q : nat, Zpower_nat n p = Zpower_nat n q -> p = q.
intros p q H'; apply le_antisym; apply Zpower_nat_anti_monotone_le;
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
 rewrite H'; auto with zarith.
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 r : Z) (q : positive) {struct q} : nat :=
  match q with
  | xH => 0
  | xI q' =>
      match (n * r)%Z with
      | r' =>
          match (r ?= v)%Z with
          | Datatypes.Gt => 0
          | _ => S (digitAux v r' q')
          end
      end
  | xO q' =>
      match (n * r)%Z with
      | r' =>
          match (r ?= v)%Z with
          | Datatypes.Gt => 0
          | _ => S (digitAux v r' q')
          end
      end
  end.
(* As we know that log_n q < log_2 q we can define our function digit*)
 
Definition digit (q : Z) :=
  match q with
  | Z0 => 0
  | Zpos q' => digitAux (Zabs q) 1 (xO q')
  | Zneg q' => digitAux (Zabs q) 1 (xO q')
  end.
Hint Unfold digit.
 
Theorem digitAux1 :
 forall p r, (Zpower_nat n (S p) * r)%Z = (Zpower_nat n p * (n * r))%Z.
intros p r; replace (S p) with (1 + p);
 [ rewrite Zpower_nat_is_exp | auto with arith ].
(* Goal: @eq Z (Z.mul (Z.mul (Zpower_nat n (S O)) (Zpower_nat n p)) r) (Z.mul (Zpower_nat n p) (Z.mul n r)) *)
rewrite Zpower_nat_1; ring.
Qed.
 
Theorem Zcompare_correct :
 forall p q : Z,
 match (p ?= q)%Z with
 | Datatypes.Gt => (q < p)%Z
 | Datatypes.Lt => (p < q)%Z
 | Datatypes.Eq => p = q
 end.
intros p q; unfold Zlt in |- *; generalize (Zcompare_EGAL p q);
 (CaseEq (p ?= q)%Z; simpl in |- *; auto).
(* Goal: forall (_ : @eq comparison (Z.compare p q) Gt) (_ : forall _ : @eq comparison Gt Eq, @eq Z p q), @eq comparison (Z.compare q p) Lt *)
intros H H0; case (Zcompare_Gt_Lt_antisym p q); auto.
Qed.
 
Theorem digitAuxLess :
 forall (v r : Z) (q : positive),
 match digitAux v r q with
 | S r' => (Zpower_nat n r' * r <= v)%Z
 | O => True
 end.
(* Goal: forall (v r : Z) (q : positive), match digitAux v r q with | O => True | S r' => Z.le (Z.mul (Zpower_nat n r') r) v end *)
intros v r q; generalize r; elim q; clear r q; simpl in |- *; auto.
(* Goal: forall (p : positive) (_ : forall r : Z, match digitAux v r p with | O => True | S r' => Z.le (Z.mul (Zpower_nat n r') r) v end) (r : Z), match match Z.compare r v with | Eq => S (digitAux v (Z.mul n r) p) | Lt => S (digitAux v (Z.mul n r) p) | Gt => O end with | O => True | S r' => Z.le (Z.mul (Zpower_nat n r') r) v end *)
intros q' Rec r; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto.
(* Goal: forall _ : Z.lt r v, Z.le (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) q')) r) v *)
intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q').
(* Goal: forall _ : True, Z.le (Z.mul (Zpower_nat n O) r) v *)
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
(* Goal: forall _ : Z.lt r v, Z.le (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) q')) r) v *)
intros; rewrite H1; rewrite Zpower_nat_O; auto with zarith.
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
intros r'; rewrite digitAux1; auto.
(* Goal: forall _ : Z.lt r v, Z.le (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) q')) r) v *)
intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q').
(* Goal: forall _ : True, Z.le (Z.mul (Zpower_nat n O) r) v *)
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
intros; rewrite Zpower_nat_O; auto with zarith.
(* Goal: Z.le (Z.mul (Z.of_nat (S O)) r) v *)
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
apply Zle_trans with (m := r); auto with zarith.
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
intros r'; rewrite digitAux1; auto.
(* Goal: forall (p : positive) (_ : forall r : Z, match digitAux v r p with | O => True | S r' => Z.le (Z.mul (Zpower_nat n r') r) v end) (r : Z), match match Z.compare r v with | Eq => S (digitAux v (Z.mul n r) p) | Lt => S (digitAux v (Z.mul n r) p) | Gt => O end with | O => True | S r' => Z.le (Z.mul (Zpower_nat n r') r) v end *)
intros q' Rec r; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto.
(* Goal: forall _ : Z.lt r v, Z.le (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) q')) r) v *)
intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q').
(* Goal: forall _ : True, Z.le (Z.mul (Zpower_nat n O) r) v *)
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
(* Goal: forall _ : Z.lt r v, Z.le (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) q')) r) v *)
intros; rewrite H1; rewrite Zpower_nat_O; auto with zarith.
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
intros r'; rewrite digitAux1; auto.
(* Goal: forall _ : Z.lt r v, Z.le (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) q')) r) v *)
intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q').
(* Goal: forall _ : True, Z.le (Z.mul (Zpower_nat n O) r) v *)
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
intros; rewrite Zpower_nat_O; auto with zarith.
(* Goal: Z.le (Z.mul (Z.of_nat (S O)) r) v *)
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
apply Zle_trans with (m := r); auto with zarith.
(* Goal: forall (n0 : nat) (_ : Z.le (Z.mul (Zpower_nat n n0) (Z.mul n r)) v), Z.le (Z.mul (Zpower_nat n (S n0)) r) v *)
intros r'; rewrite digitAux1; auto.
Qed.
(* digit is correct (first part) *)
 
Theorem digitLess :
 forall q : Z, q <> 0%Z -> (Zpower_nat n (pred (digit q)) <= Zabs q)%Z.
(* Goal: forall q : Z, Z.lt (Z.abs q) (Zpower_nat n (digit q)) *)
intros q; case q.
(* Goal: forall _ : not (@eq Z Z0 Z0), Z.le (Zpower_nat n (Init.Nat.pred (digit Z0))) (Z.abs Z0) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zpos p) Z0)), Z.le (Zpower_nat n (Init.Nat.pred (digit (Zpos p)))) (Z.abs (Zpos p)) *)
(* Goal: forall (p : positive) (_ : not (@eq Z (Zneg p) Z0)), Z.le (Zpower_nat n (Init.Nat.pred (digit (Zneg p)))) (Z.abs (Zneg p)) *)
intros H; Contradict H; auto with zarith.
intros p H; unfold digit in |- *;
 generalize (digitAuxLess (Zabs (Zpos p)) 1 (xO p));
 case (digitAux (Zabs (Zpos p)) 1 (xO p)); simpl in |- *; 
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
 auto with zarith.
intros p H; unfold digit in |- *;
 generalize (digitAuxLess (Zabs (Zneg p)) 1 (xO p));
 case (digitAux (Zabs (Zneg p)) 1 (xO p)); simpl in |- *; 
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
 auto with zarith.
Qed.
Hint Resolve digitLess: zarith.
Hint Resolve Zmult_gt_0_lt_compat_r Zmult_gt_0_lt_compat_l: zarith.
 
Fixpoint pos_length (p : positive) : nat :=
  match p with
  | xH => 0
  | xO p' => S (pos_length p')
  | xI p' => S (pos_length p')
  end.
 
Theorem digitAuxMore :
 forall (v r : Z) (q : positive),
 (0 < r)%Z ->
 (v < Zpower_nat n (pos_length q) * r)%Z ->
 (v < Zpower_nat n (digitAux v r q) * r)%Z.
(* Goal: forall (v r : Z) (q : positive) (_ : Z.lt Z0 r) (_ : Z.lt v (Z.mul (Zpower_nat n (pos_length q)) r)), Z.lt v (Z.mul (Zpower_nat n (digitAux v r q)) r) *)
intros v r q; generalize r; elim q; clear r q; simpl in |- *.
(* Goal: forall (p : positive) (_ : forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v (Z.mul (Zpower_nat n (pos_length p)) r)), Z.lt v (Z.mul (Zpower_nat n (digitAux v r p)) r)) (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n match Z.compare r v with | Eq => S (digitAux v (Z.mul n r) p) | Lt => S (digitAux v (Z.mul n r) p) | Gt => O end) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros p Rec r Hr; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto.
(* Goal: forall (_ : @eq Z r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros H1 H2; rewrite <- H1.
(* Goal: Z.lt r (Z.mul (Zpower_nat n (S (digitAux r (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
apply Zle_lt_trans with (Zpower_nat n 0 * r)%Z; auto with zarith arith.
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith.
(* Goal: forall (_ : Z.lt r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros H1 H2; rewrite digitAux1.
(* Goal: Z.lt v (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) p)) (Z.mul n r)) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
apply Rec.
(* Goal: Z.lt Z0 (Z.mul n r) *)
(* Goal: Z.lt v (Z.mul (Zpower_nat n (pos_length p)) (Z.mul n r)) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
apply Zlt_mult_ZERO; auto with zarith.
(* Goal: Z.lt v (Z.mul (Zpower_nat n (pos_length p)) (Z.mul n r)) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
rewrite <- digitAux1; auto.
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith.
(* Goal: forall (p : positive) (_ : forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v (Z.mul (Zpower_nat n (pos_length p)) r)), Z.lt v (Z.mul (Zpower_nat n (digitAux v r p)) r)) (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n match Z.compare r v with | Eq => S (digitAux v (Z.mul n r) p) | Lt => S (digitAux v (Z.mul n r) p) | Gt => O end) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros p Rec r Hr; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto.
(* Goal: forall (_ : @eq Z r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros H1 H2; rewrite <- H1.
(* Goal: Z.lt r (Z.mul (Zpower_nat n (S (digitAux r (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
apply Zle_lt_trans with (Zpower_nat n 0 * r)%Z; auto with zarith arith.
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith.
(* Goal: forall (_ : Z.lt r v) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n (S (digitAux v (Z.mul n r) p))) r) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros H1 H2; rewrite digitAux1.
(* Goal: Z.lt v (Z.mul (Zpower_nat n (digitAux v (Z.mul n r) p)) (Z.mul n r)) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
apply Rec.
(* Goal: Z.lt Z0 (Z.mul n r) *)
(* Goal: Z.lt v (Z.mul (Zpower_nat n (pos_length p)) (Z.mul n r)) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
apply Zlt_mult_ZERO; auto with zarith.
(* Goal: Z.lt v (Z.mul (Zpower_nat n (pos_length p)) (Z.mul n r)) *)
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
rewrite <- digitAux1; auto.
(* Goal: forall (_ : Z.lt v r) (_ : Z.lt v (Z.mul (Z.mul n (Zpower_nat n (pos_length p))) r)), Z.lt v (Z.mul (Zpower_nat n O) r) *)
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith.
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
auto.
Qed.
 
Theorem pos_length_pow :
 forall p : positive, (Zpos p < Zpower_nat n (S (pos_length p)))%Z.
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros p; elim p; simpl in |- *; auto.
(* Goal: forall (p : positive) (_ : Z.lt (Zpos p) (Z.mul n (Zpower_nat n (pos_length p)))), Z.lt (Zpos (xI p)) (Z.mul n (Z.mul n (Zpower_nat n (pos_length p)))) *)
(* Goal: forall (p : positive) (_ : Z.lt (Zpos p) (Z.mul n (Zpower_nat n (pos_length p)))), Z.lt (Zpos (xO p)) (Z.mul n (Z.mul n (Zpower_nat n (pos_length p)))) *)
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
intros p0 H; rewrite Zpos_xI.
apply Zlt_le_trans with (2 * (n * Zpower_nat n (pos_length p0)))%Z;
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
auto with zarith.
(* Goal: forall (p : positive) (_ : Z.lt (Zpos p) (Z.mul n (Zpower_nat n (pos_length p)))), Z.lt (Zpos (xO p)) (Z.mul n (Z.mul n (Zpower_nat n (pos_length p)))) *)
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
intros p0 H; rewrite Zpos_xO.
apply Zlt_le_trans with (2 * (n * Zpower_nat n (pos_length p0)))%Z;
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
auto with zarith.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
auto with zarith.
Qed.
(* digit is correct (second part) *)
 
Theorem digitMore : forall q : Z, (Zabs q < Zpower_nat n (digit q))%Z.
(* Goal: forall q : Z, Z.lt (Z.abs q) (Zpower_nat n (digit q)) *)
intros q; case q.
(* Goal: Z.lt (Z.abs Z0) (Zpower_nat n (digit Z0)) *)
(* Goal: forall p : positive, Z.lt (Z.abs (Zpos p)) (Zpower_nat n (digit (Zpos p))) *)
(* Goal: forall p : positive, Z.lt (Z.abs (Zneg p)) (Zpower_nat n (digit (Zneg p))) *)
easy.
(* Goal: forall p : positive, Z.lt (Z.abs (Zpos p)) (Zpower_nat n (digit (Zpos p))) *)
(* Goal: forall p : positive, Z.lt (Z.abs (Zneg p)) (Zpower_nat n (digit (Zneg p))) *)
intros q'; rewrite <- (Zmult_1_r (Zpower_nat n (digit (Zpos q')))).
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
unfold digit in |- *; apply digitAuxMore; auto with zarith.
(* Goal: Z.lt (Z.abs (Zneg q')) (Z.mul (Zpower_nat n (pos_length (xO q'))) (Zpos xH)) *)
rewrite Zmult_1_r.
(* Goal: Z.lt (Z.abs (Zneg q')) (Zpower_nat n (pos_length (xO q'))) *)
simpl in |- *; apply pos_length_pow.
(* Goal: forall p : positive, Z.lt (Z.abs (Zneg p)) (Zpower_nat n (digit (Zneg p))) *)
intros q'; rewrite <- (Zmult_1_r (Zpower_nat n (digit (Zneg q')))).
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
unfold digit in |- *; apply digitAuxMore; auto with zarith.
(* Goal: Z.lt (Z.abs (Zneg q')) (Z.mul (Zpower_nat n (pos_length (xO q'))) (Zpos xH)) *)
rewrite Zmult_1_r.
(* Goal: Z.lt (Z.abs (Zneg q')) (Zpower_nat n (pos_length (xO q'))) *)
simpl in |- *; apply pos_length_pow.
Qed.
Hint Resolve digitMore: zarith.
(* if we find an r such that n^(r-1) =< q < n^r 
   then r is the number of digits *)
 
Theorem digitInv :
 forall (q : Z) (r : nat),
 (Zpower_nat n (pred r) <= Zabs q)%Z ->
 (Zabs q < Zpower_nat n r)%Z -> digit q = r.
(* Goal: forall (q : Z) (r : nat) (_ : Z.le (Zpower_nat n (Init.Nat.pred r)) (Z.abs q)) (_ : Z.lt (Z.abs q) (Zpower_nat n r)), @eq nat (digit q) r *)
intros q r H' H'0; case (le_or_lt (digit q) r).
(* Goal: forall _ : le (digit q) r, @eq nat (digit q) r *)
(* Goal: forall _ : lt r (digit q), @eq nat (digit q) r *)
intros H'1; case (le_lt_or_eq _ _ H'1); auto; intros H'2.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
absurd (Zabs q < Zpower_nat n (digit q))%Z; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
apply Zle_not_lt; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
apply Zle_trans with (m := Zpower_nat n (pred r)); auto with zarith.
(* Goal: Z.le (Zpower_nat n r) (Zpower_nat n (Init.Nat.pred (digit q))) *)
(* Goal: Z.le (Zpower_nat n (Init.Nat.pred (digit q))) (Z.abs q) *)
apply Zpower_nat_monotone_le.
(* Goal: le (digit q) (Init.Nat.pred r) *)
(* Goal: forall _ : lt r (digit q), @eq nat (digit q) r *)
generalize H'2; case r; auto with arith.
(* Goal: forall _ : lt r (digit q), @eq nat (digit q) r *)
intros H'1.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
absurd (Zpower_nat n (pred (digit q)) <= Zabs q)%Z; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
apply Zlt_not_le; auto with zarith.
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
apply Zlt_le_trans with (m := Zpower_nat n r); auto.
(* Goal: Z.le (Zpower_nat n r) (Zpower_nat n (Init.Nat.pred (digit q))) *)
(* Goal: Z.le (Zpower_nat n (Init.Nat.pred (digit q))) (Z.abs q) *)
apply Zpower_nat_monotone_le.
(* Goal: le r (Init.Nat.pred (digit q)) *)
(* Goal: Z.le (Zpower_nat n (Init.Nat.pred (digit q))) (Z.abs q) *)
generalize H'1; case (digit q); auto with arith.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
apply digitLess; auto with zarith.
generalize H'1; case q; unfold digit in |- *; intros tmp; intros; red in |- *;
 intros; try discriminate; Contradict tmp; auto with arith.
Qed.
 
Theorem digitO : digit 0 = 0.
(* Goal: @eq nat (digit Z0) O *)
unfold digit in |- *; simpl in |- *; auto with arith.
Qed.
 
Theorem digit1 : digit 1 = 1.
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
unfold digit in |- *; simpl in |- *; auto.
Qed.
(* digit is monotone *)
 
Theorem digit_monotone :
 forall p q : Z, (Zabs p <= Zabs q)%Z -> digit p <= digit q.
intros p q H; case (le_or_lt (digit p) (digit q)); auto; intros H1;
 Contradict H.
(* Goal: not (Z.le (Z.abs p) (Z.abs q)) *)
apply Zlt_not_le.
(* Goal: Z.lt (Z.abs q) (Z.abs p) *)
cut (p <> 0%Z); [ intros H2 | idtac ].
(* Goal: Z.lt (Z.abs q) (Z.abs p) *)
(* Goal: not (@eq Z p Z0) *)
apply Zlt_le_trans with (2 := digitLess p H2).
(* Goal: Z.lt (Z.abs q) (Zpower_nat n (Init.Nat.pred (digit p))) *)
(* Goal: not (@eq Z p Z0) *)
cut (digit q <= pred (digit p)); [ intros H3 | idtac ].
apply Zlt_le_trans with (2 := Zpower_nat_monotone_le _ _ H3);
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
 auto with zarith.
(* Goal: le (digit q) (Init.Nat.pred (digit p)) *)
(* Goal: not (@eq Z p Z0) *)
generalize H1; case (digit p); simpl in |- *; auto with arith.
generalize H1; case p; simpl in |- *; intros tmp; intros; red in |- *; intros;
 try discriminate; Contradict tmp; auto with arith.
Qed.
Hint Resolve digit_monotone: arith.
(* if the number is not null so is the number of digits *)
 
Theorem digitNotZero : forall q : Z, q <> 0%Z -> 0 < digit q.
(* Goal: forall (q : Z) (_ : not (@eq Z q Z0)), lt O (digit q) *)
intros q H'.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
apply lt_le_trans with (m := digit 1); auto with zarith.
(* Goal: le (digit (Zpos xH)) (digit q) *)
apply digit_monotone.
generalize H'; case q; simpl in |- *; auto with zarith; intros q'; case q';
 simpl in |- *; auto with zarith arith; intros; red in |- *; 
 simpl in |- *; red in |- *; intros; discriminate.
Qed.
Hint Resolve Zlt_gt: zarith.
 
Theorem digitAdd :
 forall (q : Z) (r : nat),
 q <> 0%Z -> digit (q * Zpower_nat n r) = digit q + r.
(* Goal: forall (q : Z) (r : nat) (_ : not (@eq Z q Z0)), @eq nat (digit (Z.mul q (Zpower_nat n r))) (Init.Nat.add (digit q) r) *)
intros q r H0.
(* Goal: @eq nat (digit (Z.mul q (Zpower_nat n r))) (Init.Nat.add (digit q) r) *)
apply digitInv.
(* Goal: Z.le (Zpower_nat n (Init.Nat.pred (Init.Nat.add (digit q) r))) (Z.abs (Z.mul q (Zpower_nat n r))) *)
(* Goal: Z.lt (Z.abs (Z.mul q (Zpower_nat n r))) (Zpower_nat n (Init.Nat.add (digit q) r)) *)
replace (pred (digit q + r)) with (pred (digit q) + r).
rewrite Zpower_nat_is_exp; rewrite Zabs_Zmult;
 rewrite (fun x => Zabs_eq (Zpower_nat n x)); auto with zarith arith.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.pred (digit q)) r) (Init.Nat.pred (Init.Nat.add (digit q) r)) *)
(* Goal: Z.lt (Z.abs (Z.mul q (Zpower_nat n r))) (Zpower_nat n (Init.Nat.add (digit q) r)) *)
generalize (digitNotZero _ H0); case (digit q); auto with arith.
(* Goal: forall _ : lt O O, @eq nat (Init.Nat.add (Init.Nat.pred O) r) (Init.Nat.pred (Init.Nat.add O r)) *)
(* Goal: Z.lt (Z.abs (Z.mul q (Zpower_nat n r))) (Zpower_nat n (Init.Nat.add (digit q) r)) *)
intros H'; Contradict H'; auto with arith.
rewrite Zpower_nat_is_exp; rewrite Zabs_Zmult;
 rewrite (fun x => Zabs_eq (Zpower_nat n x)); auto with zarith arith.
Qed.
 
Theorem digit_minus1 : forall p : nat, digit (Zpower_nat n p - 1) = p.
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros p; case p; auto.
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros n0; apply digitInv; auto.
(* Goal: Z.le (Zpower_nat n (Init.Nat.pred (S n0))) (Z.abs (Z.sub (Zpower_nat n (S n0)) (Zpos xH))) *)
(* Goal: Z.lt (Z.abs (Z.sub (Zpower_nat n (S n0)) (Zpos xH))) (Zpower_nat n (S n0)) *)
rewrite Zabs_eq.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
cut (Zpower_nat n (pred (S n0)) < Zpower_nat n (S n0))%Z; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
cut (0 < Zpower_nat n (S n0))%Z; auto with zarith.
(* Goal: Z.lt (Zpos xH) (Z.mul n (Zpos xH)) *)
rewrite Zabs_eq; auto with zarith.
Qed.
 
Theorem digit_bound :
 forall (x y z : Z) (n : nat),
 (Zabs x <= Zabs y)%Z ->
 (Zabs y <= Zabs z)%Z -> digit x = n -> digit z = n -> digit y = n.
(* Goal: forall (x y z : Z) (n : nat) (_ : Z.le (Z.abs x) (Z.abs y)) (_ : Z.le (Z.abs y) (Z.abs z)) (_ : @eq nat (digit x) n) (_ : @eq nat (digit z) n), @eq nat (digit y) n *)
intros x y z n0 H' H'0 H'1 H'2; apply le_antisym.
(* Goal: le (digit y) n0 *)
(* Goal: le n0 (digit y) *)
rewrite <- H'2; auto with arith.
(* Goal: le n0 (digit y) *)
rewrite <- H'1; auto with arith.
Qed.
 
Theorem digit_abs : forall p : Z, digit (Zabs p) = digit p.
(* Goal: forall (r : Z) (_ : Z.lt Z0 r) (_ : Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end), Z.lt v match r with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end *)
intros p; case p; simpl in |- *; auto.
Qed.
(* Strict comparison on the number of digits gives comparison on the numbers *)
 
Theorem digit_anti_monotone_lt :
 (1 < n)%Z -> forall p q : Z, digit p < digit q -> (Zabs p < Zabs q)%Z.
(* Goal: forall (_ : Z.lt (Zpos xH) n) (p q : Z) (_ : lt (digit p) (digit q)), Z.lt (Z.abs p) (Z.abs q) *)
intros H' p q H'0.
(* Goal: forall _ : lt r (digit q), @eq nat (digit q) r *)
case (Zle_or_lt (Zabs q) (Zabs p)); auto; intros H'1.
(* Goal: Z.lt (Z.abs p) (Z.abs q) *)
Contradict H'0.
(* Goal: not (lt (digit p) (digit q)) *)
case (Zle_lt_or_eq _ _ H'1); intros H'2.
(* Goal: not (lt (digit p) (digit q)) *)
(* Goal: not (lt (digit p) (digit q)) *)
apply le_not_lt; auto with arith.
rewrite <- (digit_abs p); rewrite <- (digit_abs q); rewrite H'2;
 auto with arith.
Qed.
End Pdigit.
Hint Resolve Zpower_nat_less: zarith.
Hint Resolve Zpower_nat_monotone_lt: zarith.
Hint Resolve Zpower_nat_monotone_le: zarith.
Hint Unfold digit.
Hint Resolve digitLess: zarith.
Hint Resolve digitMore: zarith.
Hint Resolve digit_monotone: arith.