(****************************************************************************
                                                                             
          IEEE754  :  Finduct                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  *****************************************************************************
  Define an induction principle on float*)
Require Export FPred.
Section finduct.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionNotZero : precision <> 0.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Definition Fweight (p : float) :=
  (Fnum p + Fexp p * Zpower_nat radix precision)%Z.
 
Theorem FweightLt :
 forall p q : float,
 Fcanonic radix b p ->
 Fcanonic radix b q -> (0 <= p)%R -> (p < q)%R -> (Fweight p < Fweight q)%Z.
(* Goal: forall (p q : float) (_ : Fcanonic radix b p) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Rlt (FtoRradix p) (FtoRradix q)), Z.lt (Fweight p) (Fweight q) *)
intros p q H' H'0 H'1 H'2.
(* Goal: Z.lt (Fweight p) (Fweight q) *)
cut (Fbounded b p); [ intros Fb1 | apply FcanonicBound with (1 := H') ]; auto.
cut (Fbounded b q); [ intros Fb2 | apply FcanonicBound with (1 := H'0) ];
 auto.
case (FcanonicLtPos _ radixMoreThanOne b precision) with (p := p) (q := q);
 auto with arith; intros Zl1.
(* Goal: Z.lt (Fweight p) (Fweight q) *)
unfold Fweight in |- *; simpl in |- *.
(* Goal: Z.lt (Z.add (Fnum p) (Z.mul (Fexp p) (Zpower_nat radix precision))) (Z.add (Fnum q) (Z.mul (Fexp q) (Zpower_nat radix precision))) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
replace (Fexp q) with (Fexp q - Fexp p + Fexp p)%Z; [ idtac | ring ].
(* Goal: Z.lt (Z.add (Fnum p) (Z.mul (Fexp p) (Zpower_nat radix precision))) (Z.add (Fnum q) (Z.mul (Z.add (Z.sub (Fexp q) (Fexp p)) (Fexp p)) (Zpower_nat radix precision))) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
rewrite Zmult_plus_distr_l.
(* Goal: Z.lt (Z.add (Fnum p) (Z.mul (Fexp p) (Zpower_nat radix precision))) (Z.add (Fnum q) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Z.mul (Fexp p) (Zpower_nat radix precision)))) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
rewrite Zplus_assoc.
(* Goal: Z.lt (Z.add (Fnum p) (Z.mul (Fexp p) (Zpower_nat radix precision))) (Z.add (Fnum q) (Z.mul (Fexp p) (Zpower_nat radix precision))) *)
repeat rewrite (fun x y z : Z => Zplus_comm x (y * z)).
(* Goal: Z.lt (Z.add (Z.mul (Fexp p) (Zpower_nat radix precision)) (Fnum p)) (Z.add (Z.mul (Fexp p) (Zpower_nat radix precision)) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q))) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply Zplus_lt_compat_l.
(* Goal: Z.lt (Fnum p) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q)) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply Zlt_le_trans with (Zpower_nat radix precision); auto with zarith.
apply Zle_lt_trans with (Zpred (Zpower_nat radix precision));
 auto with zarith.
(* Goal: Z.le (Fnum p) (Z.pred (Zpower_nat radix precision)) *)
(* Goal: Z.le (Zpower_nat radix precision) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q)) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply Zle_Zabs_inv2; auto with float zarith.
(* Goal: Z.le (Z.abs (Fnum p)) (Z.pred (Zpower_nat radix precision)) *)
(* Goal: Z.le (Zpower_nat radix precision) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q)) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply Zle_Zpred; auto with float zarith.
(* Goal: Z.lt (Z.abs (Fnum p)) (Zpower_nat radix precision) *)
(* Goal: Z.le (Zpower_nat radix precision) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q)) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
rewrite <- pGivesBound; auto with float.
apply Zle_trans with ((Fexp q - Fexp p) * Zpower_nat radix precision)%Z;
 auto with zarith.
pattern (Zpower_nat radix precision) at 1 in |- *;
 replace (Zpower_nat radix precision) with
  (Zsucc 0 * Zpower_nat radix precision)%Z; auto.
(* Goal: Z.le (Z.mul (Z.succ Z0) (Zpower_nat radix precision)) (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) *)
(* Goal: @eq Z (Z.mul (Z.succ Z0) (Zpower_nat radix precision)) (Zpower_nat radix precision) *)
(* Goal: Z.le (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q)) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply Zle_Zmult_comp_r; auto with zarith.
(* Goal: @eq Z (Z.mul (Z.succ Z0) (Zpower_nat radix precision)) (Zpower_nat radix precision) *)
(* Goal: Z.le (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q)) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
unfold Zsucc in |- *; ring.
(* Goal: Z.le (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Z.add (Z.mul (Z.sub (Fexp q) (Fexp p)) (Zpower_nat radix precision)) (Fnum q)) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
cut (0 <= Fnum q)%Z; auto with zarith.
(* Goal: Z.le Z0 (Fnum q) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply (LeR0Fnum radix); auto.
(* Goal: Rle (IZR Z0) (FtoR radix q) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply Rle_trans with (FtoRradix p); auto; apply Rlt_le; auto.
(* Goal: Z.lt (Fweight p) (Fweight q) *)
elim Zl1; intros H'3 H'4; clear Zl1.
(* Goal: Z.lt (Fweight p) (Fweight q) *)
unfold Fweight in |- *; simpl in |- *.
(* Goal: Z.lt (Z.add (Fnum p) (Z.mul (Fexp p) (Zpower_nat radix precision))) (Z.add (Fnum q) (Z.mul (Fexp q) (Zpower_nat radix precision))) *)
rewrite <- H'3.
(* Goal: Z.lt (Z.add (Fnum p) (Z.mul (Fexp p) (Zpower_nat radix precision))) (Z.add (Fnum q) (Z.mul (Fexp p) (Zpower_nat radix precision))) *)
repeat rewrite (fun x y z : Z => Zplus_comm x (y * z)).
(* Goal: Z.lt (Z.add (Z.mul (Fexp p) (Zpower_nat radix precision)) (Fnum p)) (Z.add (Z.mul (Fexp p) (Zpower_nat radix precision)) (Fnum q)) *)
apply Zplus_lt_compat_l; auto.
Qed.
 
Theorem FweightEq :
 forall p q : float,
 Fcanonic radix b p ->
 Fcanonic radix b q -> p = q :>R -> Fweight p = Fweight q.
(* Goal: forall (p q : float) (_ : Fcanonic radix b p) (_ : Fcanonic radix b q) (_ : @eq R (FtoRradix p) (FtoRradix q)), @eq Z (Fweight p) (Fweight q) *)
intros p q H' H'0 H'1.
rewrite
 (FcanonicUnique _ radixMoreThanOne b precision) with (p := p) (q := q);
 auto with arith.
Qed.
 
Theorem FweightZle :
 forall p q : float,
 Fcanonic radix b p ->
 Fcanonic radix b q -> (0 <= p)%R -> (p <= q)%R -> (Fweight p <= Fweight q)%Z.
(* Goal: forall (p q : float) (_ : Fcanonic radix b p) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Rle (FtoRradix p) (FtoRradix q)), Z.le (Fweight p) (Fweight q) *)
intros p q H' H'0 H'1 H'2; Casec H'2; intros H'2.
(* Goal: Z.le (Fweight p) (Fweight q) *)
(* Goal: Z.le (Fweight p) (Fweight q) *)
apply Zlt_le_weak.
(* Goal: Z.lt (Fweight p) (Fweight q) *)
(* Goal: Z.le (Fweight p) (Fweight q) *)
apply FweightLt; auto.
(* Goal: Z.le (Fweight p) (Fweight q) *)
rewrite (FweightEq p q); auto with zarith.
Qed.
 
Theorem FinductPosAux :
 forall (P : float -> Prop) (p : float),
 (0 <= p)%R ->
 Fcanonic radix b p ->
 P p ->
 (forall q : float,
  Fcanonic radix b q -> (p <= q)%R -> P q -> P (FSucc b radix precision q)) ->
 forall x : Z,
 (0 <= x)%Z ->
 forall q : float,
 x = (Fweight q - Fweight p)%Z -> Fcanonic radix b q -> (p <= q)%R -> P q.
(* Goal: forall (P : forall _ : float, Prop) (p : float) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Fcanonic radix b p) (_ : P p) (_ : forall (q : float) (_ : Fcanonic radix b q) (_ : Rlt (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)) (_ : P q), P (FPred b radix precision q)) (x : Z) (_ : Z.le Z0 x) (q : float) (_ : @eq Z x (Z.sub (Fweight p) (Fweight q))) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)), P q *)
intros P p H' H'0 H'1 H'2 x H'3; pattern x in |- *.
(* Goal: (fun z : Z => forall (q : float) (_ : @eq Z z (Z.sub (Fweight p) (Fweight q))) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)), P q) x *)
apply Z_lt_induction; auto.
(* Goal: forall (x : Z) (_ : forall (y : Z) (_ : and (Z.le Z0 y) (Z.lt y x)) (q : float) (_ : @eq Z y (Z.sub (Fweight q) (Fweight p))) (_ : Fcanonic radix b q) (_ : Rle (FtoRradix p) (FtoRradix q)), P q) (q : float) (_ : @eq Z x (Z.sub (Fweight q) (Fweight p))) (_ : Fcanonic radix b q) (_ : Rle (FtoRradix p) (FtoRradix q)), P q *)
intros x0 H'4 q H'5 H'6 H'7.
(* Goal: P q *)
Casec H'7; intros H'7.
(* Goal: P q *)
(* Goal: P q *)
cut (p <= FPred b radix precision q)%R; [ intros Rl1 | idtac ].
(* Goal: P q *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
cut (P (FPred b radix precision q)); [ intros P1 | idtac ].
(* Goal: P q *)
(* Goal: P (FPred b radix precision q) *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
rewrite <- (FSucPred b radix precision) with (x := q); auto with arith.
(* Goal: P (FPred b radix precision (FSucc b radix precision q)) *)
(* Goal: P (FSucc b radix precision q) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply H'2; auto with float arith.
apply H'4 with (y := (Fweight (FPred b radix precision q) - Fweight p)%Z);
 auto.
(* Goal: and (Z.le Z0 (Z.sub (Fweight p) (Fweight (FSucc b radix precision q)))) (Z.lt (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) x0) *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
split.
(* Goal: Z.le Z0 (Z.sub (Fweight (FPred b radix precision q)) (Fweight p)) *)
(* Goal: Z.lt (Z.sub (Fweight (FPred b radix precision q)) (Fweight p)) x0 *)
(* Goal: Fcanonic radix b (FPred b radix precision q) *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
cut (Fweight p <= Fweight (FPred b radix precision q))%Z; auto with zarith.
(* Goal: Z.le (Fweight (FSucc b radix precision q)) (Fweight p) *)
(* Goal: Z.lt (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) x0 *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply FweightZle; auto.
(* Goal: Fcanonic radix b (FPred b radix precision q) *)
(* Goal: Z.lt (Z.sub (Fweight (FPred b radix precision q)) (Fweight p)) x0 *)
(* Goal: Fcanonic radix b (FPred b radix precision q) *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
apply FPredCanonic; auto with arith.
(* Goal: Z.lt (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) x0 *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
rewrite H'5.
cut (Fweight (FPred b radix precision q) < Fweight q)%Z;
 [ auto with zarith | idtac ].
(* Goal: Z.lt (Fweight q) (Fweight (FSucc b radix precision q)) *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply FweightLt; auto with float.
(* Goal: Rle (IZR Z0) (FtoRradix (FPred b radix precision q)) *)
(* Goal: Rlt (FtoRradix (FPred b radix precision q)) (FtoRradix q) *)
(* Goal: Fcanonic radix b (FPred b radix precision q) *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
apply (R0RltRlePred b radix precision); auto.
(* Goal: Rlt (IZR Z0) (FtoR radix q) *)
(* Goal: Rlt (FtoRradix (FPred b radix precision q)) (FtoRradix q) *)
(* Goal: Fcanonic radix b (FPred b radix precision q) *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
apply Rle_lt_trans with (FtoRradix p); auto.
(* Goal: Rlt (FtoRradix (FPred b radix precision q)) (FtoRradix q) *)
(* Goal: Fcanonic radix b (FPred b radix precision q) *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
apply (FPredLt b radix precision); auto.
(* Goal: Fcanonic radix b (FPred b radix precision q) *)
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
apply (FPredCanonic b radix precision); auto with arith.
(* Goal: Rle (FtoRradix p) (FtoRradix (FPred b radix precision q)) *)
(* Goal: P q *)
apply (FPredProp b radix precision); auto with arith.
rewrite <-
 (FcanonicUnique _ radixMoreThanOne b precision) with (p := p) (q := q);
 auto with arith.
Qed.
 
Theorem FinductPos :
 forall (P : float -> Prop) (p : float),
 (0 <= p)%R ->
 Fcanonic radix b p ->
 P p ->
 (forall q : float,
  Fcanonic radix b q -> (p <= q)%R -> P q -> P (FSucc b radix precision q)) ->
 forall q : float, Fcanonic radix b q -> (p <= q)%R -> P q.
(* Goal: forall (P : forall _ : float, Prop) (p : float) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Fcanonic radix b p) (_ : P p) (_ : forall (q : float) (_ : Fcanonic radix b q) (_ : Rle (FtoRradix p) (FtoRradix q)) (_ : P q), P (FSucc b radix precision q)) (q : float) (_ : Fcanonic radix b q) (_ : Rle (FtoRradix p) (FtoRradix q)), P q *)
intros P p H' H'0 H'1 H'2 q H'3 H'4.
(* Goal: P q *)
apply FinductPosAux with (p := p) (x := (Fweight q - Fweight p)%Z); auto.
(* Goal: Z.le Z0 (Z.sub (Fweight q) (Fweight p)) *)
cut (Fweight p <= Fweight q)%Z; [ auto with zarith | idtac ].
(* Goal: Z.le (Fweight q) (Fweight p) *)
apply FweightZle; auto with float.
Qed.
 
Theorem FinductNegAux :
 forall (P : float -> Prop) (p : float),
 (0 <= p)%R ->
 Fcanonic radix b p ->
 P p ->
 (forall q : float,
  Fcanonic radix b q ->
  (0 < q)%R -> (q <= p)%R -> P q -> P (FPred b radix precision q)) ->
 forall x : Z,
 (0 <= x)%Z ->
 forall q : float,
 x = (Fweight p - Fweight q)%Z ->
 Fcanonic radix b q -> (0 <= q)%R -> (q <= p)%R -> P q.
(* Goal: forall (P : forall _ : float, Prop) (p : float) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Fcanonic radix b p) (_ : P p) (_ : forall (q : float) (_ : Fcanonic radix b q) (_ : Rlt (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)) (_ : P q), P (FPred b radix precision q)) (x : Z) (_ : Z.le Z0 x) (q : float) (_ : @eq Z x (Z.sub (Fweight p) (Fweight q))) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)), P q *)
intros P p H' H'0 H'1 H'2 x H'3; pattern x in |- *.
(* Goal: (fun z : Z => forall (q : float) (_ : @eq Z z (Z.sub (Fweight p) (Fweight q))) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)), P q) x *)
apply Z_lt_induction; auto.
(* Goal: forall (x : Z) (_ : forall (y : Z) (_ : and (Z.le Z0 y) (Z.lt y x)) (q : float) (_ : @eq Z y (Z.sub (Fweight p) (Fweight q))) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)), P q) (q : float) (_ : @eq Z x (Z.sub (Fweight p) (Fweight q))) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)), P q *)
intros x0 H'4 q H'5 H'6 H'7 H'8.
(* Goal: P q *)
Casec H'8; intros H'8.
(* Goal: P q *)
(* Goal: P q *)
cut (FSucc b radix precision q <= p)%R; [ intros Rle1 | idtac ].
(* Goal: P q *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
cut (P (FSucc b radix precision q)); [ intros P1 | idtac ].
(* Goal: P q *)
(* Goal: P (FSucc b radix precision q) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
rewrite <- (FPredSuc b radix precision) with (x := q); auto with arith.
(* Goal: P (FPred b radix precision (FSucc b radix precision q)) *)
(* Goal: P (FSucc b radix precision q) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply H'2; auto with float arith.
(* Goal: Rlt (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: P (FSucc b radix precision q) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply Rle_lt_trans with (FtoRradix q); auto.
(* Goal: Rlt (FtoRradix q) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply (FSuccLt b radix); auto with arith.
apply H'4 with (y := (Fweight p - Fweight (FSucc b radix precision q))%Z);
 auto.
(* Goal: and (Z.le Z0 (Z.sub (Fweight p) (Fweight (FSucc b radix precision q)))) (Z.lt (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) x0) *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
split.
(* Goal: Z.le Z0 (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) *)
(* Goal: Z.lt (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) x0 *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
cut (Fweight (FSucc b radix precision q) <= Fweight p)%Z; auto with zarith.
(* Goal: Z.le (Fweight (FSucc b radix precision q)) (Fweight p) *)
(* Goal: Z.lt (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) x0 *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply FweightZle; auto.
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply FSuccCanonic; auto with arith.
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply Rle_trans with (FtoRradix q); auto; apply Rlt_le.
(* Goal: Rlt (FtoRradix q) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply (FSuccLt b radix); auto with arith.
(* Goal: Z.lt (Z.sub (Fweight p) (Fweight (FSucc b radix precision q))) x0 *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
rewrite H'5.
cut (Fweight q < Fweight (FSucc b radix precision q))%Z;
 [ auto with zarith | idtac ].
(* Goal: Z.lt (Fweight q) (Fweight (FSucc b radix precision q)) *)
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply FweightLt; auto with float.
(* Goal: Rlt (FtoRradix q) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply (FSuccLt b radix); auto with arith.
(* Goal: Fcanonic radix b (FSucc b radix precision q) *)
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply FSuccCanonic; auto with arith.
(* Goal: Rle (IZR Z0) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply Rle_trans with (FtoRradix q); auto; apply Rlt_le.
(* Goal: Rlt (FtoRradix q) (FtoRradix (FSucc b radix precision q)) *)
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply (FSuccLt b radix); auto with arith.
(* Goal: Rle (FtoRradix (FSucc b radix precision q)) (FtoRradix p) *)
(* Goal: P q *)
apply (FSuccProp b radix); auto with arith.
rewrite <-
 (FcanonicUnique _ radixMoreThanOne b precision) with (p := p) (q := q);
 auto with arith.
Qed.
 
Theorem FinductNeg :
 forall (P : float -> Prop) (p : float),
 (0 <= p)%R ->
 Fcanonic radix b p ->
 P p ->
 (forall q : float,
  Fcanonic radix b q ->
  (0 < q)%R -> (q <= p)%R -> P q -> P (FPred b radix precision q)) ->
 forall q : float, Fcanonic radix b q -> (0 <= q)%R -> (q <= p)%R -> P q.
(* Goal: forall (P : forall _ : float, Prop) (p : float) (_ : Rle (IZR Z0) (FtoRradix p)) (_ : Fcanonic radix b p) (_ : P p) (_ : forall (q : float) (_ : Fcanonic radix b q) (_ : Rlt (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)) (_ : P q), P (FPred b radix precision q)) (q : float) (_ : Fcanonic radix b q) (_ : Rle (IZR Z0) (FtoRradix q)) (_ : Rle (FtoRradix q) (FtoRradix p)), P q *)
intros P p H' H'0 H'1 H'2 q H'3 H'4 H'5.
(* Goal: P q *)
apply FinductNegAux with (p := p) (x := (Fweight p - Fweight q)%Z); auto.
(* Goal: Z.le Z0 (Z.sub (Fweight p) (Fweight q)) *)
cut (Fweight q <= Fweight p)%Z; [ auto with zarith | idtac ].
(* Goal: Z.le (Fweight q) (Fweight p) *)
apply FweightZle; auto with float.
Qed.
 
Theorem radixRangeBoundExp :
 forall p q : float,
 Fcanonic radix b p ->
 Fcanonic radix b q ->
 (0 <= p)%R ->
 (p < q)%R -> (q < radix * p)%R -> Fexp p = Fexp q \/ Zsucc (Fexp p) = Fexp q.
intros p q H' H'0 H'1 H'2 H'3.
case (FcanonicLtPos _ radixMoreThanOne b precision) with (p := p) (q := q);
 auto with arith.
2: intros H'4; elim H'4; intros H'5 H'6; clear H'4; auto.
intros H'4; right.
Casec H'; intros H'.
case
 (FcanonicLtPos _ radixMoreThanOne b precision)
  with (p := q) (q := Float (Fnum p) (Zsucc (Fexp p))); 
 auto with arith.
left.
case H'; intros H1 H2; red in H1.
repeat split; simpl in |- *; auto with float.
apply Zle_trans with (Fexp p); auto with float zarith.
(* Goal: Rle (IZR Z0) (FtoR radix q) *)
(* Goal: Z.lt (Fweight p) (Fweight q) *)
apply Rle_trans with (FtoRradix p); auto; apply Rlt_le; auto.
unfold FtoR in |- *; simpl in |- *.
rewrite powerRZ_Zs; auto with real zarith; auto.
rewrite <- Rmult_assoc;
 rewrite (fun (x : R) (y : Z) => Rmult_comm x y); 
 rewrite Rmult_assoc; auto.
simpl in |- *; intros; apply Zle_antisym; auto with zarith.
simpl in |- *; auto.
intros H'5; elim H'5; intros H'6 H'7; auto.
case
 (FcanonicLtPos _ radixMoreThanOne b precision)
  with (p := q) (q := Float (nNormMin radix precision) (Zsucc (Fexp p)));
 auto with arith.
left; repeat split; simpl in |- *.
rewrite Zabs_eq; auto with zarith.
apply ZltNormMinVnum; auto with zarith.
unfold nNormMin in |- *; auto with zarith.
apply Zle_trans with (Fexp p); auto with float zarith.
case H'; auto with float.
rewrite <- (PosNormMin radix b precision); auto with zarith.
apply Rle_trans with (1 := H'1); auto with real.
apply Rlt_trans with (1 := H'3).
unfold FtoR in |- *; simpl in |- *.
rewrite powerRZ_Zs; auto with real zarith; auto.
rewrite <- Rmult_assoc;
 rewrite (fun (x : R) (y : Z) => Rmult_comm x y); 
 rewrite Rmult_assoc; auto.
apply Rmult_lt_compat_l; auto with real arith.
case H'.
intros H'5 H'6; elim H'6; intros H'7 H'8; rewrite H'7; clear H'6.
change (p < firstNormalPos radix b precision)%R in |- *.
apply (FsubnormalLtFirstNormalPos radix); auto with arith.
simpl in |- *; intros; apply Zle_antisym; auto with zarith.
intros H'5; elim H'5; intros H'6 H'7; rewrite H'6; clear H'5; auto.
Qed.
End finduct.