Require Why.
Require Export sqrt_dicho_why.
Definition sqrt
: (x: Z)(_: `x >= 0`)
(sig_1 Z [result: Z](`result * result <= x` /\
`x < (result + 1) * (result + 1)`))
:= [x: Z; Pre5: `x >= 0`]
let (result, Post10) =
let (inf, Post7) = (exist_1 [result: Z]result = `0` `0`
(refl_equal ? `0`)) in
let (inf1, result, Post11) =
let (sup, Post6) = (exist_1 [result: Z]result = `x + 1` `x + 1`
(refl_equal ? `x + 1`)) in
let (inf1, sup1, result, Post12) =
let (mil, Post5) = (exist_1 [result: Z]result = `0` `0`
(refl_equal ? `0`)) in
let (inf1, mil1, sup1, result, Post13) =
let (inf1, mil1, sup1, result, Post4) =
(well_founded_induction Z (Zwf ZERO) (Zwf_well_founded `
0`) [Variant1: Z](inf1: Z)(mil1: Z)(sup1: Z)
(_: Variant1 = `sup1 - inf1`)(_0: `inf1 * inf1 <= x` /\
`x < sup1 * sup1` /\ `inf1 < sup1`)
(sig_4 Z Z Z unit [inf2: Z][mil2: Z][sup2: Z]
[result: unit]((`inf2 * inf2 <= x` /\
`x < sup2 * sup2` /\ `inf2 < sup2`) /\ `inf2 + 1 = sup2`))
[Variant1: Z; wf1: (Variant2: Z)
(Pre1: (Zwf `0` Variant2 Variant1))(inf1: Z)(mil1: Z)
(sup1: Z)(_: Variant2 = `sup1 - inf1`)
(_0: `inf1 * inf1 <= x` /\ `x < sup1 * sup1` /\
`inf1 < sup1`)
(sig_4 Z Z Z unit [inf2: Z][mil2: Z][sup2: Z]
[result: unit]((`inf2 * inf2 <= x` /\
`x < sup2 * sup2` /\ `inf2 < sup2`) /\
`inf2 + 1 = sup2`));
inf1: Z; mil1: Z; sup1: Z;
Pre4: Variant1 = `sup1 - inf1`;
Pre3: `inf1 * inf1 <= x` /\ `x < sup1 * sup1` /\
`inf1 < sup1`]
let (result, Bool2) =
let (result1, Post14) =
(Z_noteq_bool `inf1 + 1` sup1) in
(exist_1 [result2: bool]
(if result2 then `inf1 + 1 <> sup1`
else `inf1 + 1 = sup1`) result1
Post14) in
Cases
(btest
[result:bool]
(if result then `inf1 + 1 <> sup1`
else `inf1 + 1 = sup1`) result
Bool2) of
| (left Test4) =>
let (inf2, mil2, sup2, result0, Post4) =
let (inf2, mil2, sup2, result0, Post8) =
let Pre2 =
(sqrt_po_1 x Pre5 inf Post7 sup Post6 mil
Post5 Variant1 inf1 sup1 Pre4 Pre3 Test4) in
let (mil2, result0, Post1) =
let (result0, Post1) = (exist_1 [result0: Z]
result0 = (Zdiv (`inf1 + (sup1 + 1)`) `2`)
(Zdiv (`inf1 + (sup1 + 1)`) `2`)
(refl_equal ? (Zdiv (`inf1 + (sup1 + 1)`)
`2`))) in
(exist_2 [mil3: Z][result1: unit]
mil3 = (Zdiv (`inf1 + (sup1 + 1)`) `2`)
result0 tt Post1) in
let (inf2, sup2, result1, Post8) =
let (result1, Bool1) =
let (result3, Post15) =
(Z_lt_ge_bool x `mil2 * mil2`) in
(exist_1 [result4: bool]
(if result4 then `x < mil2 * mil2`
else `x >= mil2 * mil2`) result3
Post15) in
Cases
(btest
[result1:bool]
(if result1 then `x < mil2 * mil2`
else `x >= mil2 * mil2`) result1
Bool1) of
| (left Test3) =>
let (sup2, result2, Post2) =
let (result2, Post2) =
(exist_1 [result2: Z]
result2 = mil2 mil2
(refl_equal ? mil2)) in
(exist_2 [sup3: Z][result3: unit]
sup3 = mil2 result2 tt Post2) in
(exist_3 [inf2: Z][sup3: Z][result3: unit]
(`inf2 * inf2 <= x` /\
`x < sup3 * sup3` /\ `inf2 < sup3`) /\
(Zwf `0` `sup3 - inf2` `sup1 - inf1`)
inf1 sup2 result2
(sqrt_po_2 x Pre5 inf Post7 sup Post6 mil
Post5 Variant1 inf1 sup1 Pre4 Pre3 Test4
Pre2 mil2 Post1 Test3 sup2 Post2))
| (right Test2) =>
let (inf2, result2, Post3) =
let (result2, Post3) =
(exist_1 [result2: Z]
result2 = mil2 mil2
(refl_equal ? mil2)) in
(exist_2 [inf3: Z][result3: unit]
inf3 = mil2 result2 tt Post3) in
(exist_3 [inf3: Z][sup2: Z][result3: unit]
(`inf3 * inf3 <= x` /\
`x < sup2 * sup2` /\ `inf3 < sup2`) /\
(Zwf `0` `sup2 - inf3` `sup1 - inf1`)
inf2 sup1 result2
(sqrt_po_3 x Pre5 inf Post7 sup Post6 mil
Post5 Variant1 inf1 sup1 Pre4 Pre3 Test4
Pre2 mil2 Post1 Test2 inf2 Post3)) end in
(exist_4 [inf3: Z][mil3: Z][sup3: Z]
[result2: unit](`inf3 * inf3 <= x` /\
`x < sup3 * sup3` /\ `inf3 < sup3`) /\
(Zwf `0` `sup3 - inf3` `sup1 - inf1`) inf2
mil2 sup2 result1 Post8) in
((wf1 `sup2 - inf2`) (loop_variant_1 Pre4 Post8)
inf2 mil2 sup2 (refl_equal ? `sup2 - inf2`)
(proj1 ? ? Post8)) in
(exist_4 [inf3: Z][mil3: Z][sup3: Z][result1: unit]
(`inf3 * inf3 <= x` /\ `x < sup3 * sup3` /\
`inf3 < sup3`) /\ `inf3 + 1 = sup3` inf2 mil2
sup2 result0 Post4)
| (right Test1) =>
let (inf2, mil2, sup2, result0, Post4) =
(exist_4 [inf2: Z][mil2: Z][sup2: Z]
[result0: unit](`inf2 * inf2 <= x` /\
`x < sup2 * sup2` /\ `inf2 < sup2`) /\
`inf2 + 1 = sup2` inf1 mil1 sup1 tt
(conj ? ? Pre3 Test1)) in
(exist_4 [inf3: Z][mil3: Z][sup3: Z][result1: unit]
(`inf3 * inf3 <= x` /\ `x < sup3 * sup3` /\
`inf3 < sup3`) /\ `inf3 + 1 = sup3` inf2 mil2
sup2 result0 Post4) end `sup - inf` inf mil
sup (refl_equal ? `sup - inf`)
(sqrt_po_4 x Pre5 inf Post7 sup Post6 mil Post5)) in
let (result0, Post16) = (exist_1 [result0: Z]
`result0 * result0 <= x` /\
`x < (result0 + 1) * (result0 + 1)` inf1
(sqrt_po_5 x Pre5 inf Post7 sup Post6 mil Post5 inf1 sup1
Post4)) in
(exist_4 [inf2: Z][mil2: Z][sup2: Z][result1: Z]
`result1 * result1 <= x` /\
`x < (result1 + 1) * (result1 + 1)` inf1 mil1 sup1 result0
Post16) in
(exist_3 [inf2: Z][sup2: Z][result0: Z]
`result0 * result0 <= x` /\
`x < (result0 + 1) * (result0 + 1)` inf1 sup1 result Post13) in
(exist_2 [inf2: Z][result0: Z]`result0 * result0 <= x` /\
`x < (result0 + 1) * (result0 + 1)` inf1 result Post12) in
(exist_1 [result0: Z]`result0 * result0 <= x` /\
`x < (result0 + 1) * (result0 + 1)` result Post11) in
(exist_1 [result0: Z]`result0 * result0 <= x` /\
`x < (result0 + 1) * (result0 + 1)` result Post10).