proposition: Theorem Fdiv_core_correct : forall m1 e1 m2 e2 e, (0 < m1)%Z -> (0 < m2)%Z -> let '(m, l) := Fdiv_core m1 e1 m2 e2 e in inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
proof: Proof. intros m1 e1 m2 e2 e Hm1 Hm2. unfold Fdiv_core. match goal with |- context [if ?b then ?b1 else ?b2] => set (m12 := if b then b1 else b2) end. case_eq m12 ; intros m1' m2' Hm. assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * bpow e)%R /\ (0 < m2')%Z) as [Hf Hm2']. { unfold F2R, Zminus ; simpl. destruct (Zle_bool e (e1 - e2)) eqn:He' ; injection Hm ; intros ; subst. - split ; try easy. apply Zle_bool_imp_le in He'. rewrite mult_IZR, IZR_Zpower by lia. unfold Zminus ; rewrite 2!bpow_plus, 2!bpow_opp. field. repeat split ; try apply Rgt_not_eq, bpow_gt_0. now apply IZR_neq, Zgt_not_eq. - apply Z.leb_gt in He'. split ; cycle 1. { apply Z.mul_pos_pos with (1 := Hm2). apply Zpower_gt_0 ; lia. } rewrite mult_IZR, IZR_Zpower by lia. unfold Zminus ; rewrite bpow_plus, bpow_opp, bpow_plus, bpow_opp. field. repeat split ; try apply Rgt_not_eq, bpow_gt_0. now apply IZR_neq, Zgt_not_eq. } clearbody m12 ; clear Hm Hm1 Hm2. generalize (Z_div_mod m1' m2' (Z.lt_gt _ _ Hm2')). destruct (Z.div_eucl m1' m2') as (q, r). intros (Hq, Hr). rewrite Hf. unfold inbetween_float, F2R. simpl. rewrite Hq, 2!plus_IZR, mult_IZR. apply inbetween_mult_compat. apply bpow_gt_0. destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2'']. - replace 1%R with (IZR m2' * /IZR m2')%R. apply new_location_correct ; try easy. apply Rinv_0_lt_compat. now apply IZR_lt. constructor. field. now apply IZR_neq, Zgt_not_eq. field. now apply IZR_neq, Zgt_not_eq. - assert (r = 0 /\ m2' = 1)%Z as [-> ->] by (clear -Hr Hm2'' ; lia). unfold Rdiv. rewrite Rmult_1_l, Rplus_0_r, Rinv_1, Rmult_1_r. now constructor. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Generic_fmt Float_prop Digits Bracket