Library Coq.ZArith.Zsqrt
Definition and properties of square root on Z
The following tactic replaces all instances of (POS (xI ...)) by
`2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH.
Ltac compute_POS :=
match goal with
| |-
context [(
Zpos (
xI ?X1))] =>
match constr:X1
with
|
context [1%positive] =>
fail 1
|
_ =>
rewrite (
BinInt.Zpos_xI X1)
end
| |-
context [(
Zpos (
xO ?X1))] =>
match constr:X1
with
|
context [1%positive] =>
fail 1
|
_ =>
rewrite (
BinInt.Zpos_xO X1)
end
end.
Inductive sqrt_data (
n:Z) :
Set :=
c_sqrt :
forall s r:Z,
n =
s *
s +
r -> 0 <=
r <= 2 *
s ->
sqrt_data n.
Definition sqrtrempos :
forall p:positive,
sqrt_data (
Zpos p).
Defined.
Define with integer input, but with a strong (readable) specification.
Definition Zsqrt :
forall x:Z,
0 <=
x ->
{
s :
Z & {
r :
Z |
x =
s *
s +
r /\
s *
s <=
x < (
s + 1) * (
s + 1)}}.
Defined.
Define a function of type Z->Z that computes the integer square root,
but only for positive numbers, and 0 for others.
A basic theorem about Zsqrt_plain
Positivity
Direct correctness on squares.
Zsqrt_plain is increasing