Require Export sub_square.
Require Export correct_result.
Require Export division_step.
Require Export sqrt_goals.
Require Export sqrt_goals2.
Require Export sqrt_goals3.
Require Export sqrt_goals4.
Correctness sqrt_root
let rec mpn_dq_sqrtrem (sp:nat)(np:nat)(nn:nat):unit
{variant nn for lt}
= {`sp+nn<=bound`
/\`np+2*nn<=bound`
/\ (Zlt ZERO (I m np (mult (2) nn)))
/\ (`np + 2*nn <= sp`\/`sp + nn <= np`)
/\ (IsNormalized (I m np (mult (2) nn))
(pow beta (mult (2) nn)))
/\ (lt O nn)
}
(let r = ref true in
let q = ref ZERO in
let c = ref ZERO in
let b = ref ZERO in
let l = ref O in
let h = ref O in
begin
if (nat_eq_bool nn (S O))
then begin (mpn_sqrtrem2 sp np np) end
else begin
l := (div2' nn);
h := (minus nn !l);
(mpn_dq_sqrtrem (plus sp !l)
(plus np (mult (S (S O)) !l)) !h);
q := (bool2Z !rb);
assert {(SqrtremProp (I m@0 (plus np (mult (S (S O)) l))
(mult (2) h))
(I m (plus sp l) h)
(Zplus (I m (plus np (mult (2) l)) h)
(Zmult q (pow beta h))))/\
((p:nat)`0<=p<bound`->~(((le (plus np (mult (2) l)) p)/\
(lt p (plus np (mult (2) nn))))\/
((le (plus sp l) p)/\
(lt p (plus sp nn))))->
(access m@0 p)=(access m p)) /\
((q=ZERO)\/(q=`1`)) } ;
label after_recursive_call;
(division_step np sp nn l h c q);
label end_of_div;
assert {(Zdivprop' `q@after_recursive_call *(pow beta nn) +
(I m@after_recursive_call
(plus np l) nn)`
`2 *(I m@after_recursive_call
(plus sp l) h)`
`q * (pow beta l) + (I m sp l)`
`c * (pow beta h) + (I m (plus np l) h)`)
/\
((p:nat)`0<=p<bound`->~((le sp p)/\ (lt p (plus sp l))\/
(le (plus np l) p)/\ (lt p (plus np (plus (plus l l) h))))->
(access m p)=(access m@after_recursive_call p)) /\
`0 <= q <= 1`};
(square_s_and_sub np sp nn l h q c b);
(mpn_add_1 (plus sp !l) (plus sp !l) !h !q);
q := (bool2Z !rb);
label before_correction;
(correct_result np sp nn l h q c b);
rb := (Z2bool !c)
end
end)
{
(SqrtremProp (I m@ np (mult (2) nn))
(I m sp nn)
(Zplus (I m np nn)
(Zmultbool rb (pow beta nn))))/\
((p:nat)`0<=p<bound`->~(((le np p)/\
(lt p (plus np (mult (2) nn))))\/
((le sp p)/\
(lt p (plus sp nn))))->
(access m@0 p)=(access m p))}
.
Apply sqrt_goal1
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0 ; Assumption.
Apply sqrt_goal2
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0 ; Assumption.
Apply sqrt_goal3
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0
m0 := m0; Assumption.
Apply sqrt_goal4
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0
m0 := m0; Assumption.
Apply sqrt_goal5
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0
m0 := m0; Assumption.
Apply sqrt_goal6
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0
m0 := m0
m1 := m1
rb1 := rb1
c0:=c0; Assumption.
Apply sqrt_goal7
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0
m0 := m0
m1 := m1
rb1 := rb1
c0:=c0
m2 := m2
m3 := m3
c1 := c1; Assumption.
Apply sqrt_goal8
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0
m0 := m0
m1 := m1
rb1 := rb1
c0:=c0
m2 := m2
m3 := m3
c1 := c1
q1 := q1; Assumption.
Apply sqrt_goal9
with rphi1 := rphi1
sp0 := sp0
np0 := np0
nn0 := nn0
m0 := m0
m1 := m1
rb1 := rb1
c0:=c0
m2 := m2
m3 := m3
c1 := c1
q1 := q1
rb4 := rb4
m4 := m4; Assumption.
Apply sqrt_goal10
with rphi1 := rphi1 ; Assumption.
Defined.