proposition: Lemma shr_conversion : forall m d, shr m d = let (r, s) := hrndG_aux (Zfloor (IZR (Zpos m) * bpow radix2 (- Zpos d))) (IZR (Zpos m) * bpow radix2 (- Zpos d)) in rnd_record_mk (ZtoN (Zfloor (IZR (Zpos m) * bpow radix2 (- Zpos d)))) r s.
proof: Proof. intros m d. unfold shr. rewrite iter_pos_nat. rewrite (Zpos_eq_Z_of_nat_o_nat_of_P d). induction (nat_of_P d). simpl. rewrite Rmult_1_r. rewrite Zfloor_IZR. unfold hrndG_aux, inbetween_loc. now rewrite Rcompare_Eq. rewrite iter_nat_S. rewrite IHn. clear IHn. unfold hrndG_aux. set (ms := (IZR (Zpos m) * bpow radix2 (- Z_of_nat (S n)))%R). replace (IZR (Zpos m) * bpow radix2 (- Z_of_nat n))%R with (ms * 2)%R. assert (H0: (0 <= Zfloor ms)%Z). apply Zfloor_lub. unfold ms. apply Rmult_le_pos. now apply IZR_le. apply bpow_ge_0. clearbody ms. clear -H0. destruct (inbetween_spec _ _ ms (bracket_aux _)) as [H|l H1 H2]. replace (Zfloor (ms * 2)) with (Zfloor ms * 2)%Z. unfold inbetween_loc. rewrite mult_IZR. rewrite Rcompare_Eq. destruct (Zfloor ms) as [|p|p] ; try easy. now rewrite Zmult_comm. now rewrite <- H. rewrite H at 2. rewrite <- mult_IZR. now rewrite Zfloor_IZR. unfold inbetween_loc. assert (H3: Rcompare (ms * 2) (IZR (Zfloor ms) * 2 + 1) = l). rewrite <- (Rcompare_mult_r 2) in H2. now replace (IZR (Zfloor ms) * 2 + 1)%R with ((IZR (Zfloor ms) + (IZR (Zfloor ms) + 1)) / 2 * 2)%R by field. now apply IZR_lt. clear H2. rewrite <- H3. clear H3. case Rcompare_spec ; intros H4. elim Rlt_not_le with (1 := H4). apply Zfloor_lb. unfold shr_aux. simpl. rewrite H4. rewrite <- mult_IZR, <- plus_IZR. rewrite Rcompare_IZR. rewrite <- H4. replace (Zfloor (ms * 2)) with (1 + 2 * Zfloor ms)%Z. rewrite Zcompare_Eq. clear -H0. destruct (Zfloor ms) as [|p|p] ; [easy|easy|]. now elim H0. now rewrite Zmult_comm, Zplus_comm. clear -H1 H4. assert (Zfloor ms * 2 < Zfloor (ms * 2) < (Zfloor ms + 1) * 2)%Z. split ; apply lt_IZR ; rewrite <- H4 ; rewrite mult_IZR ; apply Rmult_lt_compat_r. now apply IZR_lt. apply H1. now apply IZR_lt. now rewrite plus_IZR. lia. set (rs := match Rcompare (ms * 2) ((IZR (Zfloor (ms * 2)) + (IZR (Zfloor (ms * 2)) + 1)) / 2) with Eq => (true, false) | Lt => (false, true) | Gt => (true, true) end). rewrite (surjective_pairing rs). unfold shr_aux. simpl. replace (fst rs || snd rs) with true. clear rs. case Rcompare_spec ; intros H2. replace (Zfloor (ms * 2)) with (2 * Zfloor ms)%Z. now case (Zfloor ms). apply sym_eq. rewrite Zmult_comm. apply Zfloor_imp. rewrite plus_IZR, mult_IZR. refine (conj _ H2). apply Rmult_le_compat_r. now apply IZR_le. apply Zfloor_lb. elim Rlt_not_le with (1 := H4). rewrite H2. rewrite <- mult_IZR, <- plus_IZR. rewrite Zfloor_IZR. apply Rle_refl. replace (Zfloor (ms * 2)) with (1 + 2 * Zfloor ms)%Z. revert H0. case (Zfloor ms) ; [easy|easy|]. intros p H. now elim H. apply sym_eq. apply Zfloor_imp. rewrite plus_IZR, mult_IZR. split. rewrite Rplus_comm, Rmult_comm. now apply Rlt_le. rewrite 2!plus_IZR, mult_IZR. simpl. replace (1 + 2 * IZR (Zfloor ms) + 1)%R with ((IZR (Zfloor ms) + 1) * 2)%R by ring. apply Rmult_lt_compat_r. now apply IZR_lt. apply H1. unfold rs. now case Rcompare. unfold ms. rewrite Rmult_assoc. change 2%R with (bpow radix2 1). rewrite <- bpow_plus. apply (f_equal (fun e => _ * bpow radix2 e)%R). rewrite inj_S. unfold Z.succ. ring. Qed.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux