# 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.