(****************************************************************************
                                                                             
          IEEE754  :  MSB                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export Fprop.
Require Export Zdivides.
Require Export Fnorm.
Section mf.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Fixpoint maxDiv (v : Z) (p : nat) {struct p} : nat :=
  match p with
  | O => 0
  | S p' =>
      match ZdividesP v (Zpower_nat radix p) with
      | left _ => p
      | right _ => maxDiv v p'
      end
  end.
 
Theorem maxDivLess : forall (v : Z) (p : nat), maxDiv v p <= p.
(* Goal: forall (v : Z) (p : nat), @eq nat (maxDiv v p) (maxDiv (Z.abs v) p) *)
intros v p; elim p; simpl in |- *; auto.
(* Goal: forall (n : nat) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), lt (if ZdividesP v (Z.mul radix (Zpower_nat radix n)) then S n else maxDiv v n) (S n) *)
intros n H'; case (ZdividesP v (radix * Zpower_nat radix n)); auto.
Qed.
 
Theorem maxDivLt :
 forall (v : Z) (p : nat),
 ~ Zdivides v (Zpower_nat radix p) -> maxDiv v p < p.
(* Goal: forall (v : Z) (p : nat) (_ : not (Zdivides v (Zpower_nat radix p))), lt (maxDiv v p) p *)
intros v p; case p; simpl in |- *; auto.
(* Goal: forall _ : not (Zdivides v (Zpos xH)), lt O O *)
(* Goal: forall (n : nat) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), lt (if ZdividesP v (Z.mul radix (Zpower_nat radix n)) then S n else maxDiv v n) (S n) *)
intros H'; case H'.
(* Goal: Zdivides v (Z.of_nat (S O)) *)
(* Goal: forall (n : nat) (_ : Zdivides v (Zpower_nat radix (maxDiv v n))), Zdivides v (Zpower_nat radix (maxDiv v (S n))) *)
apply Zdivides1.
(* Goal: forall (n : nat) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), lt (if ZdividesP v (Z.mul radix (Zpower_nat radix n)) then S n else maxDiv v n) (S n) *)
intros n H'; case (ZdividesP v (radix * Zpower_nat radix n)); auto.
(* Goal: forall _ : Zdivides v (Z.mul radix (Zpower_nat radix n)), lt (S n) (S n) *)
(* Goal: forall _ : not (Zdivides v (Z.mul radix (Zpower_nat radix n))), lt (maxDiv v n) (S n) *)
intros H'0; case H'; auto.
(* Goal: forall _ : not (Zdivides v (Z.mul radix (Zpower_nat radix n))), lt (maxDiv v n) (S n) *)
intros H'0; generalize (maxDivLess v n); auto with arith.
Qed.
 
Theorem maxDivCorrect :
 forall (v : Z) (p : nat), Zdivides v (Zpower_nat radix (maxDiv v p)).
(* Goal: forall (v : Z) (p : nat), Zdivides v (Zpower_nat radix (maxDiv v p)) *)
intros v p; elim p.
(* Goal: Zdivides v (Zpower_nat radix (maxDiv v O)) *)
(* Goal: forall (n : nat) (_ : Zdivides v (Zpower_nat radix (maxDiv v n))), Zdivides v (Zpower_nat radix (maxDiv v (S n))) *)
unfold maxDiv in |- *; rewrite Zpower_nat_O; auto.
(* Goal: Zdivides v (Z.of_nat (S O)) *)
(* Goal: forall (n : nat) (_ : Zdivides v (Zpower_nat radix (maxDiv v n))), Zdivides v (Zpower_nat radix (maxDiv v (S n))) *)
apply Zdivides1.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
simpl in |- *.
intros n H'; case (ZdividesP v (radix * Zpower_nat radix n)); simpl in |- *;
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
 auto with zarith.
Qed.
 
Theorem maxDivSimplAux :
 forall (v : Z) (p q : nat),
 p = maxDiv v (S (q + p)) -> p = maxDiv v (S p).
intros v p q; elim q.
simpl in |- *; case (ZdividesP v (radix * Zpower_nat radix p)); auto.
intros n H' H'0.
apply H'; auto; clear H'.
simpl in H'0; generalize H'0; clear H'0.
case (ZdividesP v (radix * (radix * Zpower_nat radix (n + p)))).
2: simpl in |- *; auto.
intros H' H'0; Contradict H'0; auto with zarith.
Qed.
 
Theorem maxDivSimpl :
 forall (v : Z) (p q : nat),
 p < q -> p = maxDiv v q -> p = maxDiv v (S p).
(* Goal: forall (v : Z) (p q : nat) (_ : lt p q) (_ : @eq nat p (maxDiv v (S p))), @eq nat p (maxDiv v q) *)
intros v p q H' H'0.
(* Goal: @eq nat p (maxDiv v (S p)) *)
apply maxDivSimplAux with (q := q - S p); auto.
(* Goal: @eq nat p (maxDiv v (S (Init.Nat.add (Init.Nat.sub q (S p)) p))) *)
replace (S (q - S p + p)) with q; auto with zarith.
Qed.
 
Theorem maxDivSimplInvAux :
 forall (v : Z) (p q : nat),
 p = maxDiv v (S p) -> p = maxDiv v (S (q + p)).
(* Goal: forall (v : Z) (p q : nat) (_ : @eq nat p (maxDiv v (S p))), @eq nat p (maxDiv v (S (Init.Nat.add q p))) *)
intros v p q H'; elim q.
(* Goal: @eq nat p (maxDiv v (S (Init.Nat.add O p))) *)
(* Goal: forall (n : nat) (_ : @eq nat p (maxDiv v (S (Init.Nat.add n p)))), @eq nat p (maxDiv v (S (Init.Nat.add (S n) p))) *)
simpl in |- *; auto.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros n; simpl in |- *.
(* Goal: forall _ : @eq nat p (if ZdividesP v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))) then S (Init.Nat.add n p) else maxDiv v (Init.Nat.add n p)), @eq nat p (if ZdividesP v (Z.mul radix (Z.mul radix (Zpower_nat radix (Init.Nat.add n p)))) then S (S (Init.Nat.add n p)) else if ZdividesP v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))) then S (Init.Nat.add n p) else maxDiv v (Init.Nat.add n p)) *)
case (ZdividesP v (radix * Zpower_nat radix (n + p))); auto.
(* Goal: forall (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))))) (_ : @eq nat p (maxDiv v (Init.Nat.add n p))), @eq nat p (if ZdividesP v (Z.mul radix (Z.mul radix (Zpower_nat radix (Init.Nat.add n p)))) then S (S (Init.Nat.add n p)) else maxDiv v (Init.Nat.add n p)) *)
case (ZdividesP v (radix * (radix * Zpower_nat radix (n + p)))); auto.
(* Goal: forall (_ : Zdivides v (Z.mul radix (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))))) (_ : Zdivides v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p)))) (_ : @eq nat p (S (Init.Nat.add n p))), @eq nat p (S (S (Init.Nat.add n p))) *)
(* Goal: forall (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))))) (_ : @eq nat p (maxDiv v (Init.Nat.add n p))), @eq nat p (if ZdividesP v (Z.mul radix (Z.mul radix (Zpower_nat radix (Init.Nat.add n p)))) then S (S (Init.Nat.add n p)) else maxDiv v (Init.Nat.add n p)) *)
intros H'0 H'1 H'2; Contradict H'2; auto with zarith.
(* Goal: forall (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))))) (_ : @eq nat p (maxDiv v (Init.Nat.add n p))), @eq nat p (if ZdividesP v (Z.mul radix (Z.mul radix (Zpower_nat radix (Init.Nat.add n p)))) then S (S (Init.Nat.add n p)) else maxDiv v (Init.Nat.add n p)) *)
case (ZdividesP v (radix * (radix * Zpower_nat radix (n + p)))); auto.
(* Goal: forall (_ : Zdivides v (Z.mul radix (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))))) (_ : @eq nat p (maxDiv v (Init.Nat.add n p))), @eq nat p (S (S (Init.Nat.add n p))) *)
intros H'0 H'1 H'2; case H'1.
(* Goal: Zdivides v (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))) *)
case H'0; intros z1 Hz1; exists (radix * z1)%Z;rewrite Hz1.
(* Goal: @eq Z (Z.mul (Z.mul radix (Z.mul radix (Zpower_nat radix (Init.Nat.add n p)))) z1) (Z.mul (Z.mul radix (Zpower_nat radix (Init.Nat.add n p))) (Z.mul radix z1)) *)
unfold Zpower_nat; simpl; ring.
Qed.
 
Theorem maxDivSimplInv :
 forall (v : Z) (p q : nat),
 p < q -> p = maxDiv v (S p) -> p = maxDiv v q.
(* Goal: forall (v : Z) (p q : nat) (_ : lt p q) (_ : @eq nat p (maxDiv v (S p))), @eq nat p (maxDiv v q) *)
intros v p q H' H'0.
(* Goal: @eq nat p (maxDiv v q) *)
replace q with (S (q - S p + p)); auto with zarith.
(* Goal: @eq nat p (maxDiv v (S (Init.Nat.add (Init.Nat.sub q (S p)) p))) *)
apply maxDivSimplInvAux; auto.
Qed.
 
Theorem maxDivUnique :
 forall (v : Z) (p : nat),
 p = maxDiv v (S p) ->
 Zdivides v (Zpower_nat radix p) /\ ~ Zdivides v (Zpower_nat radix (S p)).
(* Goal: forall (v : Z) (p : nat) (_ : @eq nat p (maxDiv v (S p))), and (Zdivides v (Zpower_nat radix p)) (not (Zdivides v (Zpower_nat radix (S p)))) *)
intros v p H'; split.
(* Goal: Zdivides v (Zpower_nat radix p) *)
(* Goal: not (Zdivides v (Zpower_nat radix (S p))) *)
rewrite H'.
(* Goal: Zdivides v (Zpower_nat radix (maxDiv v (S p))) *)
(* Goal: not (Zdivides v (Zpower_nat radix (S p))) *)
apply maxDivCorrect; auto.
(* Goal: not (Zdivides v (Zpower_nat radix (S p))) *)
red in |- *; intros H'0; generalize H'; clear H'.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
simpl in |- *.
(* Goal: @eq nat p (maxDiv v (S (Init.Nat.add O p))) *)
(* Goal: forall (n : nat) (_ : @eq nat p (maxDiv v (S (Init.Nat.add n p)))), @eq nat p (maxDiv v (S (Init.Nat.add (S n) p))) *)
case (ZdividesP v (radix * Zpower_nat radix p)); simpl in |- *; auto.
(* Goal: forall (_ : Zdivides v (Z.mul radix (Zpower_nat radix p))) (_ : @eq nat p (S p)), False *)
intros H' H'1; Contradict H'1; auto with zarith.
Qed.
 
Theorem maxDivUniqueDigit :
 forall v : Z,
 v <> 0 ->
 Zdivides v (Zpower_nat radix (maxDiv v (digit radix v))) /\
 ~ Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))).
(* Goal: forall (v : Z) (_ : not (@eq Z v (Z.of_nat O))), and (Zdivides v (Zpower_nat radix (maxDiv v (digit radix v)))) (not (Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))))) *)
intros v H'.
(* Goal: and (Zdivides v (Zpower_nat radix (maxDiv v (digit radix v)))) (not (Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))))) *)
apply maxDivUnique; auto.
(* Goal: @eq nat (maxDiv v (digit radix v)) (maxDiv v (S (maxDiv v (digit radix v)))) *)
apply maxDivSimpl with (q := digit radix v); auto.
(* Goal: lt (maxDiv (Fnum x) (Fdigit radix x)) (Fdigit radix x) *)
apply maxDivLt; auto.
(* Goal: not (Zdivides v (Zpower_nat radix (digit radix v))) *)
apply NotDividesDigit; auto.
Qed.
 
Theorem maxDivUniqueInverse :
 forall (v : Z) (p : nat),
 Zdivides v (Zpower_nat radix p) ->
 ~ Zdivides v (Zpower_nat radix (S p)) -> p = maxDiv v (S p).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros v p H' H'0; simpl in |- *.
(* Goal: @eq nat p (if ZdividesP v (Z.mul radix (Zpower_nat radix p)) then S p else maxDiv v p) *)
case (ZdividesP v (radix * Zpower_nat radix p)); auto.
(* Goal: @eq nat p (maxDiv v (S (Init.Nat.add O p))) *)
(* Goal: forall (n : nat) (_ : @eq nat p (maxDiv v (S (Init.Nat.add n p)))), @eq nat p (maxDiv v (S (Init.Nat.add (S n) p))) *)
intros H'1; case H'0; simpl in |- *; auto.
(* Goal: forall _ : not (Zdivides v (Z.mul radix (Zpower_nat radix p))), @eq nat p (maxDiv v p) *)
intros H'1.
(* Goal: @eq nat p (maxDiv v (S (Init.Nat.add O p))) *)
(* Goal: forall (n : nat) (_ : @eq nat p (maxDiv v (S (Init.Nat.add n p)))), @eq nat p (maxDiv v (S (Init.Nat.add (S n) p))) *)
generalize H'; case p; simpl in |- *; auto.
(* Goal: forall (n : nat) (_ : Zdivides v (Z.mul radix (Zpower_nat radix n))), @eq nat (S n) (if ZdividesP v (Z.mul radix (Zpower_nat radix n)) then S n else maxDiv v n) *)
intros n H'2; case (ZdividesP v (radix * Zpower_nat radix n)); auto.
(* Goal: forall _ : not (Zdivides v (Z.mul radix (Zpower_nat radix n))), @eq nat (S n) (maxDiv v n) *)
intros H'3; case H'3; auto.
Qed.
 
Theorem maxDivUniqueInverseDigit :
 forall (v : Z) (p : nat),
 v <> 0 ->
 Zdivides v (Zpower_nat radix p) ->
 ~ Zdivides v (Zpower_nat radix (S p)) -> p = maxDiv v (digit radix v).
intros v p H' H'0 H'1.
apply maxDivSimplInv; auto.
2: apply maxDivUniqueInverse; auto.
apply Zpower_nat_anti_monotone_lt with (n := radix); auto.
apply Zle_lt_trans with (m := Zabs v); auto.
rewrite <- (fun x => Zabs_eq (Zpower_nat radix x)); auto with zarith;
 apply ZDividesLe; auto.
apply digitMore; auto.
Qed.
 
Theorem maxDivPlus :
 forall (v : Z) (n : nat),
 v <> 0 ->
 maxDiv (v * Zpower_nat radix n) (digit radix v + n) =
 maxDiv v (digit radix v) + n.
(* Goal: forall (v : Z) (n : nat) (_ : not (@eq Z v (Z.of_nat O))), @eq nat (maxDiv (Z.mul v (Zpower_nat radix n)) (Init.Nat.add (digit radix v) n)) (Init.Nat.add (maxDiv v (digit radix v)) n) *)
intros v n H.
(* Goal: @eq nat (maxDiv (Z.mul v (Zpower_nat radix n)) (Init.Nat.add (digit radix v) n)) (Init.Nat.add (maxDiv v (digit radix v)) n) *)
replace (digit radix v + n) with (digit radix (v * Zpower_nat radix n)); auto.
(* Goal: @eq nat (maxDiv (Z.mul v (Zpower_nat radix n)) (digit radix (Z.mul v (Zpower_nat radix n)))) (Init.Nat.add (maxDiv v (digit radix v)) n) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
apply sym_equal.
(* Goal: @eq nat (Init.Nat.add (maxDiv v (digit radix v)) n) (maxDiv (Z.mul v (Zpower_nat radix n)) (digit radix (Z.mul v (Zpower_nat radix n)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
apply maxDivUniqueInverseDigit; auto.
(* Goal: not (@eq Z (Z.mul v (Zpower_nat radix n)) (Z.of_nat O)) *)
(* Goal: Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (Init.Nat.add (maxDiv v (digit radix v)) n)) *)
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (S (Init.Nat.add (maxDiv v (digit radix v)) n)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
red in |- *; intros Z1; case (Zmult_integral _ _ Z1); intros Z2.
(* Goal: False *)
(* Goal: False *)
(* Goal: Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (Init.Nat.add (maxDiv v (digit radix v)) n)) *)
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (S (Init.Nat.add (maxDiv v (digit radix v)) n)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
case H; auto.
(* Goal: False *)
(* Goal: Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (Init.Nat.add (maxDiv v (digit radix v)) n)) *)
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (S (Init.Nat.add (maxDiv v (digit radix v)) n)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
absurd (0 < Zpower_nat radix n)%Z; auto with zarith.
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (Init.Nat.add (S (maxDiv v (digit radix v))) n))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
rewrite Zpower_nat_is_exp.
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Z.mul (Zpower_nat radix (S (maxDiv v (digit radix v)))) (Zpower_nat radix n))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
repeat rewrite (fun x : Z => Zmult_comm x (Zpower_nat radix n)).
(* Goal: Zdivides (Z.mul (Zpower_nat radix n) v) (Z.mul (Zpower_nat radix n) (Zpower_nat radix (maxDiv v (digit radix v)))) *)
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (S (Init.Nat.add (maxDiv v (digit radix v)) n)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
apply ZdividesMult; auto.
(* Goal: not (Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v))))) *)
(* Goal: Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
case (maxDivUniqueDigit v); auto.
replace (S (maxDiv v (digit radix v) + n)) with
 (S (maxDiv v (digit radix v)) + n); auto.
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Zpower_nat radix (Init.Nat.add (S (maxDiv v (digit radix v))) n))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
rewrite Zpower_nat_is_exp.
(* Goal: not (Zdivides (Z.mul v (Zpower_nat radix n)) (Z.mul (Zpower_nat radix (S (maxDiv v (digit radix v)))) (Zpower_nat radix n))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
repeat rewrite (fun x : Z => Zmult_comm x (Zpower_nat radix n)).
(* Goal: not (Zdivides (Z.mul (Zpower_nat radix n) v) (Z.mul (Zpower_nat radix n) (Zpower_nat radix (S (maxDiv v (digit radix v)))))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
red in |- *; intros H'.
(* Goal: False *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
absurd (Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v))))).
(* Goal: not (Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v))))) *)
(* Goal: Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
case (maxDivUniqueDigit v); auto.
(* Goal: Zdivides v (Zpower_nat radix (S (maxDiv v (digit radix v)))) *)
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
apply ZdividesDiv with (p := Zpower_nat radix n); auto with zarith.
(* Goal: @eq nat (digit radix (Z.mul v (Zpower_nat radix n))) (Init.Nat.add (digit radix v) n) *)
apply digitAdd; auto with zarith.
Qed.
 
Definition LSB (x : float) :=
  (Z_of_nat (maxDiv (Fnum x) (Fdigit radix x)) + Fexp x)%Z.
 
Theorem LSB_shift :
 forall (x : float) (n : nat), ~ is_Fzero x -> LSB x = LSB (Fshift radix n x).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x n H'; unfold LSB, Fdigit in |- *; simpl in |- *.
(* Goal: @eq Z (Z.add (Z.of_nat (maxDiv (Fnum x) (digit radix (Fnum x)))) (Fexp x)) (Z.add (Z.of_nat (maxDiv (Z.mul (Fnum x) (Zpower_nat radix n)) (digit radix (Z.mul (Fnum x) (Zpower_nat radix n))))) (Z.sub (Fexp x) (Z.of_nat n))) *)
rewrite digitAdd; auto with arith.
(* Goal: @eq Z (Z.add (Z.of_nat (maxDiv (Fnum x) (digit radix (Fnum x)))) (Fexp x)) (Z.add (Z.of_nat (maxDiv (Z.mul (Fnum x) (Zpower_nat radix n)) (Init.Nat.add (digit radix (Fnum x)) n))) (Z.sub (Fexp x) (Z.of_nat n))) *)
rewrite maxDivPlus; auto.
(* Goal: @eq Z (Z.add (Z.of_nat (maxDiv (Fnum x) (digit radix (Fnum x)))) (Fexp x)) (Z.add (Z.of_nat (Init.Nat.add (maxDiv (Fnum x) (digit radix (Fnum x))) n)) (Z.sub (Fexp x) (Z.of_nat n))) *)
rewrite inj_plus; ring.
Qed.
 
Theorem LSB_comp :
 forall (x y : float) (n : nat), ~ is_Fzero x -> x = y :>R -> LSB x = LSB y.
(* Goal: forall (x y : float) (_ : nat) (_ : not (is_Fzero x)) (_ : @eq R (FtoRradix x) (FtoRradix y)), @eq Z (MSB x) (MSB y) *)
intros x y H' H'0 H'1.
(* Goal: @eq Z (MSB x) (MSB y) *)
case (FshiftCorrectSym radix) with (2 := H'1); auto.
(* Goal: forall (x0 : nat) (_ : @ex nat (fun m : nat => @eq float (Fshift radix x0 x) (Fshift radix m y))), @eq Z (MSB x) (MSB y) *)
intros m1 H'2; elim H'2; intros m2 E; clear H'2.
(* Goal: @eq Z (LSB x) (LSB y) *)
rewrite (LSB_shift x m1); auto.
(* Goal: @eq Z (MSB (Fshift radix m1 x)) (MSB y) *)
rewrite E; auto.
(* Goal: @eq Z (LSB (Fshift radix m2 y)) (LSB y) *)
apply sym_equal; apply LSB_shift; auto.
(* Goal: not (is_Fzero y) *)
apply (NisFzeroComp radix) with (x := x); auto.
Qed.
 
Theorem maxDiv_opp :
 forall (v : Z) (p : nat), maxDiv v p = maxDiv (- v) p.
(* Goal: forall (v : Z) (p : nat), @eq nat (maxDiv v p) (maxDiv (Z.abs v) p) *)
intros v p; elim p; simpl in |- *; auto.
intros n H; case (ZdividesP v (radix * Zpower_nat radix n));
 case (ZdividesP (- v) (radix * Zpower_nat radix n)); auto.
(* Goal: forall (_ : not (Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n)))) (_ : Zdivides v (Z.mul radix (Zpower_nat radix n))), @eq nat (S n) (maxDiv (Z.abs v) n) *)
(* Goal: forall (_ : Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), @eq nat (maxDiv v n) (S n) *)
intros Z1 Z2; case Z1.
(* Goal: Zdivides (Z.opp v) (Z.mul radix (Zpower_nat radix n)) *)
(* Goal: forall (_ : Zdivides (Z.opp v) (Z.mul radix (Zpower_nat radix n))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), @eq nat (maxDiv v n) (S n) *)
case Z2; intros z1 Hz1; exists (- z1)%Z; rewrite Hz1; ring.
(* Goal: forall (_ : Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), @eq nat (maxDiv v n) (S n) *)
intros Z1 Z2; case Z2.
(* Goal: Zdivides v (Z.mul radix (Zpower_nat radix n)) *)
case Z1; intros z1 Hz1; exists (- z1)%Z.
(* Goal: @eq Z v (Z.mul (Z.mul radix (Zpower_nat radix n)) (Z.opp z1)) *)
rewrite <- (Zopp_involutive v); rewrite Hz1; ring.
Qed.
 
Theorem LSB_opp : forall x : float, LSB x = LSB (Fopp x).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x; unfold LSB in |- *; simpl in |- *.
(* Goal: @eq Z (Z.pred (Z.add (Z.of_nat (Fdigit radix x)) (Fexp x))) (Z.pred (Z.add (Z.of_nat (Fdigit radix (Fopp x))) (Fexp x))) *)
rewrite Fdigit_opp; auto.
(* Goal: @eq Z (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) (Z.add (Z.of_nat (maxDiv (Z.opp (Fnum x)) (Fdigit radix x))) (Fexp x)) *)
rewrite maxDiv_opp; auto.
Qed.
 
Theorem maxDiv_abs :
 forall (v : Z) (p : nat), maxDiv v p = maxDiv (Zabs v) p.
(* Goal: forall (v : Z) (p : nat), @eq nat (maxDiv v p) (maxDiv (Z.abs v) p) *)
intros v p; elim p; simpl in |- *; auto.
intros n H; case (ZdividesP v (radix * Zpower_nat radix n));
 case (ZdividesP (Zabs v) (radix  * Zpower_nat radix n));
 auto.
(* Goal: forall (_ : not (Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n)))) (_ : Zdivides v (Z.mul radix (Zpower_nat radix n))), @eq nat (S n) (maxDiv (Z.abs v) n) *)
(* Goal: forall (_ : Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), @eq nat (maxDiv v n) (S n) *)
intros Z1 Z2; case Z1.
(* Goal: Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n)) *)
(* Goal: forall (_ : Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), @eq nat (maxDiv v n) (S n) *)
case Z2; intros z1 Hz1; exists (Zabs z1); rewrite Hz1.
(* Goal: @eq Z (Z.abs (Z.mul (Z.mul radix (Zpower_nat radix n)) z1)) (Z.mul (Z.mul radix (Zpower_nat radix n)) (Z.abs z1)) *)
(* Goal: forall (_ : Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), @eq nat (maxDiv v n) (S n) *)
rewrite Zabs_Zmult; f_equal. apply Zabs_eq. auto with zarith.
(* Goal: forall (_ : Zdivides (Z.abs v) (Z.mul radix (Zpower_nat radix n))) (_ : not (Zdivides v (Z.mul radix (Zpower_nat radix n)))), @eq nat (maxDiv v n) (S n) *)
intros Z1 Z2; case Z2.
(* Goal: Zdivides v (Z.mul radix (Zpower_nat radix n)) *)
case Z1; intros z1 Hz1.
(* Goal: Zdivides v (Z.mul radix (Zpower_nat radix n)) *)
case (Zle_or_lt v 0); intros Z4.
exists (- z1)%Z; rewrite <- (Zopp_involutive v);
(* Goal: @eq Z (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)) *)
 rewrite <- (Zabs_eq_opp v); auto; rewrite Hz1; ring.
(* Goal: Zdivides v (Z.mul radix (Zpower_nat radix n)) *)
exists z1; rewrite <- (Zabs_eq v); auto with zarith; rewrite Hz1; ring.
Qed.

Theorem LSB_abs : forall x : float, LSB x = LSB (Fabs x).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x; unfold LSB in |- *; simpl in |- *.
(* Goal: @eq Z (Z.pred (Z.add (Z.of_nat (Fdigit radix x)) (Fexp x))) (Z.pred (Z.add (Z.of_nat (Fdigit radix (Fabs x))) (Fexp x))) *)
rewrite Fdigit_abs; auto.
(* Goal: @eq Z (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) (Z.add (Z.of_nat (maxDiv (Z.abs (Fnum x)) (Fdigit radix x))) (Fexp x)) *)
rewrite maxDiv_abs; auto.
Qed.
 
Definition MSB (x : float) := Zpred (Z_of_nat (Fdigit radix x) + Fexp x).
 
Theorem MSB_shift :
 forall (x : float) (n : nat), ~ is_Fzero x -> MSB x = MSB (Fshift radix n x).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros; unfold MSB, Fshift, Fdigit in |- *; simpl in |- *.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite digitAdd; auto with zarith.
(* Goal: @eq Z (Z.pred (Z.add (Z.of_nat (digit radix (Fnum x))) (Fexp x))) (Z.pred (Z.add (Z.of_nat (Init.Nat.add (digit radix (Fnum x)) n)) (Z.sub (Fexp x) (Z.of_nat n)))) *)
rewrite inj_plus; unfold Zpred in |- *; ring.
Qed.
 
Theorem MSB_comp :
 forall (x y : float) (n : nat), ~ is_Fzero x -> x = y :>R -> MSB x = MSB y.
(* Goal: forall (x y : float) (_ : nat) (_ : not (is_Fzero x)) (_ : @eq R (FtoRradix x) (FtoRradix y)), @eq Z (MSB x) (MSB y) *)
intros x y H' H'0 H'1.
(* Goal: @eq Z (MSB x) (MSB y) *)
case (FshiftCorrectSym radix) with (2 := H'1); auto.
(* Goal: forall (x0 : nat) (_ : @ex nat (fun m : nat => @eq float (Fshift radix x0 x) (Fshift radix m y))), @eq Z (MSB x) (MSB y) *)
intros m1 H'2; elim H'2; intros m2 E; clear H'2.
(* Goal: @eq Z (MSB x) (MSB y) *)
rewrite (MSB_shift x m1); auto.
(* Goal: @eq Z (MSB (Fshift radix m1 x)) (MSB y) *)
rewrite E; auto.
(* Goal: @eq Z (MSB (Fshift radix m2 y)) (MSB y) *)
apply sym_equal; apply MSB_shift; auto.
(* Goal: not (is_Fzero y) *)
apply (NisFzeroComp radix) with (x := x); auto.
Qed.
 
Theorem MSB_opp : forall x : float, MSB x = MSB (Fopp x).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x; unfold MSB in |- *; simpl in |- *.
(* Goal: @eq Z (Z.pred (Z.add (Z.of_nat (Fdigit radix x)) (Fexp x))) (Z.pred (Z.add (Z.of_nat (Fdigit radix (Fopp x))) (Fexp x))) *)
rewrite Fdigit_opp; auto.
Qed.
 
Theorem MSB_abs : forall x : float, MSB x = MSB (Fabs x).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x; unfold MSB in |- *; simpl in |- *.
(* Goal: @eq Z (Z.pred (Z.add (Z.of_nat (Fdigit radix x)) (Fexp x))) (Z.pred (Z.add (Z.of_nat (Fdigit radix (Fabs x))) (Fexp x))) *)
rewrite Fdigit_abs; auto.
Qed.
 
Theorem LSB_le_MSB : forall x : float, ~ is_Fzero x -> (LSB x <= MSB x)%Z.
(* Goal: forall (x : float) (_ : not (is_Fzero x)), Z.le (LSB x) (MSB x) *)
intros x H'; unfold LSB, MSB in |- *.
(* Goal: Z.le (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) (Z.pred (Z.add (Z.of_nat (Fdigit radix x)) (Fexp x))) *)
apply Zle_Zpred.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
cut (maxDiv (Fnum x) (Fdigit radix x) < Fdigit radix x); auto with zarith.
(* Goal: lt (maxDiv (Fnum x) (Fdigit radix x)) (Fdigit radix x) *)
apply maxDivLt; auto.
(* Goal: not (Zdivides v (Zpower_nat radix (digit radix v))) *)
unfold Fdigit in |- *; apply NotDividesDigit; auto.
Qed.
 
Theorem Fexp_le_LSB : forall x : float, (Fexp x <= LSB x)%Z.
(* Goal: forall x : float, Z.le (Fexp x) (LSB x) *)
intros x; unfold LSB in |- *.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
auto with zarith.
Qed.
 
Theorem Ulp_Le_LSigB :
 forall x : float, (Float 1%nat (Fexp x) <= Float 1%nat (LSB x))%R.
(* Goal: forall x : float, Rle (FtoRradix (Float (Z.of_nat (S O)) (Fexp x))) (FtoRradix (Float (Z.of_nat (S O)) (LSB x))) *)
intros x; apply (oneExp_le radix); auto.
(* Goal: Z.le (Fexp x) (LSB x) *)
apply Fexp_le_LSB; auto.
Qed.
 
Theorem Fexp_le_MSB : forall x : float, ~ is_Fzero x -> (Fexp x <= MSB x)%Z.
(* Goal: forall (x : float) (_ : not (is_Fzero x)), Z.le (Fexp x) (MSB x) *)
intros x H'; unfold MSB in |- *.
cut (Fdigit radix x <> 0%Z :>Z); unfold Zpred in |- *;
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
 auto with zarith.
(* Goal: not (@eq nat (Fdigit radix x) O) *)
unfold Fdigit in |- *.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
red in |- *; intros H'0; absurd (digit radix (Fnum x) = 0); auto with zarith.
(* Goal: not (@eq nat (digit radix (Fnum y)) O) *)
apply not_eq_sym; apply lt_O_neq; apply digitNotZero; auto.
Qed.
 
Theorem MSB_le_abs :
 forall x : float, ~ is_Fzero x -> (Float 1%nat (MSB x) <= Fabs x)%R.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x H'; unfold MSB, FtoRradix, FtoR in |- *; simpl in |- *.
replace (Zpred (Fdigit radix x + Fexp x)) with
 (Zpred (Fdigit radix x) + Fexp x)%Z; [ idtac | unfold Zpred in |- *; ring ].
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Zquotient (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)))))) (powerRZ (IZR radix) (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)))) *)
rewrite powerRZ_add; auto with real zarith.
(* Goal: Rlt (Rmult (IZR (Z.abs (Fnum x))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Zpos xH)) (Rmult (powerRZ (IZR radix) (Z.of_nat (Fdigit radix (Fabs x)))) (powerRZ (IZR radix) (Fexp x)))) *)
rewrite Rmult_1_l.
(* Goal: Rlt (Rmult (IZR (Z.abs (Fnum x))) (powerRZ (IZR radix) (Fexp x))) (Rmult (powerRZ (IZR radix) (Z.of_nat (Fdigit radix (Fabs x)))) (powerRZ (IZR radix) (Fexp x))) *)
repeat rewrite (fun r : R => Rmult_comm r (powerRZ radix (Fexp x))).
(* Goal: Rle (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Z.pred (Z.of_nat (Fdigit radix x))))) (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Z.abs (Fnum x)))) *)
apply Rmult_le_compat_l; auto with real zarith.
(* Goal: Rle (powerRZ (IZR radix) (Z.pred (Z.of_nat (Fdigit radix x)))) (IZR (Z.abs (Fnum x))) *)
rewrite <- inj_pred; auto with real zarith.
(* Goal: Rle (powerRZ (IZR radix) (Z.of_nat (Init.Nat.pred (Fdigit radix x)))) (IZR (Z.abs (Fnum x))) *)
(* Goal: not (@eq nat (Fdigit radix x) O) *)
rewrite <- Zpower_nat_Z_powerRZ; auto.
(* Goal: Rle (IZR (Zpower_nat radix (Init.Nat.pred (Fdigit radix x)))) (IZR (Z.abs (Fnum x))) *)
(* Goal: not (@eq nat (Fdigit radix x) O) *)
apply Rle_IZR; auto.
(* Goal: Z.lt (Z.abs (Fnum x)) (Zpower_nat radix (Fdigit radix (Fabs x))) *)
unfold Fdigit in |- *; auto with arith.
(* Goal: Z.le (Zpower_nat radix (Init.Nat.pred (digit radix (Fnum x)))) (Z.abs (Fnum x)) *)
(* Goal: not (@eq nat (Fdigit radix x) O) *)
apply digitLess; auto.
(* Goal: not (@eq nat (Fdigit radix x) O) *)
unfold Fdigit in |- *.
(* Goal: not (@eq nat (digit radix (Fnum y)) O) *)
apply not_eq_sym; apply lt_O_neq; apply digitNotZero; auto.
Qed.
 
Theorem abs_lt_MSB :
 forall x : float, (Fabs x < Float 1%nat (Zsucc (MSB x)))%R.
(* Goal: forall x : float, Rlt (FtoRradix (Fabs x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (MSB x)))) *)
intros x.
(* Goal: Rlt (FtoRradix (Fabs x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (MSB x)))) *)
rewrite (MSB_abs x).
(* Goal: Rlt (FtoRradix (Fabs x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (MSB (Fabs x))))) *)
unfold MSB, FtoRradix, FtoR in |- *.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
rewrite <- Zsucc_pred; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Zquotient (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)))))) (powerRZ (IZR radix) (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)))) *)
rewrite powerRZ_add; auto with real zarith.
(* Goal: Rlt (Rmult (IZR (Z.abs (Fnum x))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Zpos xH)) (Rmult (powerRZ (IZR radix) (Z.of_nat (Fdigit radix (Fabs x)))) (powerRZ (IZR radix) (Fexp x)))) *)
rewrite Rmult_1_l.
(* Goal: Rlt (Rmult (IZR (Z.abs (Fnum x))) (powerRZ (IZR radix) (Fexp x))) (Rmult (powerRZ (IZR radix) (Z.of_nat (Fdigit radix (Fabs x)))) (powerRZ (IZR radix) (Fexp x))) *)
repeat rewrite (fun r : R => Rmult_comm r (powerRZ radix (Fexp x))).
(* Goal: Rlt (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Z.abs (Fnum x)))) (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Z.of_nat (Fdigit radix (Fabs x))))) *)
apply Rmult_lt_compat_l; auto with real zarith.
(* Goal: Rlt (IZR (Z.abs (Fnum x))) (powerRZ (IZR radix) (Z.of_nat (Fdigit radix (Fabs x)))) *)
rewrite <- Zpower_nat_Z_powerRZ; auto with arith.
(* Goal: Rlt (IZR (Z.abs (Fnum x))) (IZR (Zpower_nat radix (Fdigit radix (Fabs x)))) *)
apply Rlt_IZR.
(* Goal: Z.lt (Z.abs (Fnum x)) (Zpower_nat radix (Fdigit radix (Fabs x))) *)
unfold Fdigit in |- *; auto with arith.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
unfold Fabs in |- *; simpl in |- *.
pattern (Zabs (Fnum x)) at 1 in |- *; rewrite <- (Zabs_eq (Zabs (Fnum x)));
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
 auto with zarith.
Qed.
 
Theorem LSB_le_abs :
 forall x : float, ~ is_Fzero x -> (Float 1%nat (LSB x) <= Fabs x)%R.
(* Goal: forall (x : float) (_ : not (is_Fzero x)), Rle (FtoRradix (Float (Z.of_nat (S O)) (LSB x))) (FtoRradix (Fabs x)) *)
intros x H'; apply Rle_trans with (FtoRradix (Float 1%nat (MSB x))).
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fmult x y)))) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (Z.add (MSB x) (MSB y))))) *)
(* Goal: @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (Z.add (MSB x) (MSB y))))) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (Z.add (MSB x) (MSB y))))) *)
apply (oneExp_le radix); auto.
(* Goal: Z.le (LSB x) (MSB x) *)
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB x))) (FtoRradix (Fabs x)) *)
apply LSB_le_MSB; auto.
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB x))) (FtoRradix (Fabs x)) *)
apply MSB_le_abs; auto.
Qed.
 
Theorem MSB_monotoneAux :
 forall x y : float,
 (Fabs x <= Fabs y)%R -> Fexp x = Fexp y -> (MSB x <= MSB y)%Z.
(* Goal: forall (x y : float) (_ : Rle (FtoRradix (Fabs x)) (FtoRradix (Fabs y))) (_ : @eq Z (Fexp x) (Fexp y)), Z.le (MSB x) (MSB y) *)
intros x y H' H'0; unfold MSB in |- *.
(* Goal: Z.le (Z.pred (Z.add (Z.of_nat (Fdigit radix x)) (Fexp x))) (Z.pred (Z.add (Z.of_nat (Fdigit radix y)) (Fexp y))) *)
rewrite <- H'0.
cut (Fdigit radix x <= Fdigit radix y)%Z;
 [ unfold Zpred in |- *; auto with zarith | idtac ].
(* Goal: Z.le (Z.of_nat (Fdigit radix x)) (Z.of_nat (Fdigit radix y)) *)
unfold Fdigit in |- *; apply inj_le.
(* Goal: le (digit radix (Fnum x)) (digit radix (Fnum y)) *)
apply digit_monotone; auto.
(* Goal: Z.le (Z.abs (Fnum x)) (Z.abs (Fnum y)) *)
apply le_IZR.
apply Rmult_le_reg_l with (r := powerRZ radix (Fexp x));
 auto with real zarith.
(* Goal: Rle (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Z.abs (Fnum x)))) (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Z.abs (Fnum y)))) *)
repeat rewrite (Rmult_comm (powerRZ radix (Fexp x))); auto.
(* Goal: Rle (Rmult (IZR (Z.abs (Fnum x))) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Z.abs (Fnum y))) (powerRZ (IZR radix) (Fexp x))) *)
pattern (Fexp x) at 2 in |- *; rewrite H'0; auto.
Qed.
 
Theorem MSB_monotone :
 forall x y : float,
 ~ is_Fzero x -> ~ is_Fzero y -> (Fabs x <= Fabs y)%R -> (MSB x <= MSB y)%Z.
(* Goal: forall (x y : float) (_ : not (is_Fzero x)) (_ : not (is_Fzero y)) (_ : Rle (FtoRradix (Fabs x)) (FtoRradix (Fabs y))), Z.le (MSB x) (MSB y) *)
intros x y H' H'0 H'1; rewrite (MSB_abs x); rewrite (MSB_abs y).
(* Goal: Z.le (MSB (Fabs x)) (MSB (Fabs y)) *)
case (Zle_or_lt (Fexp (Fabs x)) (Fexp (Fabs y))); simpl in |- *; intros Zle1.
rewrite
 MSB_shift with (x := Fabs y) (n := Zabs_nat (Fexp (Fabs y) - Fexp (Fabs x))).
(* Goal: Z.le (MSB (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (MSB (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
apply MSB_monotoneAux; auto.
(* Goal: Rle (FtoRradix (Fabs (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x)))) (FtoRradix (Fabs (Fabs y))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (Fexp (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
unfold FtoRradix in |- *; repeat rewrite Fabs_correct; auto with real arith.
(* Goal: Rle (Rabs (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x)))) (Rabs (Rabs (FtoR radix y))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (Fexp (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
rewrite FshiftCorrect; auto with real arith.
(* Goal: Rle (Rabs (FtoR radix (Fabs x))) (Rabs (Rabs (FtoR radix y))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (Fexp (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
repeat rewrite Fabs_correct; auto with real arith.
repeat rewrite Rabs_Rabsolu; repeat rewrite <- Fabs_correct;
 auto with real arith.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq Z (Z.sub (Fexp x) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Fexp y))))) (Fexp y) *)
(* Goal: not (is_Fzero (Fabs x)) *)
rewrite inj_abs; [ ring | auto with zarith ].
(* Goal: not (is_Fzero (Fabs x)) *)
apply Fabs_Fzero; auto.
rewrite
 MSB_shift with (x := Fabs x) (n := Zabs_nat (Fexp (Fabs x) - Fexp (Fabs y))).
(* Goal: Z.le (MSB (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (MSB (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
apply MSB_monotoneAux; auto.
(* Goal: Rle (FtoRradix (Fabs (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x)))) (FtoRradix (Fabs (Fabs y))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (Fexp (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
unfold FtoRradix in |- *; repeat rewrite Fabs_correct; auto with real arith.
(* Goal: Rle (Rabs (FtoR radix (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x)))) (Rabs (Rabs (FtoR radix y))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (Fexp (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
rewrite FshiftCorrect; auto with real arith.
(* Goal: Rle (Rabs (FtoR radix (Fabs x))) (Rabs (Rabs (FtoR radix y))) *)
(* Goal: @eq Z (Fexp (Fshift radix (Z.abs_nat (Z.sub (Fexp (Fabs x)) (Fexp (Fabs y)))) (Fabs x))) (Fexp (Fabs y)) *)
(* Goal: not (is_Fzero (Fabs x)) *)
repeat rewrite Fabs_correct; auto with real arith.
repeat rewrite Rabs_Rabsolu; repeat rewrite <- Fabs_correct;
 auto with real arith.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
unfold Fshift in |- *; simpl in |- *.
(* Goal: @eq Z (Z.sub (Fexp x) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Fexp y))))) (Fexp y) *)
(* Goal: not (is_Fzero (Fabs x)) *)
rewrite inj_abs; [ ring | auto with zarith ].
(* Goal: not (is_Fzero (Fabs x)) *)
apply Fabs_Fzero; auto.
Qed.
 
Theorem MSB_le_multAux :
 forall x y : float,
 ~ is_Fzero x -> ~ is_Fzero y -> (MSB x + MSB y <= MSB (Fmult x y))%Z.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x y H' H'0; unfold MSB, Fmult, Fdigit in |- *; simpl in |- *.
replace
 (Zpred (digit radix (Fnum x) + Fexp x) +
  Zpred (digit radix (Fnum y) + Fexp y))%Z with
 (Zpred
    (digit radix (Fnum x) + Zpred (digit radix (Fnum y)) + (Fexp x + Fexp y)));
 [ idtac | unfold Zpred in |- *; ring ].
cut
 (digit radix (Fnum x) + Zpred (digit radix (Fnum y)) <=
  digit radix (Fnum x * Fnum y))%Z;
 [ unfold Zpred in |- *; auto with zarith | idtac ].
(* Goal: Z.le (Z.add (Z.of_nat (digit radix (Fnum x))) (Z.pred (Z.of_nat (digit radix (Fnum y))))) (Z.of_nat (digit radix (Z.mul (Fnum x) (Fnum y)))) *)
rewrite <- inj_pred; auto with float zarith; try rewrite <- inj_plus.
(* Goal: Z.le (Z.of_nat (Init.Nat.add (digit radix (Fnum x)) (Init.Nat.pred (digit radix (Fnum y))))) (Z.of_nat (digit radix (Z.mul (Fnum x) (Fnum y)))) *)
(* Goal: not (@eq nat (digit radix (Fnum y)) O) *)
apply inj_le.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite <- digitAdd; auto with zarith.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
apply digit_monotone; auto with zarith.
(* Goal: Z.le (Z.abs (Z.mul (Fnum x) (Fnum y))) (Z.abs (Z.mul (Fnum x) (Zpower_nat radix (digit radix (Fnum y))))) *)
repeat rewrite Zabs_Zmult.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
apply Zle_Zmult_comp_l; auto with zarith.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite (fun x => Zabs_eq (Zpower_nat radix x)); auto with zarith.
(* Goal: not (@eq nat (digit radix (Fnum y)) O) *)
apply not_eq_sym; apply lt_O_neq; apply digitNotZero; auto.
Qed.
 
Theorem MSB_le_mult :
 forall x y : float,
 ~ is_Fzero x ->
 ~ is_Fzero y ->
 (Fmult (Float 1%nat (MSB x)) (Float 1%nat (MSB y)) <=
  Float 1%nat (MSB (Fmult x y)))%R.
(* Goal: forall (x y : float) (_ : not (is_Fzero y)) (_ : Z.le (LSB x) (LSB y)), @ex Z (fun z : Z => @eq R (FtoRradix y) (FtoRradix (Float z (Fexp x)))) *)
intros x y H' H'0.
(* Goal: Rle (FtoRradix (Fmult (Float (Z.of_nat (S O)) (MSB x)) (Float (Z.of_nat (S O)) (MSB y)))) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fmult x y)))) *)
rewrite <- oneZplus.
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fmult x y)))) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (Z.add (MSB x) (MSB y))))) *)
(* Goal: @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (Z.add (MSB x) (MSB y))))) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (Z.add (MSB x) (MSB y))))) *)
apply (oneExp_le radix); auto.
(* Goal: Z.le (Z.add (MSB x) (MSB y)) (MSB (Fmult x y)) *)
apply MSB_le_multAux; auto.
Qed.
 
Theorem mult_le_MSBAux :
 forall x y : float,
 ~ is_Fzero x -> ~ is_Fzero y -> (MSB (Fmult x y) <= Zsucc (MSB x + MSB y))%Z.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
intros x y H' H'0; unfold MSB, Fmult, Fdigit in |- *; simpl in |- *.
replace
 (Zsucc
    (Zpred (digit radix (Fnum x) + Fexp x) +
     Zpred (digit radix (Fnum y) + Fexp y))) with
 (Zpred (digit radix (Fnum x) + digit radix (Fnum y) + (Fexp x + Fexp y)));
 [ idtac | unfold Zpred, Zsucc in |- *; ring ].
cut
 (digit radix (Fnum x * Fnum y) <=
  digit radix (Fnum x) + digit radix (Fnum y))%Z;
 [ unfold Zpred in |- *; auto with zarith | idtac ].
(* Goal: Z.le (Z.of_nat (digit radix (Z.mul (Fnum x) (Fnum y)))) (Z.add (Z.of_nat (digit radix (Fnum x))) (Z.of_nat (digit radix (Fnum y)))) *)
rewrite <- inj_plus.
(* Goal: Z.le (Z.of_nat (digit radix (Z.mul (Fnum x) (Fnum y)))) (Z.of_nat (Init.Nat.add (digit radix (Fnum x)) (digit radix (Fnum y)))) *)
apply inj_le; auto.
(* Goal: le (digit radix (Z.mul (Fnum x) (Fnum y))) (Init.Nat.add (digit radix (Fnum x)) (digit radix (Fnum y))) *)
rewrite <- digitAdd; auto with arith.
(* Goal: le (digit radix (Z.mul (Fnum x) (Fnum y))) (digit radix (Z.mul (Fnum x) (Zpower_nat radix (digit radix (Fnum y))))) *)
apply digit_monotone; auto with arith.
(* Goal: Z.le (Z.abs (Z.mul (Fnum x) (Fnum y))) (Z.abs (Z.mul (Fnum x) (Zpower_nat radix (digit radix (Fnum y))))) *)
repeat rewrite Zabs_Zmult.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
apply Zle_Zmult_comp_l; auto with zarith.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite (fun x => Zabs_eq (Zpower_nat radix x)); auto with zarith.
Qed.
 
Theorem mult_le_MSB :
 forall x y : float,
 ~ is_Fzero x ->
 ~ is_Fzero y ->
 (Float 1%nat (MSB (Fmult x y)) <=
  radix * Fmult (Float 1%nat (MSB x)) (Float 1%nat (MSB y)))%R.
(* Goal: Rle (FtoRradix (Fmult (Float (Z.of_nat (S O)) (MSB x)) (Float (Z.of_nat (S O)) (MSB y)))) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fmult x y)))) *)
intros x y H' H'0; rewrite <- oneZplus.
replace (radix * Float 1%nat (MSB x + MSB y))%R with
 (FtoRradix (Float 1%nat (Zsucc (MSB x + MSB y)))).
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fmult x y)))) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (Z.add (MSB x) (MSB y))))) *)
(* Goal: @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (Z.add (MSB x) (MSB y))))) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (Z.add (MSB x) (MSB y))))) *)
apply (oneExp_le radix); auto.
(* Goal: Z.le (MSB (Fmult x y)) (Z.succ (Z.add (MSB x) (MSB y))) *)
(* Goal: @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (Z.add (MSB x) (MSB y))))) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (Z.add (MSB x) (MSB y))))) *)
apply mult_le_MSBAux; auto.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.succ (MSB (Fabs x))))) (Rmult (IZR radix) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (MSB (Fabs x))))) *)
rewrite powerRZ_Zs; auto with real zarith; ring.
Qed.
 
Theorem MSB_mix :
 forall x y : float,
 ~ is_Fzero x ->
 ~ is_Fzero y ->
 (Fabs x * Float 1%nat (MSB y) < radix * (Fabs y * Float 1%nat (MSB x)))%R.
(* Goal: forall (x y : float) (_ : not (is_Fzero x)) (_ : not (is_Fzero y)), Rlt (Rmult (FtoRradix (Fabs x)) (FtoRradix (Float (Z.of_nat (S O)) (MSB y)))) (Rmult (IZR radix) (Rmult (FtoRradix (Fabs y)) (FtoRradix (Float (Z.of_nat (S O)) (MSB x))))) *)
intros x y H' H'0; rewrite (MSB_abs x); rewrite (MSB_abs y).
(* Goal: Rlt (Rmult (FtoRradix (Fabs x)) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs y))))) (Rmult (IZR radix) (Rmult (FtoRradix (Fabs y)) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x)))))) *)
apply Rle_lt_trans with (Fabs x * Fabs y)%R; auto with real.
(* Goal: Rle (Rmult (FtoRradix (Fabs x)) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs y))))) (Rmult (FtoRradix (Fabs x)) (FtoRradix (Fabs y))) *)
(* Goal: Rlt (Rmult (FtoRradix (Fabs x)) (FtoRradix (Fabs y))) (Rmult (IZR radix) (Rmult (FtoRradix (Fabs y)) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x)))))) *)
apply Rmult_le_compat_l; auto with real.
(* Goal: Rle (IZR Z0) (FtoRradix (Fabs x)) *)
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs y)))) (FtoRradix (Fabs y)) *)
(* Goal: Rlt (Rmult (FtoRradix (Fabs x)) (FtoRradix (Fabs y))) (Rmult (IZR radix) (Rmult (FtoRradix (Fabs y)) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x)))))) *)
unfold FtoRradix in |- *; rewrite Fabs_correct; auto with real arith.
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (MSB x))) (FtoRradix (Fabs x)) *)
rewrite <- MSB_abs; apply MSB_le_abs; auto.
(* Goal: Rlt (Rmult (FtoRradix (Fabs x)) (FtoRradix (Fabs y))) (Rmult (IZR radix) (Rmult (FtoRradix (Fabs y)) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x)))))) *)
rewrite (Rmult_comm (Fabs x)).
replace (radix * (Fabs y * Float 1%nat (MSB (Fabs x))))%R with
 (Fabs y * (radix * Float 1%nat (MSB (Fabs x))))%R; 
 [ idtac | ring ].
(* Goal: Rlt (Rmult (FtoRradix (Fabs y)) (FtoRradix (Fabs x))) (Rmult (FtoRradix (Fabs y)) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x)))))) *)
apply Rmult_lt_compat_l; auto with real.
(* Goal: Rlt (IZR Z0) (FtoRradix (Fabs y)) *)
(* Goal: Rlt (FtoRradix (Fabs x)) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x))))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real arith.
rewrite Rmult_comm; replace 0%R with (powerRZ radix (Fexp y) * 0)%R;
 [ idtac | ring ].
(* Goal: Rlt (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR Z0)) (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR (Z.abs (Fnum y)))) *)
(* Goal: Rlt (FtoRradix (Fabs x)) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x))))) *)
apply Rmult_lt_compat_l; auto with real arith.
(* Goal: Rlt (IZR Z0) (IZR (Z.abs (Fnum y))) *)
(* Goal: Rlt (FtoRradix (Fabs x)) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x))))) *)
rewrite Zabs_absolu.
replace 0%R with (INR 0); [ idtac | simpl in |- *; auto ];
 rewrite <- INR_IZR_INZ; apply INR_lt_nm.
(* Goal: lt O (Z.abs_nat (Fnum y)) *)
(* Goal: Rlt (FtoRradix (Fabs x)) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x))))) *)
apply absolu_lt_nz; auto.
replace (radix * Float 1%nat (MSB (Fabs x)))%R with
 (FtoRradix (Float 1%nat (Zsucc (MSB (Fabs x))))).
(* Goal: Rlt (FtoRradix (Fabs x)) (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (MSB (Fabs x))))) *)
(* Goal: @eq R (FtoRradix (Float (Z.of_nat (S O)) (Z.succ (MSB (Fabs x))))) (Rmult (IZR radix) (FtoRradix (Float (Z.of_nat (S O)) (MSB (Fabs x))))) *)
rewrite <- MSB_abs; apply abs_lt_MSB; auto.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Z.succ (MSB (Fabs x))))) (Rmult (IZR radix) (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (MSB (Fabs x))))) *)
rewrite powerRZ_Zs; auto with real zarith; ring.
Qed.
 
Theorem LSB_rep :
 forall x y : float,
 ~ is_Fzero y ->
 (LSB x <= LSB y)%Z -> exists z : Z, y = Float z (Fexp x) :>R.
(* Goal: forall (x y : float) (_ : not (is_Fzero y)) (_ : Z.le (LSB x) (LSB y)), @ex Z (fun z : Z => @eq R (FtoRradix y) (FtoRradix (Float z (Fexp x)))) *)
intros x y H' H'0.
(* Goal: @ex Z (fun z : Z => @eq R (FtoRradix y) (FtoRradix (Float z (Fexp x)))) *)
case (Zle_or_lt (Fexp x) (Fexp y)); intros Zl1.
(* Goal: @ex Z (fun z : Z => @eq R (FtoRradix y) (FtoRradix (Float z (Fexp x)))) *)
(* Goal: @ex Z (fun z : Z => @eq R (FtoRradix y) (FtoRradix (Float z (Fexp x)))) *)
exists (Fnum y * Zpower_nat radix (Zabs_nat (Fexp y - Fexp x)))%Z.
pattern (Fexp x) at 2 in |- *;
 replace (Fexp x) with (Fexp y - Zabs_nat (Fexp y - Fexp x))%Z.
unfold FtoRradix in |- *;
 rewrite <-
  (FshiftCorrect radix) with (n := Zabs_nat (Fexp y - Fexp x)) (x := y); 
 auto.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite inj_abs; try ring; auto with zarith.
(* Goal: @ex Z (fun z : Z => @eq R (FtoRradix y) (FtoRradix (Float z (Fexp x)))) *)
exists (Zquotient (Fnum y) (Zpower_nat radix (Zabs_nat (Fexp x - Fexp y)))).
unfold FtoRradix in |- *;
 rewrite <-
  (FshiftCorrect radix)
                        with
                        (n := Zabs_nat (Fexp x - Fexp y))
                       (x := 
                         Float
                           (Zquotient (Fnum y)
                              (Zpower_nat radix (Zabs_nat (Fexp x - Fexp y))))
                           (Fexp x)); auto.
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
unfold Fshift in |- *; simpl in |- *.
cut (0 <= Fexp x - Fexp y)%Z;
 [ intros Le1; repeat rewrite inj_abs | auto with zarith ]; 
 auto.
(* Goal: @eq nat p (maxDiv v (S (Init.Nat.add O p))) *)
(* Goal: forall (n : nat) (_ : @eq nat p (maxDiv v (S (Init.Nat.add n p)))), @eq nat p (maxDiv v (S (Init.Nat.add (S n) p))) *)
unfold FtoR in |- *; simpl in |- *; auto.
(* Goal: @eq R (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y))) (Rmult (IZR (Z.mul (Zquotient (Fnum y) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Fexp y))))) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Fexp y)))))) (powerRZ (IZR radix) (Z.sub (Fexp x) (Z.sub (Fexp x) (Fexp y))))) *)
replace (Fexp x - (Fexp x - Fexp y))%Z with (Fexp y); [ idtac | ring ].
replace
 (Zquotient (Fnum y) (Zpower_nat radix (Zabs_nat (Fexp x - Fexp y))) *
  Zpower_nat radix (Zabs_nat (Fexp x - Fexp y)))%Z with (
 Fnum y); auto.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
apply ZdividesZquotient; auto with zarith.
apply
 ZdividesTrans
  with (m := Zpower_nat radix (maxDiv (Fnum y) (Fdigit radix y))).
(* Goal: Zdivides (Fnum p) (Zpower_nat radix (maxDiv (Fnum p) (Fdigit radix p))) *)
(* Goal: @eq Z (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)) *)
apply maxDivCorrect.
(* Goal: Zdivides (Zpower_nat radix (maxDiv (Fnum y) (Fdigit radix y))) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Fexp y)))) *)
apply ZdividesLessPow; auto.
(* Goal: le (Z.abs_nat (Z.sub (Fexp x) (Fexp y))) (maxDiv (Fnum y) (Fdigit radix y)) *)
apply ZleLe.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite inj_abs; auto with zarith.
(* Goal: Z.le (Z.sub (Fexp x) (Fexp y)) (Z.of_nat (maxDiv (Fnum y) (Fdigit radix y))) *)
apply Zplus_le_reg_l with (p := Fexp y).
(* Goal: Z.le (Z.add (Fexp y) (Z.sub (Fexp x) (Fexp y))) (Z.add (Fexp y) (Z.of_nat (maxDiv (Fnum y) (Fdigit radix y)))) *)
apply Zle_trans with (LSB x).
(* Goal: Z.le (Z.add (Fexp y) (Z.sub (Fexp x) (Fexp y))) (LSB x) *)
(* Goal: Z.le (LSB x) (Z.add (Fexp y) (Z.of_nat (maxDiv (Fnum y) (Fdigit radix y)))) *)
replace (Fexp y + (Fexp x - Fexp y))%Z with (Fexp x); [ idtac | ring ].
(* Goal: Z.le (Fexp x) (LSB x) *)
(* Goal: Z.le (LSB x) (Z.add (Fexp y) (Z.of_nat (maxDiv (Fnum y) (Fdigit radix y)))) *)
apply Fexp_le_LSB.
(* Goal: Z.le (LSB x) (Z.add (Fexp y) (Z.of_nat (maxDiv (Fnum y) (Fdigit radix y)))) *)
rewrite Zplus_comm; auto.
Qed.
 
Theorem LSB_rep_min :
 forall p : float, exists z : Z, p = Float z (LSB p) :>R.
intros p;
 exists (Zquotient (Fnum p) (Zpower_nat radix (Zabs_nat (LSB p - Fexp p)))).
(* Goal: forall _ : @eq nat p (maxDiv v (S p)), False *)
unfold FtoRradix, FtoR, LSB in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Zquotient (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)))))) (powerRZ (IZR radix) (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)))) *)
rewrite powerRZ_add; auto with real zarith.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Zquotient (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)))))) (Rmult (powerRZ (IZR radix) (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p)))) (powerRZ (IZR radix) (Fexp p)))) *)
rewrite <- Rmult_assoc.
replace (maxDiv (Fnum p) (Fdigit radix p) + Fexp p - Fexp p)%Z with
 (Z_of_nat (maxDiv (Fnum p) (Fdigit radix p))); auto.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (Rmult (IZR (Zquotient (Fnum p) (Zpower_nat radix (Z.abs_nat (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))))))) (powerRZ (IZR radix) (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)) *)
rewrite absolu_INR.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite <- Zpower_nat_Z_powerRZ; auto with zarith.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (Rmult (Rmult (IZR (Zquotient (Fnum p) (Zpower_nat radix (maxDiv (Fnum p) (Fdigit radix p))))) (IZR (Zpower_nat radix (maxDiv (Fnum p) (Fdigit radix p))))) (powerRZ (IZR radix) (Fexp p))) *)
(* Goal: @eq Z (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)) *)
rewrite <- Rmult_IZR.
(* Goal: Z.le (Fexp x) (Z.add (Z.of_nat (maxDiv (Fnum x) (Fdigit radix x))) (Fexp x)) *)
rewrite <- ZdividesZquotient; auto with zarith.
(* Goal: Zdivides (Fnum p) (Zpower_nat radix (maxDiv (Fnum p) (Fdigit radix p))) *)
(* Goal: @eq Z (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)) *)
apply maxDivCorrect.
(* Goal: @eq Z (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Z.sub (Z.add (Z.of_nat (maxDiv (Fnum p) (Fdigit radix p))) (Fexp p)) (Fexp p)) *)
ring.
Qed.
End mf.