proposition: Theorem div_correct : forall mode p x y, toX (div mode p x y) = Xround radix mode (prec p) (Xdiv (toX x) (toX y)).
proof: Proof. intros mode p x y. unfold toX. rewrite <- Fdiv_correct. destruct x as [|mx ex] ; destruct y as [|my ey] ; try easy. simpl. now case (mantissa_sign mx). simpl. generalize (mantissa_sign_correct mx). case_eq (mantissa_sign mx) ; [ intros Hx Mx | intros sx nx Hx (Mx, Vmx) ]. destruct (mantissa_sign my) as [|sy ny]. apply refl_equal. simpl. now rewrite Hx. generalize (mantissa_sign_correct my). case_eq (mantissa_sign my) ; [ intros Hy My | intros sy ny Hy (My, Vmy) ]. apply refl_equal. rewrite exponent_cmp_correct. rewrite exponent_sub_correct, exponent_add_correct, exponent_zero_correct. rewrite 2!mantissa_digits_correct ; try easy. rewrite <- 2!digits_conversion. unfold Fdiv, Fdiv_aux, Fdiv_aux2. set (p' := match exponent_cmp p exponent_zero with Gt => p | _ => exponent_one end). assert (Hp: EtoZ p' = Zpos (prec p)). unfold p', prec. rewrite exponent_cmp_correct, exponent_zero_correct. case_eq (EtoZ p) ; try (intros ; apply exponent_one_correct). easy. rewrite Hp. unfold radix. set (d := (Zdigits Carrier.radix (Zpos (MtoP ny)) + Zpos (prec p) - Zdigits Carrier.radix (Zpos (MtoP nx)))%Z). set (nd := exponent_sub (exponent_add (mantissa_digits ny) p') (mantissa_digits nx)). assert (Hs := fun d' (H : EtoZ nd = Zpos d') => mantissa_shl_correct d' nx nd Vmx H). assert (Hs': forall d', d = Zpos d' -> MtoP (mantissa_shl nx nd) = shift Carrier.radix (MtoP nx) d' /\ valid_mantissa (mantissa_shl nx nd)). intros d' H. apply Hs. unfold nd. rewrite exponent_sub_correct, exponent_add_correct, 2!mantissa_digits_correct, <- 2!digits_conversion ; trivial. now rewrite Hp. replace (match (d ?= 0)%Z with | Gt => div_aux mode p' (xorb sx sy) (mantissa_shl nx nd) ny (exponent_sub (exponent_sub ex ey) nd) | _ => div_aux mode p' (xorb sx sy) nx ny (exponent_sub ex ey) end) with (div_aux mode p' (xorb sx sy) (match d with Zpos _ => mantissa_shl nx nd | _ => nx end) ny (match d with Zpos _ => exponent_sub (exponent_sub ex ey) nd | _ => exponent_sub ex ey end)) by now case d. unfold div_aux. assert (Vmx': valid_mantissa (match d with Zpos _ => mantissa_shl nx nd | _ => nx end)). destruct d as [|pd|pd] ; trivial. now apply (Hs' pd). assert (Hxy: (Zpos (MtoP ny) <= Zpos (MtoP (match d with Zpos _ => mantissa_shl nx nd | _ => nx end)))%Z). apply Zlt_le_weak. apply (lt_Zdigits Carrier.radix). easy. case_eq d. unfold d. clear ; lia. intros p0 Hp0. specialize (Hs' p0 Hp0). rewrite (proj1 Hs'). rewrite shift_correct. fold (Zpower Carrier.radix (Zpos p0)). rewrite Zdigits_mult_Zpower ; try easy. rewrite <- Hp0. unfold d. clear ; lia. intros p0. unfold d. clear ; lia. clear Hs. generalize (mantissa_div_correct _ ny Vmx' Vmy Hxy). destruct (mantissa_div (match d with Zpos _ => mantissa_shl nx nd | _ => nx end) ny) as (nq, nl). assert (H: Zpos (MtoP (match d with Zpos _ => mantissa_shl nx nd | _ => nx end)) = match d with Zpos p0 => (Zpos (MtoP nx) * Zpower_pos Carrier.radix p0)%Z | _ => Zpos (MtoP nx) end). destruct d as [|pd|pd] ; trivial. rewrite <- shift_correct. apply f_equal. now apply Hs'. rewrite H. clear H. intros (H1, (H2, H3)). rewrite round_aux_correct with (1 := H3). apply (f_equal2 (fun v w => FtoX (Fround_at_prec mode v w))). unfold prec. now rewrite Hp. replace (match d with Zpos p0 => ((Zpos (MtoP nx) * Zpower_pos Carrier.radix p0), (EtoZ ex - EtoZ ey + Zneg p0))%Z | _ => (Zpos (MtoP nx), (EtoZ ex - EtoZ ey)%Z) end) with (match d with Zpos p0 => (Zpos (MtoP nx) * Zpower_pos Carrier.radix p0)%Z | _ => Zpos (MtoP nx) end, match d with Zpos p0 => (EtoZ ex - EtoZ ey + Zneg p0)%Z | _ => (EtoZ ex - EtoZ ey)%Z end) by now case d. revert H1. unfold Z.div. generalize (Z_div_mod (match d with Zpos p0 => (Zpos (MtoP nx) * Zpower_pos Carrier.radix p0)%Z | _ => Zpos (MtoP nx) end) (Zpos (MtoP ny)) (refl_equal _)). rewrite Zfast_div_eucl_correct. case Z.div_eucl. intros q r (Hq,Hr) H1. rewrite <- H1. apply f_equal2. case_eq d ; try (intros ; apply exponent_sub_correct). intros p0 Hp0. rewrite 2!exponent_sub_correct. unfold Zminus. apply f_equal. change (Zneg p0) with (-Zpos p0)%Z. rewrite <- Hp0. unfold nd. rewrite exponent_sub_correct, exponent_add_correct, 2!mantissa_digits_correct, <- 2!digits_conversion ; trivial. now rewrite Hp. replace nl with (convert_location (convert_location_inv nl)) by now case nl. apply f_equal. destruct (Zle_or_lt (Zpos (MtoP ny)) 1) as [Ky|Ky]. assert (Zpos (MtoP ny) = 1%Z /\ r = Z0). clear -Hr Ky ; lia. rewrite (proj1 H), (proj2 H). inversion_clear H2. easy. apply False_ind. revert H0. rewrite (proj1 H). unfold Rdiv. rewrite Rinv_1, Rmult_1_r. intros (H0, H2). generalize (lt_IZR _ _ H0) (lt_IZR _ _ H2). clear ; lia. apply Bracket.inbetween_unique with (1 := H2). rewrite plus_IZR. replace 1%R with (IZR (Zpos (MtoP ny)) * /IZR (Zpos (MtoP ny)))%R. apply Bracket.new_location_correct ; trivial. apply Rinv_0_lt_compat. now apply IZR_lt. constructor. rewrite Hq, H1. rewrite plus_IZR. unfold Rdiv. rewrite Rmult_plus_distr_r. rewrite mult_IZR, <- (Rmult_comm (IZR q)), Rmult_assoc. rewrite Rinv_r. now rewrite Rmult_1_r. now apply IZR_neq. apply Rinv_r. now apply IZR_neq. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig