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.