# Library Coq.ZArith.Zsqrt

Require Import ZArithRing.
Require Import Omega.
Require Export ZArith_base.
Open Local Scope Z_scope.
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.
Definition Zsqrt_plain (x:Z) : Z :=
match x with
| Zpos p =>
match Zsqrt (Zpos p) (Zorder.Zle_0_pos p) with
| existS s _ => s
end
| Zneg p => 0
| Z0 => 0
end.
A basic theorem about Zsqrt_plain
Theorem Zsqrt_interval :
forall n:Z,
0 <= n ->
Zsqrt_plain n * Zsqrt_plain n <= n <
( Zsqrt_plain n + 1) * ( Zsqrt_plain n + 1).
Positivity
Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n.
Direct correctness on squares.
Theorem Zsqrt_square_id: forall a, 0 <= a -> Zsqrt_plain (a * a) = a.
Zsqrt_plain is increasing
Theorem Zsqrt_le:
forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q.