1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Definition of a square root function for Z. *)
Require Import BinPos BinInt.
Local Open Scope Z_scope.
Definition Zsqrtrem n :=
match n with
| 0 => (0, 0)
| Zpos p =>
match Pos.sqrtrem p with
| (s, IsPos r) => (Zpos s, Zpos r)
| (s, _) => (Zpos s, 0)
end
| Zneg _ => (0,0)
end.
Definition Zsqrt n :=
match n with
| 0 => 0
| Zpos p => Zpos (Pos.sqrt p)
| Zneg _ => 0
end.
Lemma Zsqrtrem_spec : forall n, 0<=n ->
let (s,r) := Zsqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
Proof.
destruct n. now repeat split.
generalize (Pos.sqrtrem_spec p). simpl.
destruct 1; simpl; subst; now repeat split.
now destruct 1.
Qed.
Lemma Zsqrt_spec : forall n, 0<=n ->
let s := Zsqrt n in s*s <= n < (Zsucc s)*(Zsucc s).
Proof.
destruct n. now repeat split. unfold Zsqrt.
rewrite <- Zpos_succ_morphism. intros _. apply (Pos.sqrt_spec p).
now destruct 1.
Qed.
Lemma Zsqrt_neg : forall n, n<0 -> Zsqrt n = 0.
Proof.
intros. now destruct n.
Qed.
Lemma Zsqrtrem_sqrt : forall n, fst (Zsqrtrem n) = Zsqrt n.
Proof.
destruct n; try reflexivity.
unfold Zsqrtrem, Zsqrt, Pos.sqrt.
destruct (Pos.sqrtrem p) as (s,r). now destruct r.
Qed.
|
