# Module sqrt.sqrt_valid

``` 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). ```

Index