proposition: Lemma sqrt_correct : forall mode p x, toX (sqrt mode p x) = Xround radix mode (prec p) (Xsqrt_nan (toX x)).
proof: Proof. intros mode p x. unfold toX. rewrite <- Fsqrt_correct. destruct x as [|mx ex] ; try easy. simpl. generalize (mantissa_sign_correct mx). case_eq (mantissa_sign mx) ; [ intros Hx Mx | intros sx nx Hx (Mx, Vx) ]. simpl. now rewrite Hx. destruct sx ; try easy. 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. clearbody p'. rewrite exponent_cmp_correct. rewrite exponent_sub_correct. rewrite exponent_add_correct. rewrite exponent_zero_correct. unfold Fsqrt, Fsqrt_aux, Fsqrt_aux2. set (s1 := match Z.compare (EtoZ p' + EtoZ p' - EtoZ (mantissa_digits nx)) 0 with Gt => exponent_sub (exponent_add p' p') (mantissa_digits nx) | _ => exponent_zero end). set (s2 := Z.max (2 * Zpos (prec p) - Zdigits radix (Zpos (MtoP nx))) 0). assert (Hs: EtoZ s1 = s2). revert s1 s2 ; cbv zeta. replace (2 * Zpos (prec p))%Z with (Zpos (prec p) + Zpos (prec p))%Z by ring. rewrite digits_conversion. change radix with Carrier.radix. rewrite <- mantissa_digits_correct with (1 := Vx). case Zcompare_spec ; rewrite Hp ; try rewrite exponent_zero_correct ; intros H ; apply eq_sym ; try apply Zmax_right. now apply Zlt_le_weak. now apply Zeq_le. rewrite exponent_sub_correct. rewrite exponent_add_correct. rewrite Hp. apply Zmax_left. now apply Z.le_ge, Zlt_le_weak. clearbody s1 s2. generalize (exponent_div2_floor_correct (exponent_sub ex s1)). case exponent_div2_floor ; intros e1 r He. rewrite exponent_cmp_correct. rewrite exponent_zero_correct. set (s3 := if r then exponent_add s1 exponent_one else s1). set (s4e2 := if Z.even (EtoZ ex - s2) then (s2, EtoZ ex - s2)%Z else (s2 + 1, EtoZ ex - s2 - 1)%Z). assert (Hes: EtoZ e1 = Z.div2 (snd s4e2) /\ EtoZ s3 = fst s4e2). clear -He Hs. generalize (Zdiv2_odd_eqn (EtoZ ex - s2)). rewrite Zodd_even_bool. rewrite exponent_sub_correct, Hs in He. assert (Z.even (EtoZ ex - s2) = negb r). rewrite He. rewrite (Zplus_comm (2 * EtoZ e1)). rewrite Z.even_add_mul_2. now case r. rewrite H. rewrite negb_involutive. change Zeven with Z.even in s4e2. intros H'. revert s4e2 s3 ; cbv zeta. rewrite H. destruct r ; simpl. split. rewrite H'. replace (2 * Z.div2 (EtoZ ex - s2) + 1 - 1)%Z with (2 * Z.div2 (EtoZ ex - s2))%Z by ring. rewrite Z.div2_div. rewrite Zmult_comm, Z_div_mult by easy. lia. rewrite exponent_add_correct. rewrite exponent_one_correct. now rewrite Hs. split. lia. exact Hs. clearbody s4e2 s3. destruct s4e2 as [s4 e2]. simpl in Hes. rewrite <- (proj2 Hes). rewrite <- (proj1 Hes). clear He Hes. set (m1 := match Z.compare (EtoZ s3) 0 with Gt => mantissa_shl nx s3 | _ => nx end). set (m2 := match EtoZ s3 with Zpos p => (Zpos (MtoP nx) * Z.pow_pos radix p)%Z | _ => Zpos (MtoP nx) end). assert (Hm: valid_mantissa m1 /\ Zpos (MtoP m1) = m2). revert m1 m2 ; cbv zeta. case_eq (EtoZ s3) ; simpl Z.compare ; cbv iota. intros _. now split. intros q Hq. generalize (mantissa_shl_correct q nx s3 Vx Hq). intros [-> H]. apply (conj H). apply shift_correct. intros q Hq. now split. generalize (mantissa_sqrt_correct m1 (proj1 Hm)). rewrite <- (proj2 Hm). clearbody m1 m2. clear Hm. destruct (mantissa_sqrt m1) as [q l]. destruct (Z.sqrtrem (Z.pos (MtoP m1))) as [s r']. intros [<- [H1 H2]]. rewrite round_aux_correct with (1 := H2). unfold prec at 1. rewrite Hp. clear -H1. apply (f_equal (fun l => FtoX (Fround_at_prec mode (prec p) (Ufloat _ _ _ l)))). destruct l. now rewrite Zeq_bool_true. rewrite Zeq_bool_false. now rewrite Zle_bool_true. now apply Zgt_not_eq. easy. rewrite Zeq_bool_false. now rewrite Zle_bool_false. apply Zgt_not_eq. now apply Z.lt_trans with (2 := H1). Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig