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.
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.
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.
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
Direct correctness on squares.
Zsqrt_plain is increasing