proposition: Lemma inbetween_shr_1 : forall x mrs e, (0 <= shr_m mrs)%Z -> inbetween_float radix2 (shr_m mrs) e x (loc_of_shr_record mrs) -> inbetween_float radix2 (shr_m (shr_1 mrs)) (e + 1) x (loc_of_shr_record (shr_1 mrs)).
proof: Proof. intros x mrs e Hm Hl. refine (_ (new_location_even_correct (F2R (Float radix2 (shr_m (shr_1 mrs)) (e + 1))) (bpow radix2 e) 2 _ _ _ x (if shr_r (shr_1 mrs) then 1 else 0) (loc_of_shr_record mrs) _ _)) ; try easy. 2: apply bpow_gt_0. 2: now case (shr_r (shr_1 mrs)) ; split. change 2%R with (bpow radix2 1). rewrite <- bpow_plus. rewrite (Zplus_comm 1), <- (F2R_bpow radix2 (e + 1)). unfold inbetween_float, F2R. simpl. rewrite plus_IZR, Rmult_plus_distr_r. replace (Bracket.new_location_even 2 (if shr_r (shr_1 mrs) then 1%Z else 0%Z) (loc_of_shr_record mrs)) with (loc_of_shr_record (shr_1 mrs)). easy. clear -Hm. destruct mrs as (m, r, s). now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|]. rewrite (F2R_change_exp radix2 e). 2: apply Zle_succ. unfold F2R. simpl. rewrite <- 2!Rmult_plus_distr_r, <- 2!plus_IZR. rewrite Zplus_assoc. replace (shr_m (shr_1 mrs) * 2 ^ (e + 1 - e) + (if shr_r (shr_1 mrs) then 1%Z else 0%Z))%Z with (shr_m mrs). exact Hl. ring_simplify (e + 1 - e)%Z. change (2^1)%Z with 2%Z. rewrite Zmult_comm. clear -Hm. destruct mrs as (m, r, s). now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative