# Module correct_result

``` Require Export sqrt_prog. Require Export correct_goals. Definition Zminus [x,y:Z]:=`x+(-y)`. Definition Z_lt_le_bool := [x,y:Z](bool_of_sumbool ? ? (Z_lt_le_dec x y)). Correctness correct_result fun (np:nat)(sp:nat)(nn:nat)(l:nat ref)(h:nat ref)       (q:Z ref)(c:Z ref)(b:Z ref) -> {(lt (S O) nn) /\ (l=(div2' nn))/\(h=(minus nn (div2' nn))) /\       `np + 2*nn<=bound`/\ `sp +nn <= bound`/\       (`np+2*nn <= sp`\/`sp + nn <= np`) /\       `q*(pow beta nn) + (I m sp nn) <= (pow beta nn)` /\       `0 < q*(pow beta nn) + (I m sp nn)`} begin   if (Z_lt_le_bool !c ZERO) then     begin       (c := (Zplus             (Zplus (mpn_addmul_1 np sp nn (inject_nat (S (S O))))             (Zmult (POS (xO xH)) !q)) {(Post_mpn_addmul_1 m m@ np sp nn (inject_nat (S (S O)))        (Zminus result (Zmult (POS (xO xH)) q)))} !c) {(Post_mpn_addmul_1 m m@ np sp nn (inject_nat (S (S O)))        (Zminus (Zminus result (Zmult (POS (xO xH)) q)) c@))}) {(Post_mpn_addmul_1 m m@ np sp nn (inject_nat (S (S O)))        (Zminus (Zminus c (Zmult (POS (xO xH)) q)) c@))};       (mpn_sub_1 np np nn (inject_nat (S O)));       c := (Zminus !c (bool2Z !rb));       (mpn_sub_1 sp sp nn (inject_nat (S O)));       q := (Zminus !q (bool2Z !rb))     end end {(`0 <= c@ ` -> (m=m@/\c=c@)) /\        (`c@ < 0 ` -> ((I m sp nn) = `q@*(pow beta nn)+ (I m@ sp nn) - 1`/\                      `c*(pow beta nn) + (I m np nn)                       = c@*(pow beta nn) + (I m@ np nn) + 2*q@*(pow beta nn) +                       2*(I m@ sp nn) - 1` /\                       ((p:nat)`0<=p<bound`->~(((le sp p)/\(lt p (plus sp nn)))\/                                ((le np p)/\(lt p (plus np (mult (S (S O)) nn)))))                           ->(access m p)=(access m@ p))))}. Apply correct_goal1 with   c := c h := h l := l m := m q := q;Assumption. Apply correct_goal2 with   sp := sp c := c h := h l := l m := m q := q x0 := x0 m0 := m0;Assumption. Apply correct_goal3 with   sp := sp l := l h := h;Assumption. Apply correct_goal4 with   np := np sp := sp nn := nn l := l h := h m := m m0 := m0 q := q c:= c c0 := c0 ;Assumption. Apply correct_goal5 with   np := np sp := sp l := l h := h q:=q m := m c := c c0 := c0 m0 := m0 m1 := m1 rb0:=rb0;Assumption. Apply correct_goal6 with   np := np sp := sp c := c h := h l := l m := m q := q m0 := m0 m1:= m1 rb1 := rb1;Assumption. Apply correct_goal7 with   l := l h := h;Assumption. Defined. ```

``` ```

Index