proposition: 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: Proof. intros s m e Hm He. assert (0 <= mw)%Z as Hmw. destruct mw as [|mw'|mw'] ; try easy. clear -Hm ; simpl in Hm ; lia. assert (0 <= ew)%Z as Hew. destruct ew as [|ew'|ew'] ; try easy. clear -He ; simpl in He ; lia. unfold split_bits, join_bits. rewrite Z.shiftl_mul_pow2 by easy. apply f_equal2 ; [apply f_equal2|]. - case s. + apply Zle_bool_true. apply Zle_0_minus_le. ring_simplify. apply Zplus_le_0_compat. apply Zmult_le_0_compat. apply He. clear -Hm ; lia. apply Hm. + 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. apply Z.lt_le_trans with (2^mw * 1)%Z. now apply Zmult_lt_compat_r. apply Zmult_le_compat_l. clear -He ; lia. clear -Hm ; lia. - rewrite Zplus_comm. rewrite Z_mod_plus_full. now apply Zmod_small. - rewrite Z_div_plus_full_l by (clear -Hm ; lia). rewrite Zdiv_small with (1 := Hm). rewrite Zplus_0_r. case s. + replace (2^ew + e)%Z with (e + 1 * 2^ew)%Z by ring. rewrite Z_mod_plus_full. now apply Zmod_small. + now apply Zmod_small. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary