(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2011-2013 Sylvie Boldo
#<br />#
Copyright (C) 2011-2013 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** * IEEE-754 encoding of binary floating-point data *)
Require Import Fcore.
Require Import Fcore_digits.
Require Import Fcalc_digits.
Require Import Fappli_IEEE.

Section Binary_Bits.

Arguments exist {A P} x _.
Arguments B754_zero {prec emax} _.
Arguments B754_infinity {prec emax} _.
Arguments B754_nan {prec emax} _ _.
Arguments B754_finite {prec emax} _ m e _.

(** Number of bits for the fraction and exponent *)
Variable mw ew : Z.
Hypothesis Hmw : (0 < mw)%Z.
Hypothesis Hew : (0 < ew)%Z.

Let emax := Zpower 2 (ew - 1).
Let prec := (mw + 1)%Z.
Let emin := (3 - emax - prec)%Z.
Let binary_float := binary_float prec emax.

Let Hprec : (0 < prec)%Z.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
unfold prec.
(* Goal: Z.lt Z0 (Z.add mw (Zpos xH)) *)
apply Zle_lt_succ.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
Qed.

Let Hm_gt_0 : (0 < 2^mw)%Z.
(* Goal: Z.lt Z0 (Z.pow (Zpos (xO xH)) ew) *)
apply (Zpower_gt_0 radix2).
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
Qed.

Let He_gt_0 : (0 < 2^ew)%Z.
(* Goal: Z.lt Z0 (Z.pow (Zpos (xO xH)) ew) *)
apply (Zpower_gt_0 radix2).
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
Qed.

Hypothesis Hmax : (prec < emax)%Z.

Definition join_bits (s : bool) m e :=
  (Z.shiftl ((if s then Zpower 2 ew else 0) + e) mw + m)%Z.

Lemma join_bits_range :
  forall s m e,
  (0 <= m < 2^mw)%Z ->
  (0 <= e < 2^ew)%Z ->
  (0 <= join_bits s m e < 2 ^ (mw + ew + 1))%Z.
Proof.
(* Goal: forall (s : bool) (m e : Z) (_ : and (Z.le Z0 m) (Z.lt m (Z.pow (Zpos (xO xH)) mw))) (_ : and (Z.le Z0 e) (Z.lt e (Z.pow (Zpos (xO xH)) ew))), @eq (prod (prod bool Z) Z) (split_bits (join_bits s m e)) (@pair (prod bool Z) Z (@pair bool Z s m) e) *)
intros s m e Hm He.
(* Goal: and (Z.le Z0 (join_bits s m e)) (Z.lt (join_bits s m e) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
unfold join_bits.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
split.
- apply (Zplus_le_compat 0 _ 0) with (2 := proj1 Hm).
  rewrite <- (Zmult_0_l (2^mw)).
(* Goal: Z.le (Z.mul (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Zpos xH)) (Z.pow (Zpos (xO xH)) mw)) (Z.mul (Z.pow (Zpos (xO xH)) (Z.add ew (Zpos xH))) (Z.pow (Zpos (xO xH)) mw)) *)
(* Goal: Z.le Z0 (Z.add ew (Zpos xH)) *)
(* Goal: Z.le Z0 mw *)
  apply Zmult_le_compat_r.
(* Goal: @eq Z (Z.modulo (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
  case s.
  clear -He ; omega.
(* Goal: Z.le Z0 (Z.add (Z.mul Z0 (Z.pow (Zpos (xO xH)) mw)) e) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
  now rewrite Zmult_0_l.
  clear -Hm ; omega.
- apply Zlt_le_trans with (((if s then 2 ^ ew else 0) + e + 1) * 2 ^ mw)%Z.
(* Goal: Z.lt (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.mul (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Zpos xH)) (Z.pow (Zpos (xO xH)) mw)) *)
(* Goal: Z.le (Z.mul (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Zpos xH)) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH))) *)
  rewrite (Zmult_plus_distr_l _ 1).
(* Goal: Z.lt (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) (Z.mul (Zpos xH) (Z.pow (Zpos (xO xH)) mw))) *)
(* Goal: Z.le (Z.mul (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Zpos xH)) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH))) *)
  apply Zplus_lt_compat_l.
(* Goal: Z.le (Z.mul (Zpos xH) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) x *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
  now rewrite Zmult_1_l.
  rewrite <- (Zplus_assoc mw), (Zplus_comm mw), Zpower_plus.
(* Goal: Z.le (Z.mul (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Zpos xH)) (Z.pow (Zpos (xO xH)) mw)) (Z.mul (Z.pow (Zpos (xO xH)) (Z.add ew (Zpos xH))) (Z.pow (Zpos (xO xH)) mw)) *)
(* Goal: Z.le Z0 (Z.add ew (Zpos xH)) *)
(* Goal: Z.le Z0 mw *)
  apply Zmult_le_compat_r.
(* Goal: Z.le (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.add ew (Zpos xH))) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.add ew (Zpos xH)) *)
(* Goal: Z.le Z0 mw *)
  rewrite Zpower_plus.
(* Goal: Z.lt (Z.add (Z.sub ex (Z.sub (Z.sub (Zpos (xI xH)) (Z.pow (Zpos (xO xH)) (Z.sub ew (Zpos xH)))) prec)) (Zpos xH)) (Z.mul (Z.pow (Zpos (xO xH)) (Z.sub ew (Zpos xH))) (Z.pow (Zpos (xO xH)) (Zpos xH))) *)
  change (2^1)%Z with 2%Z.
  case s ; clear -He ; omega.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
  now apply Zlt_le_weak.
(* Goal: Z.le Z0 (Zpos pl) *)
(* Goal: Z.lt (Zpos pl) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: and (Z.le Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) (Z.lt (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
  easy.
  clear -Hm ; omega.
  clear -Hew ; omega.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
  now apply Zlt_le_weak.
Qed.

Definition split_bits x :=
  let mm := Zpower 2 mw in
  let em := Zpower 2 ew in
  (Zle_bool (mm * em) x, Zmod x mm, Zmod (Zdiv x mm) em)%Z.

Theorem split_join_bits :
  forall s m e,
  (0 <= m < Zpower 2 mw)%Z ->
  (0 <= e < Zpower 2 ew)%Z ->
  split_bits (join_bits s m e) = (s, m, e).
Proof.
(* Goal: forall (s : bool) (m e : Z) (_ : and (Z.le Z0 m) (Z.lt m (Z.pow (Zpos (xO xH)) mw))) (_ : and (Z.le Z0 e) (Z.lt e (Z.pow (Zpos (xO xH)) ew))), @eq (prod (prod bool Z) Z) (split_bits (join_bits s m e)) (@pair (prod bool Z) Z (@pair bool Z s m) e) *)
intros s m e Hm He.
(* Goal: let 'pair (pair s m as p) e := split_bits x in @eq Z (join_bits s m e) x *)
unfold split_bits, join_bits.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
(* Goal: @eq (prod bool Z) (@pair bool Z (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m)) (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw))) (@pair bool Z s m) *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply f_equal2.
(* Goal: @eq (prod bool Z) (@pair bool Z (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m)) (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw))) (@pair bool Z s m) *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply f_equal2.
(* *)
(* Goal: @eq Z (Z.modulo (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
case s.
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add (Z.pow (Zpos (xO xH)) ew) e) (Z.pow (Zpos (xO xH)) mw)) m)) true *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Zle_bool_true.
(* Goal: Z.le (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add (Z.pow (Zpos (xO xH)) ew) e) (Z.pow (Zpos (xO xH)) mw)) m) *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Zle_0_minus_le.
(* Goal: Z.le Z0 (Z.sub (Z.add (Z.mul (Z.add (Z.pow (Zpos (xO xH)) ew) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
ring_simplify.
(* Goal: Z.le Z0 (Z.add (Z.mul e (Z.pow (Zpos (xO xH)) mw)) m) *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Zplus_le_0_compat.
(* Goal: Z.le Z0 (Z.mul e (Z.pow (Zpos (xO xH)) mw)) *)
(* Goal: Z.le Z0 m *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Zmult_le_0_compat.
(* Goal: Z.le Z0 e *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 m *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply He.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
(* Goal: Z.le Z0 m *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Hm.
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Zle_bool_false.
apply Zplus_lt_reg_l with (2^mw * (-e))%Z.
replace (2 ^ mw * - e + ((0 + e) * 2 ^ mw + m))%Z with (m * 1)%Z by ring.
rewrite <- Zmult_plus_distr_r.
(* Goal: Z.lt (Z.mul m (Zpos xH)) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Zlt_le_trans with (2^mw * 1)%Z.
(* Goal: Z.lt (Z.mul m (Zpos xH)) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Zpos xH)) *)
(* Goal: Z.le (Z.mul (Z.pow (Zpos (xO xH)) mw) (Zpos xH)) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
now apply Zmult_lt_compat_r.
(* Goal: Z.le (Z.mul (Z.pow (Zpos (xO xH)) mw) (Zpos xH)) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Zmult_le_compat_l.
clear -He. omega.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
(* *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
rewrite Zplus_comm.
(* Goal: @eq Z (Z.modulo (Z.add e (Z.mul (Zpos xH) (Z.pow (Zpos (xO xH)) ew))) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: @eq Z (Z.modulo (Z.add Z0 e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Z_mod_plus_full.
(* Goal: @eq Z (Z.modulo (Z.add Z0 e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zmod_small.
(* *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
rewrite Z_div_plus_full_l.
(* Goal: @eq Z (Z.modulo (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.div m (Z.pow (Zpos (xO xH)) mw))) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Zdiv_small with (1 := Hm).
(* Goal: @eq Z (Z.modulo (Z.add (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) Z0) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Zplus_0_r.
(* Goal: @eq Z (Z.modulo (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
case s.
(* Goal: @eq Z (Z.modulo (Z.add (Z.pow (Zpos (xO xH)) ew) e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: @eq Z (Z.modulo (Z.add Z0 e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
replace (2^ew + e)%Z with (e + 1 * 2^ew)%Z by ring.
(* Goal: @eq Z (Z.modulo (Z.add e (Z.mul (Zpos xH) (Z.pow (Zpos (xO xH)) ew))) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: @eq Z (Z.modulo (Z.add Z0 e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Z_mod_plus_full.
(* Goal: @eq Z (Z.modulo (Z.add Z0 e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zmod_small.
(* Goal: @eq Z (Z.modulo (Z.add Z0 e) (Z.pow (Zpos (xO xH)) ew)) e *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zmod_small.
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zgt_not_eq.
Qed.

Theorem join_split_bits :
  forall x,
  (0 <= x < Zpower 2 (mw + ew + 1))%Z ->
  let '(s, m, e) := split_bits x in
  join_bits s m e = x.
Proof.
(* Goal: forall (x : Z) (_ : and (Z.le Z0 x) (Z.lt x (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH))))), @eq Z (bits_of_binary_float (binary_float_of_bits x)) x *)
intros x Hx.
(* Goal: let 'pair (pair s m as p) e := split_bits x in @eq Z (join_bits s m e) x *)
unfold split_bits, join_bits.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak.
(* Goal: @eq Z (Z.add (Z.mul (Z.add (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) (Z.pow (Zpos (xO xH)) mw)) (Z.modulo x (Z.pow (Zpos (xO xH)) mw))) x *)
pattern x at 4 ; rewrite Z_div_mod_eq_full with x (2^mw)%Z.
(* Goal: @eq Z (Z.add (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) (Z.add (Z.mul (Z.pow (Zpos (xO xH)) ew) (Z.div (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply (f_equal (fun v => (v + _)%Z)).
(* Goal: @eq Z (Z.mul (Z.add (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) (Z.pow (Zpos (xO xH)) mw)) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.div x (Z.pow (Zpos (xO xH)) mw))) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Zmult_comm.
(* Goal: @eq Z (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.add (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)))) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.div x (Z.pow (Zpos (xO xH)) mw))) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply f_equal.
(* Goal: @eq Z (Z.add (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) (Z.div x (Z.pow (Zpos (xO xH)) mw)) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
pattern (x / (2^mw))%Z at 2 ; rewrite Z_div_mod_eq_full with (x / (2^mw))%Z (2^ew)%Z.
(* Goal: @eq Z (Z.add (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) (Z.add (Z.mul (Z.pow (Zpos (xO xH)) ew) (Z.div (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply (f_equal (fun v => (v + _)%Z)).
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.mul (Z.pow (Zpos (xO xH)) ew) (Z.div (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
replace (x / 2 ^ mw / 2 ^ ew)%Z with (if Zle_bool (2 ^ mw * 2 ^ ew) x then 1 else 0)%Z.
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.mul (Z.pow (Zpos (xO xH)) ew) (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0)) *)
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
case Zle_bool.
(* Goal: @eq Z (Z.pow (Zpos (xO xH)) ew) (Z.mul (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) *)
(* Goal: @eq Z Z0 (Z.mul (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now rewrite Zmult_1_r.
(* Goal: @eq Z Z0 (Z.mul (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now rewrite Zmult_0_r.
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Zdiv_Zdiv.
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply sym_eq.
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
case Zle_bool_spec ; intros Hs.
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) (Zpos xH) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply Zle_antisym.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
cut (x / (2^mw * 2^ew) < 2)%Z. clear ; omega.
(* Goal: Z.lt (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply Zdiv_lt_upper_bound.
(* Goal: Z.lt Z0 (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le (Z.mul (Zpos xH) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) x *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
try apply Hx. (* 8.2/8.3 compatibility *)
(* Goal: Z.lt Z0 (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le (Z.mul (Zpos xH) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) x *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zmult_lt_0_compat.
rewrite <- Zpower_exp ; try ( apply Zle_ge ; apply Zlt_le_weak ; assumption ).
(* Goal: Z.lt x (Z.mul (Zpos (xO xH)) (Z.pow (Zpos (xO xH)) (Z.add mw ew))) *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
change 2%Z at 1 with (Zpower 2 1).
rewrite <- Zpower_exp.
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
now rewrite Zplus_comm.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
discriminate.
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply Zle_ge.
(* Goal: Z.le Z0 (Z.add mw ew) *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zplus_le_0_compat ; apply Zlt_le_weak.
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply Zdiv_le_lower_bound.
(* Goal: Z.lt Z0 (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le (Z.mul (Zpos xH) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) x *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
try apply Hx. (* 8.2/8.3 compatibility *)
(* Goal: Z.lt Z0 (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le (Z.mul (Zpos xH) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) x *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zmult_lt_0_compat.
(* Goal: Z.le (Z.mul (Zpos xH) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) x *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now rewrite Zmult_1_l.
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply Zdiv_small.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
now split.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zgt_not_eq.
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zgt_not_eq.
Qed.

Theorem split_bits_inj :
  forall x y,
  (0 <= x < Zpower 2 (mw + ew + 1))%Z ->
  (0 <= y < Zpower 2 (mw + ew + 1))%Z ->
  split_bits x = split_bits y ->
  x = y.
Proof.
(* Goal: forall (x y : Z) (_ : and (Z.le Z0 x) (Z.lt x (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH))))) (_ : and (Z.le Z0 y) (Z.lt y (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH))))) (_ : @eq (prod (prod bool Z) Z) (split_bits x) (split_bits y)), @eq Z x y *)
intros x y Hx Hy.
(* Goal: forall _ : @eq (prod (prod bool Z) Z) (split_bits x) (split_bits y), @eq Z x y *)
generalize (join_split_bits x Hx) (join_split_bits y Hy).
(* Goal: forall (_ : let 'pair (pair s m as p) e := split_bits x in @eq Z (join_bits s m e) x) (_ : let 'pair (pair s m as p) e := split_bits y in @eq Z (join_bits s m e) y) (_ : @eq (prod (prod bool Z) Z) (split_bits x) (split_bits y)), @eq Z x y *)
destruct (split_bits x) as ((sx, mx), ex).
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : let 'pair (pair s m as p) e := split_bits y in @eq Z (join_bits s m e) y) (_ : @eq (prod (prod bool Z) Z) (@pair (prod bool Z) Z (@pair bool Z sx mx) ex) (split_bits y)), @eq Z x y *)
destruct (split_bits y) as ((sy, my), ey).
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq Z (join_bits sy my ey) y) (_ : @eq (prod (prod bool Z) Z) (@pair (prod bool Z) Z (@pair bool Z sx mx) ex) (@pair (prod bool Z) Z (@pair bool Z sy my) ey)), @eq Z x y *)
intros Jx Jy H. revert Jx Jy.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq Z (join_bits sy my ey) y), @eq Z x y *)
inversion_clear H.
(* Goal: forall (_ : @eq Z (join_bits sy my ey) x) (_ : @eq Z (join_bits sy my ey) y), @eq Z x y *)
intros Jx Jy.
now rewrite <- Jx.
Qed.

Definition bits_of_binary_float (x : binary_float) :=
  match x with
  | B754_zero sx => join_bits sx 0 0
  | B754_infinity sx => join_bits sx 0 (Zpower 2 ew - 1)
  | B754_nan sx (exist plx _) => join_bits sx (Zpos plx) (Zpower 2 ew - 1)
  | B754_finite sx mx ex _ =>
    let m := (Zpos mx - Zpower 2 mw)%Z in
    if Zle_bool 0 m then
      join_bits sx m (ex - emin + 1)
    else
      join_bits sx (Zpos mx) 0
  end.

Definition split_bits_of_binary_float (x : binary_float) :=
  match x with
  | B754_zero sx => (sx, 0, 0)%Z
  | B754_infinity sx => (sx, 0, Zpower 2 ew - 1)%Z
  | B754_nan sx (exist plx _) => (sx, Zpos plx, Zpower 2 ew - 1)%Z
  | B754_finite sx mx ex _ =>
    let m := (Zpos mx - Zpower 2 mw)%Z in
    if Zle_bool 0 m then
      (sx, m, ex - emin + 1)%Z
    else
      (sx, Zpos mx, 0)%Z
  end.

Theorem split_bits_of_binary_float_correct :
  forall x,
  split_bits (bits_of_binary_float x) = split_bits_of_binary_float x.
Proof.
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] ;
  try ( simpl ; apply split_join_bits ; split ; try apply Zle_refl ; try apply Zlt_pred ; trivial ; omega ).
simpl. apply split_join_bits; split; try (zify; omega).
destruct (digits2_Pnat_correct plx).
rewrite Zpos_digits2_pos, <- Z_of_nat_S_digits2_Pnat in Hplx.
rewrite Zpower_nat_Z in H0.
eapply Zlt_le_trans. apply H0.
change 2%Z with (radix_val radix2). apply Zpower_le.
rewrite Z.ltb_lt in Hplx.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
unfold prec in *. zify; omega.
(* *)
unfold bits_of_binary_float, split_bits_of_binary_float.
assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z).
destruct (andb_prop _ _ Hx) as (Hx', _).
unfold canonic_mantissa in Hx'.
rewrite Zpos_digits2_pos in Hx'.
generalize (Zeq_bool_eq _ _ Hx').
unfold FLT_exp.
unfold emin.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
clear ; zify ; omega.
case Zle_bool_spec ; intros H ;
  [ apply -> Z.le_0_sub in H | apply -> Z.lt_sub_0 in H ] ;
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
  apply split_join_bits ; try now split.
(* *)
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
split.
clear -He_gt_0 H ; omega.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
cut (Zpos mx < 2 * 2^mw)%Z. clear ; omega.
replace (2 * 2^mw)%Z with (2^prec)%Z.
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
apply Hf.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
unfold prec.
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
rewrite Zplus_comm.
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply Zpower_exp ; apply Zle_ge.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
discriminate.
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
(* *)
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
split.
generalize (proj1 Hf).
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
clear ; omega.
destruct (andb_prop _ _ Hx) as (_, Hx').
unfold emin.
replace (2^ew)%Z with (2 * emax)%Z.
generalize (Zle_bool_imp_le _ _ Hx').
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
clear ; omega.
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply sym_eq.
rewrite (Zsucc_pred ew).
unfold Zsucc.
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
rewrite Zplus_comm.
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply Zpower_exp ; apply Zle_ge.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
discriminate.
now apply Zlt_0_le_0_pred.
Qed.

Theorem bits_of_binary_float_range:
  forall x, (0 <= bits_of_binary_float x < 2^(mw+ew+1))%Z.
Proof.
(* Goal: forall x : binary_float, and (Z.le Z0 (bits_of_binary_float x)) (Z.lt (bits_of_binary_float x) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
unfold bits_of_binary_float.
(* Goal: forall x : binary_float, and (Z.le Z0 match x with | B754_zero sx => join_bits sx Z0 Z0 | B754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_nan sx (exist plx e as n) => join_bits sx (Zpos plx) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_finite sx mx ex e => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end) (Z.lt match x with | B754_zero sx => join_bits sx Z0 Z0 | B754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_nan sx (exist plx e as n) => join_bits sx (Zpos plx) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_finite sx mx ex e => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
intros [sx|sx|sx [pl pl_range]|sx mx ex H].
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
- apply join_bits_range ; now split.
- apply join_bits_range.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
  now split.
  clear -He_gt_0 ; omega.
- apply Z.ltb_lt in pl_range.
(* Goal: and (Z.le Z0 (join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)))) (Z.lt (join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH))) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
  apply join_bits_range.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
  split.
(* Goal: Z.le Z0 (Zpos pl) *)
(* Goal: Z.lt (Zpos pl) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: and (Z.le Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) (Z.lt (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
  easy.
(* Goal: Z.lt (Zpos pl) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: and (Z.le Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) (Z.lt (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
  apply (Zpower_gt_Zdigits radix2 _ (Zpos pl)).
(* Goal: Z.le (Zdigits radix2 (Zpos pl)) mw *)
(* Goal: and (Z.le Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) (Z.lt (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
  apply Z.lt_succ_r.
  now rewrite <- Zdigits2_Zdigits.
  clear -He_gt_0 ; omega.
- unfold bounded in H.
(* Goal: and (Z.le Z0 (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0)) (Z.lt (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
  apply Bool.andb_true_iff in H ; destruct H as [A B].
(* Goal: and (Z.le Z0 (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0)) (Z.lt (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
  apply Z.leb_le in B.
(* Goal: and (Z.le Z0 (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0)) (Z.lt (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
  unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A.
(* Goal: and (Z.le Z0 (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0)) (Z.lt (if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
  case Zle_bool_spec ; intros H.
(* Goal: and (Z.le Z0 (join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)))) (Z.lt (join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH))) (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH)))) *)
  + apply join_bits_range.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
    * split.
      clear -H ; omega.
(* Goal: Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
      rewrite Zpos_digits2_pos in A.
(* Goal: Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
      cut (Zpos mx < 2 ^ prec)%Z.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
      unfold prec.
      rewrite Zpower_plus by (clear -Hmw ; omega).
(* Goal: Z.lt (Z.add (Z.sub ex (Z.sub (Z.sub (Zpos (xI xH)) (Z.pow (Zpos (xO xH)) (Z.sub ew (Zpos xH)))) prec)) (Zpos xH)) (Z.mul (Z.pow (Zpos (xO xH)) (Z.sub ew (Zpos xH))) (Z.pow (Zpos (xO xH)) (Zpos xH))) *)
      change (2^1)%Z with 2%Z.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
      clear ; omega.
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
      apply (Zpower_gt_Zdigits radix2 _ (Zpos mx)).
      clear -A ; zify ; omega.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
    * split.
      unfold emin ; clear -A ; zify ; omega.
      replace ew with ((ew - 1) + 1)%Z by ring.
      rewrite Zpower_plus by (clear - Hew ; omega).
      unfold emin, emax in *.
(* Goal: Z.lt (Z.add (Z.sub ex (Z.sub (Z.sub (Zpos (xI xH)) (Z.pow (Zpos (xO xH)) (Z.sub ew (Zpos xH)))) prec)) (Zpos xH)) (Z.mul (Z.pow (Zpos (xO xH)) (Z.sub ew (Zpos xH))) (Z.pow (Zpos (xO xH)) (Zpos xH))) *)
      change (2^1)%Z with 2%Z.
      clear -B ; omega.
  + apply -> Z.lt_sub_0 in H.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
    apply join_bits_range ; now split.
Qed.

Definition binary_float_of_bits_aux x :=
  let '(sx, mx, ex) := split_bits x in
  if Zeq_bool ex 0 then
    match mx with
    | Z0 => F754_zero sx
    | Zpos px => F754_finite sx px emin
    | Zneg _ => F754_nan false xH (* dummy *)
    end
  else if Zeq_bool ex (Zpower 2 ew - 1) then
    match mx with
      | Z0 => F754_infinity sx
      | Zpos plx => F754_nan sx plx
      | Zneg _ => F754_nan false xH (* dummy *)
    end
  else
    match (mx + Zpower 2 mw)%Z with
    | Zpos px => F754_finite sx px (ex + emin - 1)
    | _ => F754_nan false xH (* dummy *)
    end.

Lemma binary_float_of_bits_aux_correct :
  forall x,
  valid_binary prec emax (binary_float_of_bits_aux x) = true.
Proof.
intros x.
unfold binary_float_of_bits_aux, split_bits.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
case Zeq_bool_spec ; intros He1.
(* Goal: Z.le Z0 (Zpos pl) *)
(* Goal: Z.lt (Zpos pl) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: and (Z.le Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) (Z.lt (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
case_eq (x mod 2^mw)%Z ; try easy.
(* subnormal *)
intros px Hm.
assert (Zdigits radix2 (Zpos px) <= mw)%Z.
apply Zdigits_le_Zpower.
simpl.
rewrite <- Hm.
eapply Z_mod_lt.
(* Goal: Z.gt (Z.pow (Zpos (xO xH)) mw) Z0 *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now apply Zlt_gt.
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exp.
fold emin.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply sym_eq.
apply Zmax_right.
clear -H Hprec.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
unfold prec ; omega.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold emin, prec.
apply Zlt_not_le.
cut (0 < emax)%Z. clear -H Hew ; omega.
(* Goal: Z.lt Z0 (Z.pow (Zpos (xO xH)) ew) *)
apply (Zpower_gt_0 radix2).
clear -Hew ; omega.
apply bpow_gt_0.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
case Zeq_bool_spec ; intros He2.
(* Goal: Z.le Z0 (Zpos pl) *)
(* Goal: Z.lt (Zpos pl) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: and (Z.le Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) (Z.lt (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
case_eq (x mod 2 ^ mw)%Z; try easy.
(* nan *)
intros plx Eqplx. apply Z.ltb_lt.
rewrite Zpos_digits2_pos.
assert (forall a b, a <= b -> a < b+1)%Z by (intros; omega). apply H. clear H.
apply Zdigits_le_Zpower. simpl.
rewrite <- Eqplx. edestruct Z_mod_lt; eauto.
change 2%Z with (radix_val radix2).
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
apply Z.lt_gt, Zpower_gt_0. omega.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
(* Goal: Z.le Z0 (Zpos pl) *)
(* Goal: Z.lt (Zpos pl) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: and (Z.le Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) (Z.lt (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
case_eq (x mod 2^mw + 2^mw)%Z ; try easy.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
(* normal *)
intros px Hm.
assert (prec = Zdigits radix2 (Zpos px)).
(* . *)
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Zdigits_ln_beta. 2: discriminate.
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply sym_eq.
apply ln_beta_unique.
rewrite <- Z2R_abs.
unfold Zabs.
replace (prec - 1)%Z with mw by ( unfold prec ; ring ).
rewrite <- Z2R_Zpower with (1 := Zlt_le_weak _ _ Hmw).
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite <- Z2R_Zpower. 2: now apply Zlt_le_weak.
rewrite <- Hm.
(* Goal: and (Z.le Z0 (Z.add (Z.sub ex emin) (Zpos xH))) (Z.lt (Z.add (Z.sub ex emin) (Zpos xH)) (Z.pow (Zpos (xO xH)) ew)) *)
split.
apply Z2R_le.
change (radix2^mw)%Z with (0 + 2^mw)%Z.
apply Zplus_le_compat_r.
eapply Z_mod_lt.
(* Goal: Z.gt (Z.pow (Zpos (xO xH)) mw) Z0 *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now apply Zlt_gt.
apply Z2R_lt.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
unfold prec.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite Zpower_exp. 2: now apply Zle_ge ; apply Zlt_le_weak. 2: discriminate.
rewrite <- Zplus_diag_eq_mult_2.
apply Zplus_lt_compat_r.
eapply Z_mod_lt.
(* Goal: Z.gt (Z.pow (Zpos (xO xH)) mw) Z0 *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now apply Zlt_gt.
(* . *)
apply bounded_canonic_lt_emax ; try assumption.
unfold canonic, canonic_exp.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
unfold Fexp, FLT_exp.
rewrite <- H.
set (ex := ((x / 2^mw) mod 2^ew)%Z).
replace (prec + (ex + emin - 1) - prec)%Z with (ex + emin - 1)%Z by ring.
(* Goal: @eq Z (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Zpos xH else Z0) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply sym_eq.
apply Zmax_left.
revert He1.
fold ex.
cut (0 <= ex)%Z.
unfold emin.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
clear ; intros H1 H2 ; omega.
eapply Z_mod_lt.
apply Zlt_gt.
(* Goal: Z.lt Z0 (Z.pow (Zpos (xO xH)) ew) *)
apply (Zpower_gt_0 radix2).
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
apply Rnot_le_lt.
intros H0.
refine (_ (ln_beta_le radix2 _ _ _ H0)).
rewrite ln_beta_bpow.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
rewrite <- H.
apply Zlt_not_le.
unfold emin.
apply Zplus_lt_reg_r with (emax - 1)%Z.
(* Goal: Z.le Z0 (Z.sub (Z.add (Z.mul (Z.add (Z.pow (Zpos (xO xH)) ew) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
ring_simplify.
revert He2.
set (ex := ((x / 2^mw) mod 2^ew)%Z).
cut (ex < 2^ew)%Z.
replace (2^ew)%Z with (2 * emax)%Z.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
clear ; intros H1 H2 ; omega.
replace ew with (1 + (ew - 1))%Z by ring.
rewrite Zpower_exp.
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
apply refl_equal.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
discriminate.
clear -Hew ; omega.
eapply Z_mod_lt.
apply Zlt_gt.
(* Goal: Z.lt Z0 (Z.pow (Zpos (xO xH)) ew) *)
apply (Zpower_gt_0 radix2).
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
now apply Zlt_le_weak.
apply bpow_gt_0.
(* Goal: forall _ : Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec), Z.lt (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.lt (Zpos mx) (Z.pow (Zpos (xO xH)) prec) *)
simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega.
Qed.

Definition binary_float_of_bits x :=
  FF2B prec emax _ (binary_float_of_bits_aux_correct x).

Theorem binary_float_of_bits_of_binary_float :
  forall x,
  binary_float_of_bits (bits_of_binary_float x) = x.
Proof.
intros x.
apply B2FF_inj.
unfold binary_float_of_bits.
rewrite B2FF_FF2B.
(* Goal: forall (_ : let 'pair (pair s m as p) e := split_bits x in @eq Z (join_bits s m e) x) (_ : @eq bool (valid_binary prec emax (binary_float_of_bits_aux x)) true), @eq Z match binary_float_of_bits_aux x with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
unfold binary_float_of_bits_aux.
rewrite split_bits_of_binary_float_correct.
destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Bx].
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
apply refl_equal.
(* *)
simpl.
rewrite Zeq_bool_false.
now rewrite Zeq_bool_true.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
cut (1 < 2^ew)%Z. clear ; omega.
now apply (Zpower_gt_1 radix2).
(* *)
simpl.
rewrite Zeq_bool_false.
rewrite Zeq_bool_true; auto.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
cut (1 < 2^ew)%Z. clear ; omega.
now apply (Zpower_gt_1 radix2).
(* *)
unfold split_bits_of_binary_float.
case Zle_bool_spec ; intros Hm.
(* . *)
rewrite Zeq_bool_false.
rewrite Zeq_bool_false.
now ring_simplify (Zpos mx - 2 ^ mw + 2 ^ mw)%Z (ex - emin + 1 + emin - 1)%Z.
destruct (andb_prop _ _ Bx) as (_, H1).
generalize (Zle_bool_imp_le _ _ H1).
unfold emin.
replace (2^ew)%Z with (2 * emax)%Z.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
clear ; omega.
replace ew with (1 + (ew - 1))%Z by ring.
rewrite Zpower_exp.
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
apply refl_equal.
(* Goal: Z.ge (Zpos xH) Z0 *)
(* Goal: Z.ge (Z.add mw ew) Z0 *)
(* Goal: Z.le (Zpos xH) (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq Z (Z.div x (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) Z0 *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) ew) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) ew) Z0) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
discriminate.
clear -Hew ; omega.
destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Zpos_digits2_pos.
unfold FLT_exp, emin.
generalize (Zdigits radix2 (Zpos mx)).
clear.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
intros ; zify ; omega.
(* . *)
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
rewrite Zeq_bool_true. 2: apply refl_equal.
simpl.
(* Goal: @eq Z (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.add (if Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) x then Z.pow (Zpos (xO xH)) ew else Z0) (Z.modulo (Z.div x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)))) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.div x (Z.pow (Zpos (xO xH)) mw))) *)
(* Goal: not (@eq Z (Z.pow (Zpos (xO xH)) mw) Z0) *)
apply f_equal.
destruct (andb_prop _ _ Bx) as (H1, _).
generalize (Zeq_bool_eq _ _ H1).
rewrite Zpos_digits2_pos.
unfold FLT_exp, emin, prec.
apply -> Z.lt_sub_0 in Hm.
generalize (Zdigits_le_Zpower radix2 _ (Zpos mx) Hm).
generalize (Zdigits radix2 (Zpos mx)).
clear.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
intros ; zify ; omega.
Qed.

Theorem bits_of_binary_float_of_bits :
  forall x,
  (0 <= x < 2^(mw+ew+1))%Z ->
  bits_of_binary_float (binary_float_of_bits x) = x.
Proof.
(* Goal: forall (x : Z) (_ : and (Z.le Z0 x) (Z.lt x (Z.pow (Zpos (xO xH)) (Z.add (Z.add mw ew) (Zpos xH))))), @eq Z (bits_of_binary_float (binary_float_of_bits x)) x *)
intros x Hx.
(* Goal: @eq Z (bits_of_binary_float (binary_float_of_bits x)) x *)
unfold binary_float_of_bits, bits_of_binary_float.
(* Goal: @eq Z match FF2B prec emax (binary_float_of_bits_aux x) (binary_float_of_bits_aux_correct x) with | B754_zero sx => join_bits sx Z0 Z0 | B754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_nan sx (exist plx e as n) => join_bits sx (Zpos plx) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_finite sx mx ex e => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
set (Cx := binary_float_of_bits_aux_correct x).
(* Goal: @eq Z match FF2B prec emax (binary_float_of_bits_aux x) Cx with | B754_zero sx => join_bits sx Z0 Z0 | B754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_nan sx (exist plx e as n) => join_bits sx (Zpos plx) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_finite sx mx ex e => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
clearbody Cx.
(* Goal: @eq Z match FF2B prec emax (binary_float_of_bits_aux x) Cx with | B754_zero sx => join_bits sx Z0 Z0 | B754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_nan sx (exist plx e as n) => join_bits sx (Zpos plx) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | B754_finite sx mx ex e => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
rewrite match_FF2B.
(* Goal: @eq Z match binary_float_of_bits_aux x with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
revert Cx.
(* Goal: forall _ : @eq bool (valid_binary prec emax (binary_float_of_bits_aux x)) true, @eq Z match binary_float_of_bits_aux x with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
generalize (join_split_bits x Hx).
(* Goal: forall (_ : let 'pair (pair s m as p) e := split_bits x in @eq Z (join_bits s m e) x) (_ : @eq bool (valid_binary prec emax (binary_float_of_bits_aux x)) true), @eq Z match binary_float_of_bits_aux x with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
unfold binary_float_of_bits_aux.
(* Goal: forall (_ : let 'pair (pair s m as p) e := split_bits x in @eq Z (join_bits s m e) x) (_ : @eq bool (valid_binary prec emax (let 'pair (pair sx mx as p) ex := split_bits x in if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p0 => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p0 => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p0 => F754_nan false xH end)) true), @eq Z match (let 'pair (pair sx mx as p) ex := split_bits x in if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p0 => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p0 => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p0 => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
case_eq (split_bits x).
(* Goal: forall (p : prod bool Z) (z : Z) (_ : @eq (prod (prod bool Z) Z) (split_bits x) (@pair (prod bool Z) Z p z)) (_ : let 'pair s m := p in @eq Z (join_bits s m z) x) (_ : @eq bool (valid_binary prec emax (let 'pair sx mx := p in if Zeq_bool z Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p0 => F754_nan false xH end else if Zeq_bool z (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p0 => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add z emin) (Zpos xH)) | Zneg p0 => F754_nan false xH end)) true), @eq Z match (let 'pair sx mx := p in if Zeq_bool z Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p0 => F754_nan false xH end else if Zeq_bool z (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p0 => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add z emin) (Zpos xH)) | Zneg p0 => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p0 => join_bits b (Zpos p0) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
intros (sx, mx) ex Sx.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
assert (Bm: (0 <= mx < 2^mw)%Z).
(* Goal: and (Z.le Z0 mx) (Z.lt mx (Z.pow (Zpos (xO xH)) mw)) *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
inversion_clear Sx.
(* Goal: and (Z.le Z0 (Z.modulo x (Z.pow (Zpos (xO xH)) mw))) (Z.lt (Z.modulo x (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw)) *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
apply Z_mod_lt.
(* Goal: Z.gt (Z.pow (Zpos (xO xH)) mw) Z0 *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now apply Zlt_gt.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex Z0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end else if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
case Zeq_bool_spec ; intros He1.
(* subnormal *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end) true), @eq Z match match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg p => F754_nan false xH end with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
case_eq mx.
(* Goal: forall (_ : @eq Z mx Z0) (_ : @eq Z (join_bits sx Z0 ex) x) (_ : @eq bool (valid_binary prec emax (F754_zero sx)) true), @eq Z (join_bits sx Z0 Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z mx (Zpos p)) (_ : @eq Z (join_bits sx (Zpos p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_finite sx p emin)) true), @eq Z (if Z.leb Z0 (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub emin emin) (Zpos xH)) else join_bits sx (Zpos p) Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z mx (Zneg p)) (_ : @eq Z (join_bits sx (Zneg p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
intros Hm Jx _.
(* Goal: @eq Z (join_bits sx Z0 Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z mx (Zpos p)) (_ : @eq Z (join_bits sx (Zpos p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_finite sx p emin)) true), @eq Z (if Z.leb Z0 (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub emin emin) (Zpos xH)) else join_bits sx (Zpos p) Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z mx (Zneg p)) (_ : @eq Z (join_bits sx (Zneg p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now rewrite He1 in Jx.
(* Goal: forall (p : positive) (_ : @eq Z mx (Zpos p)) (_ : @eq Z (join_bits sx (Zpos p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_finite sx p emin)) true), @eq Z (if Z.leb Z0 (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub emin emin) (Zpos xH)) else join_bits sx (Zpos p) Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z mx (Zneg p)) (_ : @eq Z (join_bits sx (Zneg p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
intros px Hm Jx _.
(* Goal: @eq Z (if Z.leb Z0 (Z.sub (Zpos px) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos px) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub emin emin) (Zpos xH)) else join_bits sx (Zpos px) Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z mx (Zneg p)) (_ : @eq Z (join_bits sx (Zneg p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
rewrite Zle_bool_false.
now rewrite <- He1.
apply <- Z.lt_sub_0.
now rewrite <- Hm.
(* Goal: forall (p : positive) (_ : @eq Z mx (Zneg p)) (_ : @eq Z (join_bits sx (Zneg p) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
intros px Hm _ _.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
apply False_ind.
(* Goal: False *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
apply Zle_not_lt with (1 := proj1 Bm).
(* Goal: Z.lt mx Z0 *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now rewrite Hm.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end)) true), @eq Z match (if Zeq_bool ex (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end else match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
case Zeq_bool_spec ; intros He2.
(* infinity/nan *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end) true), @eq Z match match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg p => F754_nan false xH end with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) true), @eq Z match match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
case_eq mx; intros Hm.
(* Goal: forall (_ : @eq Z mx (Zpos Hm)) (_ : @eq Z (join_bits sx (Zpos Hm) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan sx Hm)) true), @eq Z (join_bits sx (Zpos Hm) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z mx (Zneg Hm)) (_ : @eq Z (join_bits sx (Zneg Hm) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) true), @eq Z match match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now rewrite He2.
(* Goal: forall (_ : @eq Z mx (Zpos Hm)) (_ : @eq Z (join_bits sx (Zpos Hm) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan sx Hm)) true), @eq Z (join_bits sx (Zpos Hm) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z mx (Zneg Hm)) (_ : @eq Z (join_bits sx (Zneg Hm) ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end) true), @eq Z match match Z.add mx (Z.pow (Zpos (xO xH)) mw) with | Z0 => F754_nan false xH | Zpos px => F754_finite sx px (Z.sub (Z.add ex emin) (Zpos xH)) | Zneg p => F754_nan false xH end with | F754_zero sx => join_bits sx Z0 Z0 | F754_infinity sx => join_bits sx Z0 (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_nan b p => join_bits b (Zpos p) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH)) | F754_finite sx mx ex => if Z.leb Z0 (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos mx) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub ex emin) (Zpos xH)) else join_bits sx (Zpos mx) Z0 end x *)
now rewrite He2.
(* Goal: Z.le (Zpos xH) (Z.add (Z.opp e) (Z.pow (Zpos (xO xH)) ew)) *)
(* Goal: Z.le Z0 (Z.pow (Zpos (xO xH)) mw) *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
intros. zify; omega.
(* normal *)
case_eq (mx + 2 ^ mw)%Z.
(* Goal: forall (_ : @eq Z (Z.add mx (Z.pow (Zpos (xO xH)) mw)) Z0) (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Zpos p)) (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_finite sx p (Z.sub (Z.add ex emin) (Zpos xH)))) true), @eq Z (if Z.leb Z0 (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub (Z.sub (Z.add ex emin) (Zpos xH)) emin) (Zpos xH)) else join_bits sx (Zpos p) Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Zneg p)) (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
intros Hm.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
apply False_ind.
clear -Bm Hm ; omega.
(* Goal: forall (p : positive) (_ : @eq Z (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Zpos p)) (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_finite sx p (Z.sub (Z.add ex emin) (Zpos xH)))) true), @eq Z (if Z.leb Z0 (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Zpos p) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub (Z.sub (Z.add ex emin) (Zpos xH)) emin) (Zpos xH)) else join_bits sx (Zpos p) Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Zneg p)) (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
intros p Hm Jx Cx.
rewrite <- Hm.
(* Goal: @eq Z (if Z.leb Z0 (Z.sub (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw)) then join_bits sx (Z.sub (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) mw)) (Z.add (Z.sub (Z.sub (Z.add ex emin) (Zpos xH)) emin) (Zpos xH)) else join_bits sx (Z.add mx (Z.pow (Zpos (xO xH)) mw)) Z0) x *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Zneg p)) (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
rewrite Zle_bool_true.
now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z.
(* Goal: Z.le Z0 (Z.sub (Z.add (Z.mul (Z.add (Z.pow (Zpos (xO xH)) ew) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew))) *)
(* Goal: @eq bool (Z.leb (Z.mul (Z.pow (Zpos (xO xH)) mw) (Z.pow (Zpos (xO xH)) ew)) (Z.add (Z.mul (Z.add Z0 e) (Z.pow (Zpos (xO xH)) mw)) m)) false *)
(* Goal: @eq Z (Z.modulo (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) m *)
(* Goal: @eq Z (Z.modulo (Z.div (Z.add (Z.mul (Z.add (if s then Z.pow (Zpos (xO xH)) ew else Z0) e) (Z.pow (Zpos (xO xH)) mw)) m) (Z.pow (Zpos (xO xH)) mw)) (Z.pow (Zpos (xO xH)) ew)) e *)
now ring_simplify.
(* Goal: forall (p : positive) (_ : @eq Z (Z.add mx (Z.pow (Zpos (xO xH)) mw)) (Zneg p)) (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
intros p Hm.
(* Goal: forall (_ : @eq Z (join_bits sx mx ex) x) (_ : @eq bool (valid_binary prec emax (F754_nan false xH)) true), @eq Z (join_bits false (Zpos xH) (Z.sub (Z.pow (Zpos (xO xH)) ew) (Zpos xH))) x *)
apply False_ind.
clear -Bm Hm ; zify ; omega.
Qed.

End Binary_Bits.

(** Specialization for IEEE single precision operations *)
Section B32_Bits.

Arguments B754_nan {prec emax} _ _.

Definition binary32 := binary_float 24 128.

Let Hprec : (0 < 24)%Z.
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
apply refl_equal.
Qed.

Let Hprec_emax : (24 < 128)%Z.
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
apply refl_equal.
Qed.

Definition default_nan_pl32 : bool * nan_pl 24 :=
  (false, exist _ (iter_nat xO 22 xH) (refl_equal true)).

Definition unop_nan_pl32 (f : binary32) : bool * nan_pl 24 :=
  match f with
  | B754_nan s pl => (s, pl)
  | _ => default_nan_pl32
  end.

Definition binop_nan_pl32 (f1 f2 : binary32) : bool * nan_pl 24 :=
  match f1, f2 with
  | B754_nan s1 pl1, _ => (s1, pl1)
  | _, B754_nan s2 pl2 => (s2, pl2)
  | _, _ => default_nan_pl32
  end.

Definition b32_opp := Bopp 24 128 pair.
Definition b32_plus := Bplus _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_minus := Bminus _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_mult := Bmult _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_div := Bdiv _ _ Hprec Hprec_emax binop_nan_pl32.
Definition b32_sqrt := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl32.

Definition b32_of_bits : Z -> binary32 := binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _).
Definition bits_of_b32 : binary32 -> Z := bits_of_binary_float 23 8.

End B32_Bits.

(** Specialization for IEEE double precision operations *)
Section B64_Bits.

Arguments B754_nan {prec emax} _ _.

Definition binary64 := binary_float 53 1024.

Let Hprec : (0 < 53)%Z.
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
apply refl_equal.
Qed.

Let Hprec_emax : (53 < 1024)%Z.
(* Goal: Z.lt (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) *)
apply refl_equal.
Qed.

Definition default_nan_pl64 : bool * nan_pl 53 :=
  (false, exist _ (iter_nat xO 51 xH) (refl_equal true)).

Definition unop_nan_pl64 (f : binary64) : bool * nan_pl 53 :=
  match f with
  | B754_nan s pl => (s, pl)
  | _ => default_nan_pl64
  end.

Definition binop_nan_pl64 (pl1 pl2 : binary64) : bool * nan_pl 53 :=
  match pl1, pl2 with
  | B754_nan s1 pl1, _ => (s1, pl1)
  | _, B754_nan s2 pl2 => (s2, pl2)
  | _, _ => default_nan_pl64
  end.

Definition b64_opp := Bopp 53 1024 pair.
Definition b64_plus := Bplus _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_minus := Bminus _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_mult := Bmult _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_div := Bdiv _ _ Hprec Hprec_emax binop_nan_pl64.
Definition b64_sqrt := Bsqrt _ _ Hprec Hprec_emax unop_nan_pl64.

Definition b64_of_bits : Z -> binary64 := binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _).
Definition bits_of_b64 : binary64 -> Z := bits_of_binary_float 52 11.

End B64_Bits.
