proposition: Lemma mantissa_sqrt_correct : forall x, valid_mantissa x -> let (q,l) := mantissa_sqrt x in let (s,r) := Z.sqrtrem (Zpos (MtoP x)) in Zpos (MtoP q) = s /\ match l with pos_Eq => r = Z0 | pos_Lo => (0 < r <= s)%Z | pos_Mi => False | pos_Up => (s < r)%Z end /\ valid_mantissa q.
proof: Proof. intros x [x' Vx]. unfold mantissa_sqrt, MtoP. rewrite BigN.spec_eqb. rewrite BigN.spec_compare. rewrite BigN.spec_sub. rewrite BigN.spec_square. rewrite BigN.spec_sqrt. rewrite <- Z.sqrtrem_sqrt. refine (_ (Z.sqrtrem_spec (Zpos x') _)). 2: easy. rewrite Vx. case_eq (Z.sqrtrem (Zpos x')). intros s r Hsr. simpl fst. intros [H1 H2]. refine ((fun H => conj (proj1 H) (conj _ (proj2 H))) _). clear H. rewrite H1. replace (s * s + r - s * s)%Z with r by ring. rewrite Zmax_right by easy. change (BigN.to_Z 0) with Z0. case Z.eqb_spec. easy. intros H. assert (H3: (0 < r)%Z) by lia. case Zcompare_spec ; intros H4. apply (conj H3). now apply Zlt_le_weak. apply (conj H3). now apply Zeq_le. exact H4. destruct s as [|s|s]. simpl in H1. rewrite <- H1 in H2. now elim (proj2 H2). split. apply eq_refl. exists s. rewrite BigN.spec_sqrt. rewrite <- Z.sqrtrem_sqrt. now rewrite Vx, Hsr. now elim (Z.le_trans _ _ _ (proj1 H2) (proj2 H2)). Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig