proposition: 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: Proof. intros x Hx. unfold split_bits, join_bits. rewrite Z.shiftl_mul_pow2 by now apply Zlt_le_weak. pattern x at 4 ; rewrite Z.div_mod with x (2^mw)%Z. apply (f_equal (fun v => (v + _)%Z)). rewrite Zmult_comm. apply f_equal. pattern (x / (2^mw))%Z at 2 ; rewrite Z.div_mod with (x / (2^mw))%Z (2^ew)%Z. apply (f_equal (fun v => (v + _)%Z)). replace (x / 2 ^ mw / 2 ^ ew)%Z with (if Zle_bool (2 ^ mw * 2 ^ ew) x then 1 else 0)%Z. case Zle_bool. now rewrite Zmult_1_r. now rewrite Zmult_0_r. rewrite Zdiv_Zdiv. apply sym_eq. case Zle_bool_spec ; intros Hs. apply Zle_antisym. cut (x / (2^mw * 2^ew) < 2)%Z. clear ; lia. apply Zdiv_lt_upper_bound. now apply Zmult_lt_0_compat. rewrite <- Zpower_exp ; try ( apply Z.le_ge ; apply Zlt_le_weak ; assumption ). change 2%Z with (Zpower 2 1) at 1. rewrite <- Zpower_exp. now rewrite Zplus_comm. discriminate. apply Z.le_ge. now apply Zplus_le_0_compat ; apply Zlt_le_weak. apply Zdiv_le_lower_bound. now apply Zmult_lt_0_compat. now rewrite Zmult_1_l. apply Zdiv_small. now split. now apply Zlt_le_weak. now apply Zlt_le_weak. now apply Zgt_not_eq. now apply Zgt_not_eq. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary