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.