Require Why.
Require Export sqrt_why.
Definition sqrt
: (x: Z)(_: `x >= 0`)
(sig_1 Z [result: Z](`result * result <= x` /\
`x < (result + 1) * (result + 1)`))
:= [x: Z; Pre6: `x >= 0`]
let (result, Post9) =
let (result, Bool3) =
let (result1, Post10) = (Z_eq_bool x `0`) in
(exist_1 [result2: bool]
(if result2 then `x = 0` else `x <> 0`) result1 Post10) in
(Cases (btest [result:bool](if result then `x = 0` else `x <> 0`)
result Bool3) of
| (left Test6) =>
let (result0, Post19) = (exist_1 [result0: Z]
`result0 * result0 <= x` /\
`x < (result0 + 1) * (result0 + 1)` `0`
(sqrt_po_1 x Pre6 Test6)) in
(exist_1 [result1: Z]`result1 * result1 <= x` /\
`x < (result1 + 1) * (result1 + 1)` result0 Post19)
| (right Test5) =>
let (result0, Post11) =
let (result0, Bool2) =
let (result2, Post12) = (Z_le_gt_bool x `3`) in
(exist_1 [result3: bool]
(if result3 then `x <= 3` else `x > 3`) result2 Post12) in
(Cases (btest
[result0:bool](if result0 then `x <= 3` else `x > 3`)
result0 Bool2) of
| (left Test4) =>
let (result1, Post18) = (exist_1 [result1: Z]
`result1 * result1 <= x` /\
`x < (result1 + 1) * (result1 + 1)` `1`
(sqrt_po_2 x Pre6 Test5 Test4)) in
(exist_1 [result2: Z]`result2 * result2 <= x` /\
`x < (result2 + 1) * (result2 + 1)` result1 Post18)
| (right Test3) =>
let (result1, Post13) =
let (result1, Post5) = (exist_1 [result1: Z]
result1 = x x (refl_equal ? x)) in
let (y0, result2, Post14) =
let Pre5 =
(sqrt_po_3 x Pre6 Test5 Test3 result1 Post5) in
let (result2, Post4) = (exist_1 [result2: Z]
result2 = (Zdiv (`x + 1`) `2`) (Zdiv (`x + 1`) `2`)
(refl_equal ? (Zdiv (`x + 1`) `2`))) in
let (y0, z0, result3, Post15) =
let (y0, z0, result3, Post3) =
(well_founded_induction Z (Zwf ZERO)
(Zwf_well_founded `0`) [Variant1: Z](y0: Z)
(z0: Z)(_: Variant1 = y0)(_0: `z0 > 0` /\
`y0 > 0` /\
`z0 = (Zdiv ((Zdiv x y0) + y0) 2)` /\
`x < (y0 + 1) * (y0 + 1)` /\
`x < (z0 + 1) * (z0 + 1)`)
(sig_3 Z Z unit [y1: Z][z1: Z][result3: unit]
((`z1 > 0` /\ `y1 > 0` /\
`z1 = (Zdiv ((Zdiv x y1) + y1) 2)` /\
`x < (y1 + 1) * (y1 + 1)` /\
`x < (z1 + 1) * (z1 + 1)`) /\ `z1 >= y1`))
[Variant1: Z; wf1: (Variant2: Z)
(Pre1: (Zwf `0` Variant2 Variant1))(y0: Z)
(z0: Z)(_: Variant2 = y0)(_0: `z0 > 0` /\
`y0 > 0` /\
`z0 = (Zdiv ((Zdiv x y0) + y0) 2)` /\
`x < (y0 + 1) * (y0 + 1)` /\
`x < (z0 + 1) * (z0 + 1)`)
(sig_3 Z Z unit [y1: Z][z1: Z][result3: unit]
((`z1 > 0` /\ `y1 > 0` /\
`z1 = (Zdiv ((Zdiv x y1) + y1) 2)` /\
`x < (y1 + 1) * (y1 + 1)` /\
`x < (z1 + 1) * (z1 + 1)`) /\ `z1 >= y1`));
y0: Z; z0: Z; Pre4: Variant1 = y0;
Pre3: `z0 > 0` /\ `y0 > 0` /\
`z0 = (Zdiv ((Zdiv x y0) + y0) 2)` /\
`x < (y0 + 1) * (y0 + 1)` /\
`x < (z0 + 1) * (z0 + 1)`]
let (result3, Bool1) =
let (result5, Post16) =
(Z_lt_ge_bool z0 y0) in
(exist_1 [result6: bool]
(if result6 then `z0 < y0` else `z0 >= y0`)
result5 Post16) in
(Cases (btest
[result3:bool](if result3
then `z0 < y0`
else `z0 >= y0`)
result3 Bool1) of
| (left Test2) =>
let (y1, z1, result4, Post3) =
let (y1, z1, result4, Post6) =
let (y1, result4, Post1) =
let (result4, Post1) =
(exist_1 [result4: Z]
result4 = z0 z0
(refl_equal ? z0)) in
(exist_2 [y2: Z][result5: unit]
y2 = z0 result4 tt Post1) in
let Pre2 = Pre5 in
let (z1, result5, Post2) =
let (result5, Post2) =
(exist_1 [result5: Z]
result5 = (Zdiv (`(Zdiv x z0) + z0`)
`2`) (Zdiv (`(Zdiv x z0) +
z0`)
`2`)
(refl_equal ? (Zdiv (`(Zdiv x z0) +
z0`)
`2`))) in
(exist_2 [z2: Z][result6: unit]
z2 = (Zdiv (`(Zdiv x z0) + z0`) `2`)
result5 tt Post2) in
(exist_3 [y2: Z][z2: Z][result6: unit]
(`z2 > 0` /\ `y2 > 0` /\
`z2 = (Zdiv ((Zdiv x y2) + y2) 2)` /\
`x < (y2 + 1) * (y2 + 1)` /\
`x < (z2 + 1) * (z2 + 1)`) /\
(Zwf `0` y2 y0) y1 z1 result5
(sqrt_po_4 x Pre6 Test5 Test3 result1
Post5 Pre5 result2 Post4 Variant1 y0
z0 Pre4 Pre3 Test2 y1 Post1 Pre2 z1
Post2)) in
((wf1 y1) (loop_variant_1 Pre4 Post6)
y1 z1 (refl_equal ? y1)
(proj1 ? ? Post6)) in
(exist_3 [y2: Z][z2: Z][result5: unit]
(`z2 > 0` /\ `y2 > 0` /\
`z2 = (Zdiv ((Zdiv x y2) + y2) 2)` /\
`x < (y2 + 1) * (y2 + 1)` /\
`x < (z2 + 1) * (z2 + 1)`) /\
`z2 >= y2` y1 z1 result4 Post3)
| (right Test1) =>
let (y1, z1, result4, Post3) =
(exist_3 [y1: Z][z1: Z][result4: unit]
(`z1 > 0` /\ `y1 > 0` /\
`z1 = (Zdiv ((Zdiv x y1) + y1) 2)` /\
`x < (y1 + 1) * (y1 + 1)` /\
`x < (z1 + 1) * (z1 + 1)`) /\
`z1 >= y1` y0 z0 tt
(conj ? ? Pre3 Test1)) in
(exist_3 [y2: Z][z2: Z][result5: unit]
(`z2 > 0` /\ `y2 > 0` /\
`z2 = (Zdiv ((Zdiv x y2) + y2) 2)` /\
`x < (y2 + 1) * (y2 + 1)` /\
`x < (z2 + 1) * (z2 + 1)`) /\
`z2 >= y2` y1 z1 result4 Post3) end)
result1 result1 result2 (refl_equal ? result1)
(sqrt_po_5 x Pre6 Test5 Test3 result1 Post5 Pre5
result2 Post4)) in
let (result4, Post17) = (exist_1 [result4: Z]
`result4 * result4 <= x` /\
`x < (result4 + 1) * (result4 + 1)` y0
(sqrt_po_6 x Pre6 Test5 Test3 result1 Post5 Pre5
result2 Post4 y0 z0 Post3)) in
(exist_3 [y1: Z][z1: Z][result5: Z]
`result5 * result5 <= x` /\
`x < (result5 + 1) * (result5 + 1)` y0 z0 result4
Post17) in
(exist_2 [y1: Z][result4: Z]
`result4 * result4 <= x` /\
`x < (result4 + 1) * (result4 + 1)` y0 result3 Post15) in
(exist_1 [result3: Z]`result3 * result3 <= x` /\
`x < (result3 + 1) * (result3 + 1)` result2 Post14) in
(exist_1 [result2: Z]`result2 * result2 <= x` /\
`x < (result2 + 1) * (result2 + 1)` result1 Post13) end) in
(exist_1 [result1: Z]`result1 * result1 <= x` /\
`x < (result1 + 1) * (result1 + 1)` result0 Post11) end) in
(exist_1 [result0: Z]`result0 * result0 <= x` /\
`x < (result0 + 1) * (result0 + 1)` result Post9).